Типизации по Черчу и Карри

Существуют два основных подхода к определению типизированного лямбда-исчисления. Первый подход, принадлежащий Черчу это явная типизация. Каждому терму сопоставляется единственный тип. Это означает, что в процессе конструирования термов, нетипизированные термы модифицируются с помощью дополнительной характеристики - типа. Для констант этот тип задан заранее, но переменные могут иметь любой тип. Правила корректного формирования термов выглядят следующим образом:

Однако мы будем использовать для типизации подход Карри, который является неявным. Термы могут иметь или не иметь типа, и если терм имеет тип, то он может быть не единственным. Например, функция идентичности λх. х может иметь любой тип вида σ —> σ. Такой подход более предпочтителен, поскольку, во-первых, он соответствует используемому в языках типа Haskell понятию полиморфизма, а во-вторых, позволяет не задавать типы явным образом.

Определим понятие типизируемости по отношению к контексту, т. е. конечному набору предположений о типах переменных. Будем записывать:

чтобы обозначить, что «в контексте? терм Т может иметь тип σ». Будем употреблять запись или просто Т:: σ, если суждение о типизации выполняется в пустом контексте. Элементы контекста? имеют вид ν:: σ, т. е. они представляют собой предположения о типах переменных. Будем предполагать, что в? нет противоречивых предположений.