SKS равен SKK?

Question

Контекст

Вчера вечером я начал изучать лямбда-исчисление, и я пытаюсь определить, правильно ли то, что я понимаю до сих пор.

Понимание

SKK эквивалентен комбинатору Identity I.

Где L означает лямбда:

S = LxLyLz((xz)(yz))

К = LxLy(x)

K по существу берет следующие 2 (лямбда) термина и возвращает первый из них. S кажется немного более сложным в нетипизированном лямбда-исчислении.

Моя интерпретация

SK (любой лямбда-термин) также эквивалентен I.

Т.е. применение приложения S к K к Any-lambda-term эквивалентно комбинатору Identity:

((СК)(Любой)) = I = СКК = ((СК)(К))

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

Рассуждение

SK = LyLz((Kz)(yz))

Следующий лямбда-терм будет заменен на y, пусть это будет Y.

НЕБО = Lz((Kz)(Yz))

(Y z) — это применение Y к z, также лямбда-члену.(K z) возвращает постоянную функцию, которая возвращает z при наличии другого входного термина: (Y z).

Верна ли моя интерпретация? Если нет, можете ли вы дать объяснение? Я буду очень признателен. В частности, если можно объяснить своего рода порядок операций — я регулярно оказываюсь в замешательстве, когда решаю, когда оценивать. Возможно, это исправится с практикой.

Answer 1

Ваша интуиция верна, но интуиция ничего не доказывает (увы...)

Итак, как мы можем доказать ваше утверждение? Просто показав, что SKK и SKS ведут себя одинаково. «Поведение» - это неформальное понятие, которое формально охвачено «семантикой»: если СКК и СКС равны, то они всегда должны сводиться к одному и тому же термину, согласно семантике СКИ-исчисления.

Теперь возникает глубокий вопрос: что такое SKI-исчисление? На самом деле, нет единого способа ответить на этот вопрос. Что вы неявно делаете в своем вопросе, так это то, что вы выражаете SKI в терминах λ и полагаетесь на семантику λ-исчисления. Это абсолютно правильно. Другой способ сделать это мог бы заключаться в непосредственном определении семантики SKI. Например, если вы посмотрите на страницу википедии , вы увидите, что семантика не определяется с помощью лямбда-терминов (и тот факт, что она соответствует лямбда-термину, является (приятным и ожидаемым) побочным эффектом). В остальной части этого ответа я буду использовать тот же подход, что и вы, и конвертировать термины SKI в термины λ. Хорошим упражнением для вас будет повторить доказательство, используя правильную семантику SKI.

Итак, позвольте формализовать ваш вопрос: ваш вопрос состоит в том, для любого термина SKI , SKKt = SKSt? Что ж... Посмотрим.

кодируется как (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)tв λ-исчислении. Теперь осталось привести его к нормальной форме (я подробно описываю каждый шаг, каждый раз уменьшая крайний левый λ, хоть это и не самая быстрая стратегия):

      (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.x)t
= (λy.λz.((λx.λy.x)z)(yz))(λx.λy.x)t
= (λz.((λx.λy.x)z)((λx.λy.x)z))t
= ((λx.λy.x)t)((λx.λy.x)t)
= (λy.t)((λx.λy.x)t)
= t

Итак, кодировка SKKtв исчислении λ сводится к (в качестве примечания, мы только что доказали, что это эквивалентно здесь). Чтобы завершить наше доказательство, мы должны свести и посмотреть, сводится ли оно также к .

SKStкодируется как (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.λz.(xz)(yz))t. Пусть уменьшит. (на этот раз я не так подробно рассказываю)

      (λx.λy.λz.(xz)(yz))(λx.λy.x)(λx.λy.λz.(xz)(yz))t
= ((λx.λy.x) t)((λx.λy.λz.(xz)(yz)) t))
= (λy.t)((λx.λy.λz.(xz)(yz)) t))
= t

Ура! Это также сводится к , так что действительно, SKSа также SKKэквивалентны. Кажется, что третий комбинатор не важен: как только вы SK?, это эквивалентно I. В качестве упражнения это можно легко доказать (такая же стратегия, если и так, то для любых условий tа также s, SKts = s). Как упоминалось выше, другим хорошим упражнением является повторение доказательства без использования семантики λ, но с использованием правильной семантики SKI.

Наконец, мой ответ должен вызвать у вас новый вопрос: у нас есть две семантики, одна из которых кодирует термины SKI в термины λ, а другая — нет. У вас может возникнуть вопрос: эквивалентны ли две семантики? Что означает эквивалентность двух семантик? Если вы только начинаете изучать λ-исчисление, возможно, вам пока рано пытаться ответить на эти вопросы прямо сейчас, но вы можете держать их в уме до тех пор, пока не познакомитесь с формальными языками.