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

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

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

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

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

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

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

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

$(\mathrm{\lambda <!--\; \lambda \; -->}x:\mathrm{\sigma <!--\; \sigma \; -->}.M)N{\to <!--\; \to \; -->}_{\mathrm{\beta <!--\; \beta \; -->}}M[x:=N]$$(\lambda x\!:\!\sigma .~M)~N\ \to _{{\beta }}\ M[x:=N]$ .

$\mathrm{\eta <!--\; \eta \; -->}$$\eta$ -редукция определяется так

$\mathrm{\lambda <!--\; \lambda \; -->}x:\mathrm{\sigma <!--\; \sigma \; -->}.Mx{\to <!--\; \to \; -->}_{\mathrm{\eta <!--\; \eta \; -->}}M$$\lambda x\!:\!\sigma .~M~x\ \to _{{\eta }}\ M$ .

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

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

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

$f:(\mathrm{\beta <!--\; \beta \; -->}\to <!--\; \to \; -->\mathrm{\gamma <!--\; \gamma \; -->}),g:(\mathrm{\alpha <!--\; \alpha \; -->}\to <!--\; \to \; -->\mathrm{\beta <!--\; \beta \; -->}),x:\mathrm{\alpha <!--\; \alpha \; -->}$$f\!:\!(\beta \to \gamma ),g\!:\!(\alpha \to \beta ),x\!:\!\alpha$ 

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

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

$\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->M:\mathrm{\sigma <!--\; \sigma \; -->}$$\Gamma \vdash M\!:\!\sigma$ 

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

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

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

Аксиома. Если переменной $x$$x$  присвоен в контексте тип $\mathrm{\sigma <!--\; \sigma \; -->}$$\sigma$ , то в этом контексте $x$$x$  имеет тип $\mathrm{\sigma <!--\; \sigma \; -->}$$\sigma$ . В виде правила вывода:

$\frac{x:\mathrm{\sigma <!--\; \sigma \; -->}\in <!--\; \in \; -->\mathrm{\Gamma <!--\; \Gamma \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->x:\mathrm{\sigma <!--\; \sigma \; -->}}$${{x\!:\!\sigma \in \Gamma } \over {\Gamma \vdash x\!:\!\sigma }}$

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

$\frac{\mathrm{\Gamma <!--\; \Gamma \; -->},x:\mathrm{\sigma <!--\; \sigma \; -->}⊢<!--\; ⊢\; -->M:\mathrm{\tau <!--\; \tau \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->(\mathrm{\lambda <!--\; \lambda \; -->}x:\mathrm{\sigma <!--\; \sigma \; -->}.M):(\mathrm{\sigma <!--\; \sigma \; -->}\to <!--\; \to \; -->\mathrm{\tau <!--\; \tau \; -->})}$${{\Gamma ,x\!:\!\sigma \vdash M\!:\!\tau } \over {\Gamma \vdash (\lambda x\!:\!\sigma .~M)\!:\!(\sigma \to \tau )}}$

Правило удаления $\to <!--\; \to \; -->$$\rightarrow$ . Если в некотором контексте терм $M$$M$  имеет тип $\mathrm{\sigma <!--\; \sigma \; -->}\to <!--\; \to \; -->\mathrm{\tau <!--\; \tau \; -->}$$\sigma \to \tau$ , а терм $N$$N$  имеет тип $\mathrm{\sigma <!--\; \sigma \; -->}$$\sigma$ , то применение $MN$$M~N$  имеет тип $\mathrm{\tau <!--\; \tau \; -->}$$\tau$ . В виде правила вывода:

$\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->M:(\mathrm{\sigma <!--\; \sigma \; -->}\to <!--\; \to \; -->\mathrm{\tau <!--\; \tau \; -->})\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->N:\mathrm{\sigma <!--\; \sigma \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->(MN):\mathrm{\tau <!--\; \tau \; -->}}$${{\Gamma \vdash M\!:\!(\sigma \to \tau )\quad \Gamma \vdash N\!:\!\sigma } \over {\Gamma \vdash (M~N)\!:\!\tau }}$

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

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

$x:\mathrm{\alpha <!--\; \alpha \; -->}⊢<!--\; ⊢\; -->x:\mathrm{\alpha <!--\; \alpha \; -->}$$x\!:\!\alpha \vdash x\!:\!\alpha$      (аксиома)

$⊢<!--\; ⊢\; -->(\mathrm{\lambda <!--\; \lambda \; -->}x:\mathrm{\alpha <!--\; \alpha \; -->}.x):(\mathrm{\alpha <!--\; \alpha \; -->}\to <!--\; \to \; -->\mathrm{\alpha <!--\; \alpha \; -->})$$\vdash (\lambda x\!:\!\alpha .~x)\!:\!(\alpha \to \alpha )$      (введение $\to <!--\; \to \; -->$$\rightarrow$ )

$f:(\mathrm{\beta <!--\; \beta \; -->}\to <!--\; \to \; -->\mathrm{\gamma <!--\; \gamma \; -->}\to <!--\; \to \; -->\mathrm{\delta <!--\; \delta \; -->}),y:\mathrm{\beta <!--\; \beta \; -->}⊢<!--\; ⊢\; -->(fy):(\mathrm{\gamma <!--\; \gamma \; -->}\to <!--\; \to \; -->\mathrm{\delta <!--\; \delta \; -->})$$f\!:\!(\beta \to \gamma \to \delta ),y\!:\!\beta \vdash (f~y)\!:\!(\gamma \to \delta )$       (удаление $\to <!--\; \to \; -->$$\rightarrow$ )

СвойстваПравить

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