Я внедряю в Haskell нечистый нетипизированный лямбда-исчисление-интерпретатор.Haskell и лямбда-исчисление: реализация альфа-конгруэнтности (альфа-эквивалентность)
В настоящее время я придерживаюсь реализации «альфа-конгруэнтности» (также называемой «альфа-эквивалентность» или «альфа-равенство» в некоторых учебниках). Я хочу, чтобы проверить, являются ли два лямбда-выражения равными или не равными друг другу. Например, если ввести следующее выражение в интерпретатор он должен давать True (\ используется для обозначения символа лямбды):
>\x.x == \y.y
True
Проблемы понимание ли следующая лямбда-выражения считаются альфа-эквивалентом или нет:
>\x.xy == \y.yx
???
>\x.yxy == \z.wzw
???
В случае \x.xy == \y.yx я предположил бы, что ответ True. Это связано с тем, что \x.xy => \z.zy и \y.yx => \z.zy и правые части обоих одинаковы (где символ => используется для обозначения альфа-восстановления).
В cae \x.yxy == \z.wzw Я бы также предположил, что ответ True. Это потому, что \x.yxy => \a.yay и \z.wzw => \a.waw, которые (я думаю) равны.
Беда в том, что все определения моих учебников утверждают, что для обозначения двух лямбда-выражений необходимо учитывать только имена переменных. В нем ничего не говорится о переменных в выражении, которое необходимо также переименовать. Так что хотя y и w оба находятся в правильном месте в лямбда-выражениях, как бы программа «знала», что первая y представляет первые w, а вторая y представляет вторую w. Мне нужно было быть последовательным в этом.
Вкратце, как я мог бы реализовать безошибочную версию функции isAlphaCongruent? Каковы точные правила, которые я должен соблюдать, чтобы это работало?
Я бы предпочел сделать это, не используя индексы Bruijn.
Они не эквивалентны , Возьмем '\ x.xy'. Вы можете переименовать 'x' по своему усмотрению и всегда получать одно и то же, но вы не можете переименовать' y' по своему усмотрению, поскольку он не ограничен лямбда-абстракцией. То же самое касается '\ y.yx', но на этот раз это' x', который не связан и, следовательно, не может быть переименован. Это означает, что вы не можете переименовать их, чтобы выполнить сравнение «\ x.xy == \ y.yx» true. См. wikipedia для получения более подробной информации. –
Более конкретно, '\ x.xy' можно переписать в' \ a.ay' и '\ y.yx' могут быть переписаны на' \ a.ax', тогда должно быть очевидно, что '\ a.ay/= \ a.ax'. –