Можно ли определить

18

Я знаю, что невозможно определить эквивалентность для нетипизированного лямбда-исчисления. Цитирование Барендрегта, Л. П. Лямбда-исчисление: его синтаксис и семантика. Северная Голландия, Амстердам (1984). :β

Если A и B являются непересекающимися непустыми множествами лямбда-членов, замкнутых относительно равенства, то A и B рекурсивно неразделимы. Отсюда следует, что если A - нетривиальное множество лямбда-термов, замкнутое при равенстве, то A не является рекурсивным. Итак, мы не можем решить проблему "M = x?" для любого конкретного М. Кроме того, из этого следует, что лямбда не имеет рекурсивных моделей.

Если у нас есть нормализующая система, такая как Система F, то мы можем решить -эквивалентность «извне», сократив два заданных условия и сравнив, являются ли их нормальные формы одинаковыми или нет. Однако можем ли мы сделать это «изнутри»? Существует ли комбинатор System-F такой, что для двух комбинаторов и мы имеем если и имеют одинаковую нормальную форму, и противном случае? Или это можно сделать хотя бы для некоторых с? комбинатор такой, что истинно тогда и только тогда, когдаβЕMNEMN=trueMNEMN=falseMEMEMNNβM? Если нет, то почему?

Петр Pudlák
источник

Ответы:

19

Нет, это невозможно. Рассмотрим следующие два обитателя типа .(AB)(AB)

M=λf.fN=λf.λa.fa

Это различные -нормальные формы, но их нельзя отличить лямбда-термином, поскольку N является η- расширением M , а η- расширение сохраняет наблюдательную эквивалентность в чисто типизированном лямбда-исчислении.βNηMη

Коди спросил, что произойдет, если мы также откажемся от эквивалентности. Ответ все еще отрицателен из-за параметричности. Рассмотрим следующие два условия на типа ( & alpha ; .η :(α.αα)(α.αα)

Mзнак равноλе:(α,αα),Λα,λИкс:α,е[α,αα](Λβ,λY:β,Y)[α]ИксNзнак равноλе:(α,αα),Λα,λИкс:α,е[α]Икс

Они имеют различную нормальную, η- длинную форму, но обсервационно эквивалентны. Фактически все функции этого типа эквивалентны, так как α .βη - кодировка типа блока, и поэтому все функции типа ( α .α,αα должен быть экстенсивно эквивалентным.(α,αα)(α,αα)

Нил Кришнасвами
источник
2
Хорошо, тот же вопрос с -эквивалентностью :)β,η
cody
11

Другой возможный ответ на совершенно правильному Нееля: Предположим , что это комбинатор , хорошо напечатанный в системе F такое , что вышеуказанное условие выполнено. Тип E :ЕЕ

Е:α,ααбооL

Оказывается, есть бесплатная теорема, которая выражает, что такой термин обязательно постоянен :

T, T,U,T',U':T, Е T T Uзнак равноЕ T T' U'

В частности, - это постоянно истинная функция или постоянно ложная функция, и она не может быть «решающим фактором равенства».Е

Коди
источник