Комбинаторная интерпретация лямбда-исчисления

10

По словам Питера Селинджера , Лямбда-исчисление алгебраическое (PDF). В начале этой статьи он говорит:

Известно, что комбинаторная интерпретация лямбда-исчисления несовершенна, поскольку она не удовлетворяет правилу: при интерпретации не подразумевает (Barendregt, 1984).ξM=Nλx.M=λx.N

Вопросов:

  • Какая эквивалентность подразумевается здесь?
  • Учитывая это определение эквивалентности, что является контрпримером импликации?
Саймон Шайн
источник

Ответы:

7

Эквивалентность - это просто эквивалентность в обсуждаемой эквациональной теории. В данном случае это теория, изложенная в таблице 1. Обратите внимание, что в эту теорию не входит : это сделает теорию экстенсиональной, и суть в том, что уважает , в то время как это делает CL частично экстенсиональный. Я не уверен, почему другой ответ упоминает .ληξλη

Обратите внимание, что в :λ

(1)(M=βN)(λx.M=βλx.N)

Это должно быть интуитивно очевидно: если является -конвертируемым в когда он стоит сам по себе, то он также -конвертируемым в когда он является .MβNβNλx.M

-правило, определяется как делает этот вывод напрямую возможным, когда он является частью -theory. Его аналогом CL будет: ξ

M=N(ξλ)(λx.M)=(λx.N)
λ
M=N(ξCL)(λx.M)=(λx.N)

Теперь дело в том, что в CL не выполняется следующее :

(2)(M=wN)(λx.M=wλx.N)

Другими словами, если два члена слабо равны, то это не обязательно верно для их псевдообращенных версий.

Следовательно, если мы добавим к теории CL, то начнем приравнивать члены, которые имеют разные нормальные формы.ξCL


Запись. Здесь обозначает слабое равенство. Это означает, что можно преобразовать в (и наоборот) с помощью ряда сокращений и (возможно, также , если это является частью теории). Как вы, вероятно, знаете, - это аналог CL .M=wNMNSKI=w=β

λ - это псевдоабстрактор, как определено на странице 5 вашего документа. Он имеет следующее свойство:

(3)(λx.M)Nw[N/x]M

Это свойство позволяет легко найти аналог CL для любого -term: просто измените на и примените переводы в соответствии с определением .λλλλ


Чтобы было ясно, «контрпример» в этом ответе не является контрпримером к (2). Потому что если у нас есть:

(4)M=x
(5)N=(λz.z)x

Тогда действительно означает (применяя переводы страницы 5 и тот факт, что определяется как в конце страницы 4):NISKK

(6)N=(λz.z)x=Ix=SKKx

Так , мы действительно имеем , что . Однако, если это контрпример, мы должны иметь это . Но если мы переведем, мы действительно получим:SKKxwKx(Kx)wxM=wN(λy.M)w(λy.N)

(7)(λy.M)=(λy.x)=Kx
(8)(λy.N)=(λy.SKKx)=K(SKKx)

И легко проверить, что (7) и (8) все еще слабо равны, для:

(9)K(SKKx)wK(Kx(Kx))wKx

Теперь правильным контрпримером к (2) будет:

M=Kxy
N=x

Так , мы , безусловно , есть , что . Однако, если вы внимательно переведете абстрагированные версии, то увидите, что обе они представляют собой разные нормальные формы - и они не могут быть преобразованы в соответствии с теоремой Черча-Россера.KxywxM=wN

Сначала мы проверяем :M

M=λx.Kxy=S(λx.Kx)(λx.y)=S(λx.Kx)(Ky)=S(S(λx.K)(λx.x))(Ky)=S(S(λx.K)(I))(Ky)=S(S(λx.K)(SKK))(Ky)=S(S(KK)(SKK))(Ky)
Здесь вы можете убедиться, что является нормальной формой. Здесь вы можете проверить, что , как и следовало ожидать, если должен вести себя как абстрактный для CL.M(λx.Kxy)PwPλ

Теперь мы проверяем : N

N=λx.x=I=SKK

Что, очевидно, является нормальной формой, отличной от , поэтому по теореме Черча-Россера. Отметим также , что , т.е. и „дают одинаковый выход“ для произвольных входов .MMwNNPwPMNP

Теперь мы доказали, что (2) не выполняется в CL, и что теория CL, включающая будет приравнивать термины, которые не являются слабо равными. Но почему мы заботимся?ξ

Ну, во-первых, это делает комбинаторную интерпретацию несовершенной: очевидно, не все метатеоретические свойства переносятся.λ

Кроме того, и, возможно, что еще более важно, хотя существуют экстенсиональные теории и CL, они изначально и обычно сохраняются как интенсиональные. Интенсивность является хорошим свойством, потому что и CL моделируют вычисления как процесс, и с этой точки зрения две разные программы (в частности, термины, которые имеют различную нормальную форму), которые всегда дают одинаковые результаты (при равных входных данных), не должны приравниваться. уважает этот принцип в , и если мы хотим сделать экстенсиональным, мы можем просто добавить, например, . Но введениеλλξλληξв CL больше не сделал бы это полностью интенциональным (фактически, только частично так). И это причина «s„Известность“, как кладет статью.ξ

Рой О.
источник
1
Я не могу комментировать качество, потому что мало знаю предмет, но это похоже на небольшую работу. Ценится, спасибо!
Рафаэль
Действительно, пост закончился дольше, чем я ожидал. Спасибо за ваш комментарий. :)
Рой О.
2
Ах это. Бывает . Регулярно .
Рафаэль
3

РЕДАКТИРОВАТЬ Этот ответ является неправильным, как правильно указал другой ответчик. Я использовал перевод в комбинаторную логику от Asperti & Longo, который немного отличается от того, что в Selinger.

Фактически, это иллюстрирует ключевой момент: «комбинаторная интерпретация» лямбда-исчисления - это не единственная вещь! Разные авторы делают это немного по-разному.

Я оставляю свой ответ здесь для потомков, но другой ответ лучше.


Эквивалентность в этом контексте определяется таблицами 1 и 2 в статье Селинджера. Однако, немного другая аксиоматизация может сделать вещи немного более ясными.

Что это действительно означает, так это то, что два термина обратимы в теории . Мы можем определить «конвертируемость» следующими двумя аксиомами:λ

  • β . , если свободен для в(λx.M)N=[N/x]MxNM
  • η . , если не свободен вλy.My=MyM

плюс, конечно же, обычные аксиомы и правила вывода, необходимые для конгруэнтности. Из этого должно быть очевидно, что любой контрпример будет опираться на условие свободной переменной при нарушении правила .=η

Я думаю, что это, наверное, самое простое:

M=x
N=(λz.z)x

Вы можете убедиться, что , но их соответствующие комбинаторные интерпретации не равны по правилам в таблице 2.λy.M=λy.N

Псевдоним
источник
Что я не понимаю в вашем ответе: 1) зачем упоминать , хотя теория в Таблице 1 не включает его и является явно интенциональной? 2) Как происходят комбинаторные интерпретации и не равно? Вывод в моем ответе показывает, что они есть. 3) Правило не рассматривается, хотя это и является причиной проблемы. ηλy.Mλy.Nξ
Рой О.