Объясните в самом простом, большая часть возможного английского языка без жаргонов, “универсальное свойство сгиба”?
Вы должны использовать структуру хэш-набора и сделать что-то вроде этого непроверенного java-кода:
HashSet set = new LinkedHashSet();
while (set.size() < n) {
set.add(random.nextInt(delta));
}
return set.toArray();
Метод HashSet.add не добавит значение, если оно уже присутствует. [ 114]
Адаптируйте этот код к вашей ситуации.
4 ответа
(Режим жаргона отключен: -)
Универсальное свойство - это просто способ доказать, что два выражения равны. (Это то, что подразумевается под жаргоном «принцип доказательства».) Универсальное свойство гласит, что если вы можете доказать эти два уравнения
g [] = v
g (x:xs) = f x (g xs)
, то вы можете заключить дополнительное уравнение
g = fold f v
Обратное также верно, но это тривиально показать, просто расширив определение сгиба . Универсальное свойство - это гораздо более глубокое свойство (что является жаргонным способом сказать, что менее очевидно, почему оно истинно).
Причина, по которой это вообще интересно, заключается в том, что это позволяет вам избежать доказательства по индукции, что почти всегда стоит избегать.
Я только что нашел новую (для меня) запись в Википедии «Универсальная собственность». Это проливает тонну света на этот вопрос. Вот ссылка: Из этого я (условно) заключаю следующее:
- Хотя вы можете подумать о 100 различных способах просмотра списка, вычисления по пути и производя одно окончательное значение из списка, все 100 из этих способов изоморфны (это означает, что в конечном итоге они одинаковы). На самом деле есть только один способ уменьшить список до одного значения, это FOLD.
- Fold также является «наиболее эффективным решением» того, как свести список к одному значению. Или вы можете сказать, самое «факторизованное» или наиболее «упрощенное» решение.
Вместе, кажется, эти 2 пункта отражают значение термина «универсальная собственность».
the paper defines two properties:
g [] = v
g (x : xs) = f x (g xs)
and then states that fold is not only a function that satisfies those properties, but is the only function that satisfies those properties. that it is unique in that regard is what makes it 'universal' in the sense the paper is using.
Свойство fold состоит в том, что это функция рекурсии списка, которая эквивалентна всем другим функциям рекурсии списка, при условии, что вы зададите ей правильные параметры.
У него есть это свойство, потому что он принимает в качестве параметра функции, которые будут применяться к элементам в списке.
Например, если мы написали простую функцию суммы:
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, это не имеет значения!)