Знает, я упоминал полное в каком-то месте на форуме (вместе с этим сокращением, так что ищется), но вообще это
Types and programming languages. У неё ещё есть продолжение —
Advanced topics in types and programming languages.
Я бы создал тему, но опять же не имею понятия о чём. Самую базовую конструкцию в соответствии Карри—Говарда — соответствие между типизированным исчислением комбинаторов и импликативным куском интуиционистской логики — легко увидеть практически сразу.
В первом у нас есть базовые комбинаторы
с типами
и
, и можно получить из комбинаторов
и
комбинатор
. (Стрелку
я считаю здесь везде правоассоциативной, что и естественно.)
Во втором у нас есть аксиомы
и
и есть правило вывода Modus ponens:
.
Видно, что
и аксиомы друг другу соответствуют (почти: я записал вторую аксиому в более традиционном для неё виде, но в ней можно поменять порядок «аргументов» и иметь
), а аппликация комбинаторов, позволяющая строить новые, соответствует MP, позволяющему получать новые теоремы. Конечно, тут нам везёт, что сейчас это соответствие такое буквальное, ведь есть эквивалентные аксиоматизации второй логики и эквивалентные базисы в первом исчислении, и можно выбрать их так, что соответствие будет не таким наглядным. И даже MP может быть иногда заменён чем-то ещё, хотя для импликативного фрагмента такое выглядело бы неестественным.
Теперь должны стать понятнее слова «термы-типы соответствуют высказываниям, термы-значения соответствуют выводам», хотя тут ещё мало что можно увидеть.
Дальше всё просто наращивается. Например, можно перейти к просто типизированному λ-исчислению с одного края и к натуральной дедукции (опять же интуиционистской и ограниченной формулами с одной импликацией) с другого: абстракция будет соответствовать превращению вывода из гипотезы в безусловный вывод импликации (в гильбертовском исчислении это метатеорема, а не правило вывода — оно недостаточно выразительно, чтобы сделать её «настоящим» правилом). Правило типирования λ-абстракции такое:
— и его можно прочитать как операцию над натуральным выводом: если у нас в нём есть подвывод из гипотезы
, помеченной маркером
некоторого
(и весь этот подвывод мы могли бы назвать выражением
), мы можем дальше вывести
и разрядить гипотезу
, то есть её больше нигде нельзя использовать (и такой вывод обозначим как
, и в нём
уже не встречается свободно, он «инкапсулирован»).
означает все прочие ещё не разряженные гипотезы — множество каких-то других предположений вида
— они в новом выводе остаются неразряженными.