Да, конечно. Многие типизированные лямбда-исчисления по своей природе принимают только строго нормализующие термины, поэтому они не могут выражать произвольные вычисления. Но система типов может быть чем угодно; сделайте его достаточно широким, и вы сможете выразить все детерминированные вычисления.
Система тривиального типа, которая охватывает полный по Тьюрингу фрагмент лямбда-исчисления, - это система, которая принимает каждый термин как хорошо типизированный (с верхним типом ).
Γ ⊢ M: ⊤
На практике статически типизированные функциональные языки программирования имеют в своей основе типизированное лямбда-исчисление, которое позволяет использовать комбинатор с фиксированной точкой как хорошо типизированный. Например, начните с простого набора лямбда-исчисления (или системы типов ML, или системы F, или любой другой системы типов по вашему выбору) и добавьте правило, которое делает некоторый комбинатор с фиксированной точкой, например, хорошо напечатан.
Γ ⊢ f : T → TY =λf, ( λ x . f( хx ) ) ( λ x . f( хх ) )
Правила, представленные выше, довольно неуклюжи, так как они составляют такие термины, какY
Γ ⊢ f: T→ TΓ ⊢ Yе: TΓ ⊢ f: T→ TΓ ⊢ ( λ x . F( хx ) ) ( λ x . f( хх ) ) : Т
хорошо напечатаны, хотя их составляющие не являются хорошо напечатанными - они не являются полностью композиционными. Простое решение - добавить комбинатор точек фиксации в качестве языковой константы и предоставить для него дельта-правило; тогда легко иметь систему типов и семантику редукции ссохранением типов. Вы действительно уходите от чистого лямбда-исчисления в область лямбда-исчисления с константами.
Yе
Таким образом, у вас есть система типов, которая определяет полный по Тьюрингу язык (поскольку каждый термин хорошо типизирован), и простую характеристику завершающих вычислений. Конечно, поскольку эта система типов характеризует нормализацию, она не разрешима.
Ответы:
Да, конечно. Многие типизированные лямбда-исчисления по своей природе принимают только строго нормализующие термины, поэтому они не могут выражать произвольные вычисления. Но система типов может быть чем угодно; сделайте его достаточно широким, и вы сможете выразить все детерминированные вычисления.
Система тривиального типа, которая охватывает полный по Тьюрингу фрагмент лямбда-исчисления, - это система, которая принимает каждый термин как хорошо типизированный (с верхним типом ).
На практике статически типизированные функциональные языки программирования имеют в своей основе типизированное лямбда-исчисление, которое позволяет использовать комбинатор с фиксированной точкой как хорошо типизированный. Например, начните с простого набора лямбда-исчисления (или системы типов ML, или системы F, или любой другой системы типов по вашему выбору) и добавьте правило, которое делает некоторый комбинатор с фиксированной точкой, например, хорошо напечатан. Γ ⊢ f : T → TY =λf, ( λ x . f( хx ) ) ( λ x . f( хх ) )
Правила, представленные выше, довольно неуклюжи, так как они составляют такие термины, какY
Придерживаясь чистого лямбда-исчисления, интересной системой типов является лямбда-исчисление с типами пересечений.
Типы пересечений имеют интересные свойства в отношении нормализации:
См. Характеристика лямбда-терминов, которые имеют типы объединения, для понимания того, почему типы пересечений имеют такую замечательную область.
Таким образом, у вас есть система типов, которая определяет полный по Тьюрингу язык (поскольку каждый термин хорошо типизирован), и простую характеристику завершающих вычислений. Конечно, поскольку эта система типов характеризует нормализацию, она не разрешима.
источник