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

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

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

В базовой версии системы ${\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 году доказал , что ${\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. // Handbook of Logic in Computer Science. — Oxford University Press, 1992. — Т. II . — С. 117-309 .