Языки программирования с каноническими функциями

29

Существуют ли (функциональные?) Языки программирования, в которых все функции имеют каноническую форму? То есть любые две функции, которые возвращают одинаковые значения для всего набора ввода, представляются одинаково, например, если f (x) вернул x + 1, а g (x) вернул x + 2, то f (f (x )) и g (x) будут генерировать неразличимые исполняемые файлы при компиляции программы.

Возможно, что еще более важно, где / как я могу найти больше информации о каноническом представлении программ (поиск в программах "программы канонического представления" был менее чем плодотворным)? Кажется, что это естественный вопрос, и я боюсь, что просто не знаю, как найти то, что я ищу. Мне любопытно, возможно ли, чтобы такой язык был завершен по Тьюрингу, и если нет, то насколько выразительным может быть язык программирования, при этом сохраняя такое свойство.

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

math4tots
источник

Ответы:

38

Степень, в которой это возможно, на самом деле является главным открытым вопросом в теории лямбда-исчисления. Вот краткое изложение того, что известно:

  • Простое типизированное лямбда-исчисление с единицами, продуктами и функциональным пространством имеет свойство простых канонических форм. Два слагаемых равны тогда и только тогда, когда они имеют одинаковую бета-нормальную и длинную форму. Вычисление этих нормальных форм также довольно просто.

  • Добавление типов сумм значительно усложняет ситуацию. Проблема равенства все еще разрешима (ключевое слово для поиска - «совместное равенство»), но известные алгоритмы работают по чрезвычайно сложным причинам, и, насколько мне известно, не существует полностью удовлетворяющей теоремы о нормальной форме. Вот четыре подхода, которые я знаю:

  • Добавление неограниченных типов, таких как натуральные числа, делает проблему неразрешимой. По сути, теперь вы можете закодировать десятую проблему Гильберта.

  • Добавление рекурсии делает проблему неразрешимой, потому что наличие нормальных форм делает равенство разрешимым, и это позволит вам решить проблему остановки.

Нил Кришнасвами
источник
Эта статья расширяет эквивалентность с копроизведениями до эквивалентности с суммами, но нет синтаксиса «единой» канонической формы, вы выбираете «функцию насыщения», которая достаточно умна, чтобы обнаружить, когда два сравниваемых вами термина имеют подтермы, которые оказываются ложными. Это больше всего похоже на Ахмеда-Ликата-Харпера в том, что они оба используют фокусировку.
Макс Новый
При наличии только единицы, продуктов и функций количество элементов, которые вы можете записать, равно 1, тогда как, если вы добавите суммы, вы внезапно получите много разных мощностей (и сможете выполнить «полезные вычисления»). Связаны ли эти факты?
Glaebhoerl
1
бλИкс:б,λY:б,ИксλИкс:б,λY:б,Y