Классификация типизированных / нетипизированных лямбда-исчислений

Может кто-нибудь объяснить кратко (если это возможно!) Или отослать меня к ссылке, обобщающей различия между нетипизированным лямбда-исчислением и более распространенным типизированным лямбда-исчислением?

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

Хотя я, конечно, намереваюсь читать, что-то вроде справочной таблицы с изложением исчислений и их эквивалентностей / различий / места в иерархии было бы ОГРОМНЫМ справочником, чтобы помочь мне разобраться в них.

Не сказать, что ниже это правильно, просто пытаюсь набросать вместе некоторые из впечатлений, которые я должен увидеть, если они хотя бы служат отправной точкой (или что-то, чтобы исправить!)

Нетипизированное лямбда-исчисление - экв. к логике первого порядка - не могу сделать X

Проще говоря, лямбда-исчисление - eq to ... логика, связанная с Лиспом?

«Полиморфный» лямбда-кальций и т. Д.

Конструктивное исчисление - интуиционистская логика?

Комбинаторная логика - сравнима с ??? типизированное лямбда-исчисление, относящееся к языкам APL / J

Если это связано с лямбда-кубом и его тремя осями, тем лучше.

Несмотря на то, что я знаком с основами лямбда-исчисления и программирования с функциональными языками, я никогда не задумывался и не имел каких-либо существенных связей с системами типов и различными разновидностями лямбда-исчислений (и, возможно, пи?).

Когда я пытаюсь исследовать это, я не могу помочь, но оказываюсь в стороне, открывая множество вкладок браузера и разветвляясь в столь многих направлениях, что я никогда не вхожу ни в одну из них с какой-либо глубиной!

Я не уверен, разумно ли то, о чем я прошу, но, надеюсь, по крайней мере, я нарисовал достаточно картинок, чтобы предложить какое-то чтение, которое может объяснить, что я ищу?

Ваш стол немного запутан; вот лучше.

• Как отмечает Андрей, нетипизированное лямбда-исчисление - без логической интерпретации
• Простое типизированное лямбда-исчисление - интуиционистская логика высказываний
• Полиморфное лямбда-исчисление - чистая логика второго порядка (т.е. без квантификаторов первого порядка)
• Зависимые типы - обобщение логики первого порядка
• Исчисление конструкций - обобщение логики высшего порядка

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

Вы также можете связать синтаксическую форму исчисления с логическими системами.

• Комбинаторные исчисления (например, комбинаторы SKI). Гильбертовы системы
• А-нормальная форма - исчисление секвенций
• Обычное типизированное лямбда-исчисление - естественный вывод

Чистый нетипизированный калькуляция является полным по Тьюрингу, т. Е. Частичное теоретико-числовое отображение вычислимо тогда и только тогда, когда оно определимо в нетипизированном λ- калькуляторе. Вычислительная мощность типизированного λ- исчисления намного меньше. Например, если мы добавим тип натуральных чисел к типизированному λ- вычислению вместе с 0 , преемником и примитивной рекурсией, мы получим то, что обычно известно как T Геделя . Он вычисляет только примитивно-рекурсивные функции (и все они суммарные).$\lambda$$\lambda$$\lambda$nat$\lambda$$0$$T$

Нетипизированный калькуляция не имеет разумной интерпретации в соответствии с соответствием Карри-Говарда, в то время как типизированный λ- калькуляция точно соответствует интуиционистскому исчислению высказываний.$\lambda$$\lambda$

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

$\lambda$$\lambda$$\lambda$Ulambda : U -> (U -> U)gamma : (U -> U) -> U$\lambda$$\mathbb{U}$$\lambda$$\mathcal{C}$$\mathbb{U}$$\mathbb{U}$$[\mathcal{C}^{\mathrm{op}}, \mathsf{Set}]$$\mathbb{U} \cong \mathbb{U}^{\mathbb{U}}$

Ссылки:

• Дана С. Скотт: « Лямбда-исчисление: некоторые модели, некоторая философия », Исследования по логике и основам математики, том 101, 1980, страницы 223-265, Симпозиум Клини

• Хендрик Питер Барендрегт: « Лямбда-исчисление: его синтаксис и семантика », Elsevier, 1984.

Довольно полное обсуждение этого материала можно найти в этой книге: Лекции по изоморфизму Карри-Ховарда . Это основано на свободно доступной старой версии: лекции по изоморфизму Карри-Говарда .