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

Эта статья находится на начальном уровне проработки, в одной из её версий выборочно используется текст из источника, распространяемого под свободной лицензией
Материал из энциклопедии Руниверсалис

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

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

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

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

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

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

Правила редукции не отличаются от правил для бестипового лямбда-исчисления. [math]\displaystyle{ \beta }[/math]-редукция определяется через подстановку

[math]\displaystyle{ (\lambda x\!:\!\sigma.~M)~N\ \to_{\beta}\ M[x:=N] }[/math].

[math]\displaystyle{ \eta }[/math]-редукция определяется так

[math]\displaystyle{ \lambda x\!:\!\sigma.~M~x\ \to_{\eta}\ M }[/math].

Для [math]\displaystyle{ \eta }[/math]-редукции требуется, чтобы переменная [math]\displaystyle{ x }[/math] не была свободной в терме [math]\displaystyle{ M }[/math].

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

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

[math]\displaystyle{ f\!:\!(\beta\to\gamma),g\!:\!(\alpha\to\beta),x\!:\!\alpha }[/math]

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

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

[math]\displaystyle{ \Gamma\vdash M\!:\!\sigma }[/math]

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

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

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

Аксиома. Если переменной [math]\displaystyle{ x }[/math] присвоен в контексте тип [math]\displaystyle{ \sigma }[/math], то в этом контексте [math]\displaystyle{ x }[/math] имеет тип [math]\displaystyle{ \sigma }[/math]. В виде правила вывода:

[math]\displaystyle{ {x\!:\!\sigma \in \Gamma}\over{\Gamma \vdash x\!:\!\sigma } }[/math]

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

[math]\displaystyle{ {\Gamma,x\!:\!\sigma\vdash M\!:\!\tau}\over{\Gamma\vdash (\lambda x\!:\!\sigma.~M)\!:\!(\sigma \to \tau)} }[/math]

Правило удаления [math]\displaystyle{ \rightarrow }[/math]. Если в некотором контексте терм [math]\displaystyle{ M }[/math] имеет тип [math]\displaystyle{ \sigma \to \tau }[/math], а терм [math]\displaystyle{ N }[/math] имеет тип [math]\displaystyle{ \sigma }[/math], то применение [math]\displaystyle{ M~N }[/math] имеет тип [math]\displaystyle{ \tau }[/math]. В виде правила вывода:

[math]\displaystyle{ {\Gamma\vdash M\!:\!(\sigma\to\tau)\quad\Gamma\vdash N\!:\!\sigma}\over{\Gamma\vdash (M~N)\!:\!\tau} }[/math]

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

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

[math]\displaystyle{ x\!:\!\alpha\vdash x\!:\!\alpha }[/math]     (аксиома)
[math]\displaystyle{ \vdash (\lambda x\!:\!\alpha.~x)\!:\!(\alpha\to\alpha) }[/math]     (введение [math]\displaystyle{ \rightarrow }[/math])
[math]\displaystyle{ f\!:\!(\beta\to\gamma\to\delta),y\!:\!\beta\vdash (f~y)\!:\!(\gamma\to\delta) }[/math]      (удаление [math]\displaystyle{ \rightarrow }[/math])

Свойства

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

Примечания

  1. ↑ A. Church. A Formulation of the Simple Theory of Types // J. Symbolic Logic. — 1940. — С. 56-68.
  2. ↑ H. B. Curry. Functionality in Combinatory Logic // Proc Natl Acad Sci USA. — 1934. — С. 584–590.
  3. ↑ W. W. Tait. Intensional Interpretations of Functionals of Finite Type I // J. Symbolic Logic. — 1967. — Т. 32(2).

Литература

  • 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.
Источник — https://xn--h1ajim.xn--p1ai/index.php?title=Просто_типизированное_лямбда-исчисление&oldid=5822659