Просто типизированное лямбда-исчисление

В базовой версии системы ${\displaystyle \lambda ^{\rightarrow }}$ типы конструируются из набора переменных с помощью единственного бинарного инфиксного конструктора ${\displaystyle \rightarrow }$. По традиции для переменных типа используют греческие буквы, а оператор ${\displaystyle \rightarrow }$ считают правоассоциативным, то есть ${\displaystyle \alpha \rightarrow \beta \to \gamma }$ является сокращением для ${\displaystyle \alpha \rightarrow (\beta \to \gamma )}$. Буквы из второй половины греческого алфавита (${\displaystyle \sigma }$, ${\displaystyle \tau }$, и т.д.) часто используются для обозначения произвольных типов, а не только переменных типа.

Различают две версии просто типизированной системы. Если в качестве термов используются те же термы, что и в бестиповом лямбда-исчислении, то систему называют неявно типизированной или типизированной по Карри. Если же переменные в лямбда-абстракции аннотируются типами, то систему называют явно типизированной или типизированной по Чёрчу. В качестве примера приведём тождественную функцию в стиле Карри: ${\displaystyle \lambda x.~x}$, и в стиле Чёрча: ${\displaystyle \lambda x\!:\!\alpha .~x}$.

Правила редукции не отличаются от правил для бестипового лямбда-исчисления. ${\displaystyle \beta }$-редукция определяется через подстановку

${\displaystyle (\lambda x\!:\!\sigma .~M)~N\ \to _{\beta }\ M[x:=N]}$.

${\displaystyle \eta }$-редукция определяется так

${\displaystyle \lambda x\!:\!\sigma .~M~x\ \to _{\eta }\ M}$.

Для ${\displaystyle \eta }$-редукции требуется, чтобы переменная ${\displaystyle x}$ не была свободной в терме ${\displaystyle M}$.

Контекстом называется множество утверждений о типизации переменных, разделённых запятой, например,

${\displaystyle f\!:\!(\beta \to \gamma ),g\!:\!(\alpha \to \beta ),x\!:\!\alpha }$

Контексты обычно обозначают прописными греческими буквами: ${\displaystyle \Gamma ,\Delta }$. В контекст можно добавить «свежую» для этого контекста переменную: если ${\displaystyle \Gamma }$ — допустимый контекст, не содержащий переменной ${\displaystyle x}$, то ${\displaystyle \Gamma ,x\!:\!\alpha }$ — тоже допустимый контекст.

Общий вид утверждения о типизации таков:

${\displaystyle \Gamma \vdash M\!:\!\sigma }$

Это читается следующим образом: в контексте ${\displaystyle \Gamma }$ терм ${\displaystyle M}$ имеет тип ${\displaystyle \sigma }$.

В просто типизированном лямбда-исчислении приписывание типов термам осуществляется по приведённым ниже правилам.

Аксиома. Если переменной ${\displaystyle x}$ присвоен в контексте тип ${\displaystyle \sigma }$, то в этом контексте ${\displaystyle x}$ имеет тип ${\displaystyle \sigma }$. В виде правила вывода:

${\displaystyle {x\!:\!\sigma \in \Gamma } \over {\Gamma \vdash x\!:\!\sigma }}$

Правило введения ${\displaystyle \rightarrow }$. Если в некотором контексте, расширенном утверждением, что ${\displaystyle x}$ имеет тип ${\displaystyle \sigma }$, терм ${\displaystyle M}$ имеет тип ${\displaystyle \tau }$, то в упомянутом контексте (без ${\displaystyle x}$), лямбда-абстракция ${\displaystyle \lambda x\!:\!\sigma .~M}$ имеет тип ${\displaystyle \sigma \to \tau }$. В виде правила вывода:

${\displaystyle {\Gamma ,x\!:\!\sigma \vdash M\!:\!\tau } \over {\Gamma \vdash (\lambda x\!:\!\sigma .~M)\!:\!(\sigma \to \tau )}}$

Правило удаления ${\displaystyle \rightarrow }$. Если в некотором контексте терм ${\displaystyle M}$ имеет тип ${\displaystyle \sigma \to \tau }$, а терм ${\displaystyle N}$ имеет тип ${\displaystyle \sigma }$, то применение ${\displaystyle M~N}$ имеет тип ${\displaystyle \tau }$. В виде правила вывода:

${\displaystyle {\Gamma \vdash M\!:\!(\sigma \to \tau )\quad \Gamma \vdash N\!:\!\sigma } \over {\Gamma \vdash (M~N)\!:\!\tau }}$

Первое правило позволяет приписать тип свободным переменным, задав их в контексте. Второе правило позволяет типизировать лямбда-абстракцию стрелочным типом, убирая из контекста связываемую этой абстракцией переменную. Третье правило позволяет типизировать аппликацию (применение) при условии, что левый аппликант имеет подходящий стрелочный тип.

Примеры утверждений о типизации в стиле Чёрча:

${\displaystyle x\!:\!\alpha \vdash x\!:\!\alpha }$     (аксиома)

${\displaystyle \vdash (\lambda x\!:\!\alpha .~x)\!:\!(\alpha \to \alpha )}$     (введение ${\displaystyle \rightarrow }$)

${\displaystyle f\!:\!(\beta \to \gamma \to \delta ),y\!:\!\beta \vdash (f~y)\!:\!(\gamma \to \delta )}$      (удаление ${\displaystyle \rightarrow }$)