Историческая связь между типизированным лямбда-исчислением и Лиспом?

16

Недавно у меня была беседа с другом (сторонником строго типизированных языков). Он сделал комментарий:

Изобретатели Lambda Calculus всегда предполагали, что он будет напечатан.

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

Теперь, когда Джон Маккарти создал Лисп - он основал его на лямбда-исчислении . По его собственному признанию, он опубликовал «Рекурсивные функции символьных выражений и их вычисление на машине, часть I» . Вы можете прочитать это здесь .

Маккарти, кажется, не обращался к Простому Типу Лямбда-исчисления. Кажется, в этом доминирует Робин Милнер с ML .

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

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

Hawkeye
источник
1
Вероятно, как-то связано с тем, что типизированное лямбда-исчисление не является полным по Тьюрингу.
Ян Йоханнсен
Спасибо @JanJohannsen - не могли бы вы рассказать об этом?
Соколиный глаз

Ответы:

17

λ

Отличный обзор истории находится в этой статье .

λ

Сэм Тобин-Хохштадт
источник
Ничего себе - ответил самый квалифицированный человек в мире на эту тему. Спасибо @Sam. Возможно, я получу к вам докторскую заявку к концу года. (Похоже, что Ambrose BS с нетерпением ожидает совместной работы с вами).
Соколиный глаз
3
Я действительно очень далек от самого квалифицированного человека в мире по этой теме.
Сэм Тобин-Хохштадт
Ссылка не работает. Я полагаю, что это тот же документ: hope.simons-rock.edu/~pshields/cs/cmpt312/cardone-hindley.pdf
bmaddy