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

Материал из Википедии — свободной энциклопедии
Перейти к: навигация, поиск

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

Формальное описание[править | править вики-текст]

Синтаксис типов и термов[править | править вики-текст]

В базовой версии системы \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 году Уильям Тэйт доказал[3], что \beta-редукция для просто типизированной системы обладает свойством сильной нормализации: любой допустимый терм за конечное число \beta-редукций приводится к единственной нормальной форме. Как следствие \beta\eta-эквивалентность термов оказывается разрешимой в этой системе.
  • Изоморфизм Карри — Ховарда связывает просто типизированное лямбда-исчисление с так называемой «минимальной логикой» (фрагментом интуиционистской логики высказываний, включающим только импликацию): населённые типы являются в точности тавтологиями этой логики, а термы соответствуют доказательствам, записанным в форме естественного вывода.

Примечания[править | править вики-текст]

  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).

Литература[править | править вики-текст]