Просто типизированное лямбда-исчисление (Hjkvmk mnhn[njkfguuky lxbQ;g-nvcnvlyuny)

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

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

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

В базовой версии системы $\lambda ^{\rightarrow }$ типы конструируются из набора переменных с помощью единственного бинарного инфиксного конструктора $\rightarrow$. По традиции для переменных типа используют греческие буквы, а оператор $\rightarrow$ считают правоассоциативным, то есть $\alpha \rightarrow \beta \to \gamma$ является сокращением для $\alpha \rightarrow (\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 .~M~x\ \to _{\eta }\ M$.

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

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

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

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

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

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

$\Gamma \vdash M\!:\!\sigma$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Свойства

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

Литература

• Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — ISBN 0-262-16209-1.
  • Перевод на русский язык: Пирс Б. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9.
• Barendregt, Henk. Lambda Calculi with Types // Handbook of Logic in Computer Science. — Oxford University Press, 1992. — Т. II. — С. 117-309.