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

Ответ 1

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

Да, но только грубо. В "чистом" нетипизированном лямбда-исчислении все кодируется как функции. (Вы можете использовать Google для популярной "Церковной кодировки" и менее популярной "кодировки Скотта".) Lisp имеет нефункциональные данные, такие как атомы и числа и т.д., Поэтому это будет считаться "нетипизированным лямбда-исчислением, расширенным с помощью констант."

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

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

Ответ 2

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

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

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

Ключевое слово lambda в LISP можно понять, ссылаясь на лямбда-исчисление только по аналогии. A LISP lambda expression является типом анонимной функции.

Ответ 3

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

Если вы хотите идентифицировать лямбда-исчисления с помощью системы типов, тогда Lisp является ее собственным, конечно. Ключевое слово 'lambda' в любом Lisp перед Схемой, конечно, претенциозно, и после Scheme есть место, чтобы сказать это. Просто использование "func" было бы более скромным. Lisp является главным процессором списка, а не "лямбда-исчислением"

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

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

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