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

Question

Я работаю через «Real World Haskell», который привел к бесплатному PDF-файлу под названием "A tutorial on the universality and expressiveness of fold". В нем говорится о том, что «складка» является «универсальной». Я борюсь с его определением «универсальный» и хотел бы услышать от тех, кто уже вложил время, переваривая его: Пожалуйста, объясните в простом, максимально свободном на английском языке английском языке «универсальное свойство складки»? Что это за «универсальная собственность», и почему это важно?

Спасибо.

Answer 1

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

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

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

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

g = fold f v 

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

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

Answer 2

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

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

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

Answer 3

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

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

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

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) 

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

Answer 4

Я только что нашел новую (для меня) запись в Википедии, Универсальная собственность ". Он проливает TON света на этот вопрос. Here's the link: От него я (tenatively) заключить следующее:

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

Вместе, кажется, эти 2 точки фиксируют значение термина «универсальное свойство».

Answer 5

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

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

Хотя я до сих пор пишу это, Followup обобщим это (и сделать это гораздо проще понять, хотя и более абстрактным), чтобы «откидные как» операции по общим структурам данных.

Посмотреть этот пост еще на то, что универсальное свойство: http://jeremykun.com/2013/05/24/universal-properties/

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

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