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

Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ${\lambda }^{\to }$) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году.

Формальное описание

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

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

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

Правила редукции

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

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

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

$\lambda x:\sigma .Mx{\to }_{\eta }M$.

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

Контексты типизации и утверждения типизации

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

$f:(\beta \to \gamma ),g:(\alpha \to \beta ),x:\alpha$

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

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

$\mathrm{\Gamma }⊢M:\sigma$

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

Правила типизации (по Чёрчу)

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

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

$\frac{x:\sigma \in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x:\sigma }$

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

$\frac{\mathrm{\Gamma },x:\sigma ⊢M:\tau }{\mathrm{\Gamma }⊢(\lambda x:\sigma .M):(\sigma \to \tau )}$

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

$\frac{\mathrm{\Gamma }⊢M:(\sigma \to \tau )\mathrm{\Gamma }⊢N:\sigma }{\mathrm{\Gamma }⊢(MN):\tau }$

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

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

$x:\alpha ⊢x:\alpha$     (аксиома)

$⊢(\lambda x:\alpha .x):(\alpha \to \alpha )$     (введение $\to$)

$f:(\beta \to \gamma \to \delta ),y:\beta ⊢(fy):(\gamma \to \delta )$      (удаление $\to$)

Свойства

• Просто типизированная система обладает свойством типовой безопасности: при $\beta$-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
• В 1967 году Уильям Тэйт доказал, что $\beta$-редукция для просто типизированной системы обладает свойством сильной нормализации: любой допустимый терм за конечное число $\beta$-редукций приводится к единственной нормальной форме. Как следствие $\beta \eta$-эквивалентность термов оказывается разрешимой в этой системе.
• Изоморфизм Карри — Ховарда связывает просто типизированное лямбда-исчисление с так называемой «минимальной логикой» (фрагментом интуиционистской логики высказываний, включающим только импликацию): населённые типы являются в точности тавтологиями этой логики, а термы соответствуют доказательствам, записанным в форме естественного вывода.

Литература

• Шаблон:Книга
  • Перевод на русский язык: Шаблон:Книга
• Шаблон:Статья