Пожалуйста, объясните на простейшем, наиболее свободном от жаргона английском языке «универсальное свойство сгиба»? - PullRequest
16 голосов
/ 09 мая 2009

Я работаю через "Real World Haskell", что привело к созданию бесплатного PDF-файла под названием "Учебник по универсальности и выразительности сгиба" . Это указывает на то, что «сгиб» является «универсальным». Я борюсь с его определением «универсальный» и хотел бы услышать от тех, кто уже потратил время на его усвоение: Пожалуйста, объясните на простейшем, наиболее свободном от жаргонного словаря английском языке «универсальное свойство сгиба» ? Что это за «универсальное свойство» и почему оно важно?

Спасибо.

Ответы [ 5 ]

16 голосов
/ 09 мая 2009

(режим жаргона выключен: -)

Универсальное свойство - это просто способ доказать, что два выражения равны. (Это то, что подразумевается под жаргоном "принцип доказательства".) Универсальное свойство говорит о том, что если вы сможете доказать эти два уравнения

g []     = v
g (x:xs) = f x (g xs)

тогда вы можете заключить дополнительное уравнение

g = fold f v

Обратное также верно, но это тривиально показать, просто расширив определение fold. Универсальное свойство является гораздо более глубоким свойством (что является грубым выражением того, что менее очевидно, почему оно истинно.)

Причина, по которой вообще интересно делать это, заключается в том, что это позволяет вам избежать доказательства по индукции, чего почти всегда стоит избегать.

8 голосов
/ 09 мая 2009

бумага определяет два свойства:

g   []     = v
g (x : xs) = f x (g xs)

и затем заявляет, что fold - это не только функция a , которая удовлетворяет этим свойствам, но и функция only , которая удовлетворяет этим свойствам. то, что он уникален в этом отношении, делает его «универсальным» в том смысле, в котором его использует бумага.

6 голосов
/ 10 мая 2009

Свойство, которое имеет сворачивание, состоит в том, что это функция рекурсивной рассылки, которая эквивалентна всем другим функциям рекурсивной рассылки, если вы зададите ей правильные параметры.

У него есть это свойство, поскольку он принимает в качестве параметра функции, которые будут применяться к элементам в списке.

Например, если мы написали простую функцию суммы:

sum []          = 0
sum (head:tail) = head + (sum tail)

тогда мы могли бы вместо этого написать ее как функцию сгиба, передав оператор (+), который мы хотим использовать для объединения элементов:

sum list = foldl (+) 0 list

Таким образом, любая функция, которая действует просто и рекурсивно над списком, может быть переписана как функция сгиба. Эта эквивалентность является свойством. Я полагаю, что он называет это свойство универсальным, потому что оно работает над всеми этими без исключения рекурсивными алгоритмами с линейным списком.

И, как он объясняет, причина, по которой это свойство так полезно, состоит в том, что, поскольку мы можем показать, что все эти другие алгоритмы фактически эквивалентны свертыванию, доказав что-то о сворачивании, мы также докажем это для всех этих других алгоритмов. *

Мне лично было трудно понять функцию сгиба, поэтому иногда я использовал свою собственную, которая выглядит следующим образом:

-- forall - A kind of for next loop
-- list is list of things to loop through
-- f is function to perform on each thing
-- c is the function which combines the results of f
-- e is the thing to combine to when the end of the list is reached
forall :: [a] -> (a->b) -> (b->b->b) -> b -> b
forall [] f c e = e
forall (x:xs) f c e = c (f x) (forall xs f c e)

(На самом деле это немного мощнее, чем foldl, поскольку он имеет дополнительную функцию применения функции f к каждому элементу в списке.)

Ну, никто ничего не доказал в моей функции. Но это не имеет значения, потому что я могу показать, что моя функция на самом деле является функцией сгиба:

forall l f c e = foldl c e (map fn l)

И, следовательно, все то, что было доказано относительно сгиба, также подтверждено для моей функции поиска и всех ее применений в моей программе. (Обратите внимание, что нам даже не нужно учитывать, какая функция c предоставляется в каждом из различных вызовов forall и foldl, это не имеет значения!)

4 голосов
/ 09 сентября 2010

Я только что нашел новую (для меня) запись в Википедии "Универсальная собственность". Это проливает тонну света на этот вопрос. Вот ссылка: Из этого я (условно) заключаю следующее:

  1. Хотя вы можете думать о 100 различных способах обхода списка, вычислениях по пути и получении одного окончательного значения из списка, все 100 из этих способов изоморфны (что означает, что тоже самое) На самом деле есть только один способ сократить список до одного значения, это FOLD.
  2. Fold также является «наиболее эффективным решением» того, как свести список к одному значению. Или вы можете сказать, самое «факторизованное» или наиболее «упрощенное» решение.

Похоже, что вместе эти два пункта отражают значение термина "универсальная собственность".

2 голосов
/ 02 октября 2013

Хотя может быть немного трудно следовать без чтения предыдущих постов в серии, объясняющих универсальные свойства с категориальной точки зрения, этот пост дает подробное категориальное объяснение универсального свойства сгиба, а также карту и фильтр. 1001 *

http://jeremykun.com/2013/09/30/the-universal-properties-of-map-fold-and-filter/

Хотя мне еще предстоит написать это, продолжение обобщит это (и сделает его намного более простым для понимания, хотя и более абстрактным) для «складывающихся» операций над общими структурами данных.

См. Этот пост, чтобы узнать, что такое универсальное свойство: http://jeremykun.com/2013/05/24/universal-properties/

А здесь ссылки на все посты в серии: http://jeremykun.com/main-content/

По правде говоря, принятый в настоящее время ответ является самым простым способом понять, что универсальное свойство говорит о сгибе. Статьи, ссылки на которые приведены выше, просто дают более подробное техническое описание с помощью теории категорий, которая отсутствует в данной статье. Я не согласен с утверждением в принятом ответе, что универсальное свойство является гораздо более глубоким свойством, чем утверждение без жаргона. Универсальное свойство сгиба - это точно такое же утверждение, просто заключенное в язык начальных и конечных объектов, согласно природе анализа вещей с помощью теории категорий. Этот анализ ценен именно благодаря его естественным обобщениям.

...