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

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

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

• Просто типизированная система обладает свойством типовой безопасности: при ${\displaystyle \beta }$-редукциях тип лямбда-терма остаётся неизменным, а сама типизация не мешает продвижению вычислений.
• В 1967 году Уильям Тэйт доказал^[3], что ${\displaystyle \beta }$-редукция для просто типизированной системы обладает свойством сильной нормализации: любой допустимый терм за конечное число ${\displaystyle \beta }$-редукций приводится к единственной нормальной форме. Как следствие ${\displaystyle \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.