Существует ли полное типизированное лямбда-исчисление по Тьюрингу?

Question

Существуют ли какие-либо полные типизированные лямбда-исчисления по Тьюрингу?Если да, то приведите несколько примеров?

Answer 1

Да, конечно.Многие типизированные лямбда-вычисления принимают только сильно нормализующий термины сконструированы таким образом, что они не могут выражать произвольные вычисления.Но система типов может быть любой, какой вам заблагорассудится;сделайте его достаточно широким, и вы сможете выразить все детерминированные вычисления.

Тривиальная система типов, которая охватывает полный по Тьюрингу фрагмент лямбда-исчисления, - это та, которая принимает каждый термин как хорошо типизированный (с верхний тип).$$\dfrac{}{\Гамма \vdash M : op}$$

Более практично, статически типизированные функциональные языки программирования имеют в своей основе типизированное лямбда-исчисление, которое позволяет комбинатор фиксированных точек так же хорошо напечатанный.Например, начните с просто набранное лямбда - исчисление (или система типа ML, или система F или любая другая система типов по вашему выбору) и добавьте правило, которое создает некоторый комбинатор фиксированной точки, такой как $\ mathbf{Y} = \lambda f.(\лямбда x.f (x\,x)) (\лямбда x.f (x\,x))$ хорошо напечатан.$$ \dfrac{\Гамма \vdash f :T ightarrow T} {\Гамма \vdash \mathbf{Y}\,f :T} \qquad \dfrac{\Гамма \vdash f :T ightarrow T} {\Гамма \vdash (\лямбда x.f (x\,x)) (\лямбда x.f (x\,x)) :T} $$ Правила, представленные выше, довольно неуклюжи, поскольку они делают термины типа $\ mathbf{Y} \,f $ хорошо типизированными, даже если их составляющие не очень хорошо типизированы — они не являются полностью композиционными.Простое исправление состоит в том, чтобы добавить комбинатор фиксированной точки в качестве языковой константы и предоставить для него дельта-правило;тогда несложно иметь систему типов и семантику сокращения с сохранение типа.Вы действительно уходите от чистого лямбда-исчисления в область лямбда-исчисления с константами.$$\begin{собрать*} \dfrac{}{\Gamma \vdash extbf{исправить} :(T ightarrow T) ightarrow T} \\ extbf{исправить}\,f o f ( extbf {исправить}\,f) \\ \end{собрать*}$$

Придерживаясь чистого лямбда-исчисления, интересной системой типов является лямбда-исчисление с типами пересечений.

$$ \dfrac{\Гамма \vdash M :T_1 \quad \Gamma \vdash M :T_2} {\Гамма \vdash M :T_1 \клин T_2} (\клин I) \qquad\qquad \dfrac{} {\Гамма \vdash M : op} ( op I) $$

Типы пересечений обладают интересными свойствами в отношении нормализации:

• Лямбда-терм может быть введен без использования правила $ \ top I $, если оно сильно нормализуется.
• Лямбда-термин допускает тип, не содержащий $\ top$, если он имеет обычную форму.

Видишь Характеристика лямбда-терминов, имеющих типы объединения для понимания того, почему типы пересечений имеют такой замечательный охват.

Итак, у вас есть система типов, которая определяет язык, полный по Тьюрингу (поскольку каждый термин хорошо типизирован), и простая характеристика завершающих вычислений.Конечно, поскольку эта система типов характеризует нормализацию, она неразрешима.

_{Замечание по поводу имен правил $( op I)$ и $(\wedge I)$:они не имеют формального значения, но выбраны намеренно.$ I $ означает “введение”, потому что это правила введения — они вводят символ ($ \ wedge $ или $ \ top $) в тип под строкой.Дважды вы найдете правила исключения, когда символ появляется над линией, но не ниже.Например, правило проверки типа лямбда-выражения в простом типизированном лямбда-исчислении является вводным правилом для $ \ rightarrow $, а правило проверки типа приложения является правилом исключения для $ \ rightarrow $.}