Какой тип лямбда-исчисления будет примером для Лисп?

Question

Я пытаюсь лучше понять, как типы вступают в игру в лямбда-исчислении. По общему признанию, много вещей теории типа находится над моей головой. Лисп - это динамически типизированный язык, примерно ли это соответствует нетипизированному лямбда-исчислению? Или есть какое-то «динамически типизированное лямбда-исчисление», о котором я не знаю?

Answer 1

Лисп - это динамически типизированный язык, примерно ли это соответствует нетипизированному лямбда-исчислению?

Да, но только приблизительно. В «чистом» нетипизированном лямбда-исчислении все закодировано как функции. (Вы можете поискать в Google популярную «церковную кодировку» и менее популярную «кодировку Скотта».) Lisp имеет нефункциональные данные, такие как атомы, числа и т. Д., Так что это будет считаться «нетипизированным лямбда-исчислением, расширенным константами». 1005 *

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

Таким образом, Lisp соответствует нетипизированному лямбда-исчислению с вызовом по значению, расширенному с помощью констант .

Answer 2

Джон Маккарти представил LISP в в своей апрельской работе 1960 года «Рекурсивные функции символических выражений и их вычисление на машине, часть I» . Следующий абзац со страницы 6:

е. Функции и формы. Обычно в математике - вне математической логики - неточно употребляют слово «функция» и применяют его к формам. такие как у ² + х. Потому что мы позже будем вычислять с выражениями для функций, нам нужно различие между функциями и формами и обозначение для Это различие. Это различие и обозначение для его описания, от что мы отклоняемся тривиально, дано церковью [3].
...
3. А. ЦЕРКОВЬ, исчисления лямбда-преобразования (Принстонский университет Press, Princeton, N.J., 1941).

Статья Википедии о лямбда-исчислении имеет историю публикаций Церкви. Статья 1941 года, на которую ссылается Маккарти, похоже, о набранном *1016* лямбда-исчислении, что противоречит введению статьи из Википедии.

Ключевое слово lambda в Лиспе можно понимать как относящееся к лямбда-исчислению только по аналогии. Лямбда-выражение Lisp представляет собой тип анонимной функции .

Answer 3

Лисп не является "лямбда-исчислением", я не знаю, что такое "лямбда-исчисление".

Если вы хотите идентифицировать лямбда-исчисления по системе типов, тогда, конечно, Lisp - свое собственное. Ключевое слово «лямбда» в любом списке до Scheme, безусловно, претенциозно, и после Scheme есть место, чтобы сказать, что это так. Использование «func» было бы более скромным. Lisp - это в основном обработчик списков, а не «лямбда-исчисление»

Я также написал довольно обширную статью об этом, однажды пытаясь продемонстрировать, почему A: термин «функциональное программирование» не имеет смысла, а B: почему говорить о «лямбда-исчислении», а не «системе типов» так :

http://blog.nihilarchitect.net/archives/289/on-functional-programming/

Кроме того, имейте в виду, что в Лиспе все функции действуют один аргумент и могут иметь только списки в качестве аргументов.