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

Ответы:

37

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

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

ΓM:

На практике статически типизированные функциональные языки программирования имеют в своей основе типизированное лямбда-исчисление, которое позволяет использовать комбинатор с фиксированной точкой как хорошо типизированный. Например, начните с простого набора лямбда-исчисления (или системы типов ML, или системы F, или любой другой системы типов по вашему выбору) и добавьте правило, которое делает некоторый комбинатор с фиксированной точкой, например, хорошо напечатан. Γ f : T TY=λf.(λx.f(xx))(λx.f(xx)) Правила, представленные выше, довольно неуклюжи, так как они составляют такие термины, какY

Γf:TTΓYf:TΓf:TTΓ(λx.f(xx))(λx.f(xx)):T
хорошо напечатаны, хотя их составляющие не являются хорошо напечатанными - они не являются полностью композиционными. Простое решение - добавить комбинатор точек фиксации в качестве языковой константы и предоставить для него дельта-правило; тогда легко иметь систему типов и семантику редукции ссохранением типов. Вы действительно уходите от чистого лямбда-исчисления в область лямбда-исчисления с константами. Yf
Γfix:(TT)Tfixff(fixf)

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

ΓM:T1ΓM:T2ΓM:T1T2(I)ΓM:(I)

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

  • I

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

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

(I)(I)I

Жиль "ТАК - прекрати быть злым"
источник