WikiSort.ru - Не сортированное

Синтаксис типов и термов

В базовой версии системы ${\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 }$ )