Оценка SKI-комбинаторов без достаточных аргументов

Question

Мне было поручено показать, что

S(KK)I = K

Поскольку S принимает три аргумента, я просто застрял в начале, не зная, как с этим справиться. Я вижу два аргумента, а именно (К.К.) и я, но третьего, который я могу "заметить", нет. Что происходит в этой ситуации? Это своего рода работал для меня уже, просто оставив вне г в S хуг = XZ (YZ), что давало KK(I) и, как следствие, K. Мне это кажется неправильным, поэтому я хочу спросить здесь. Это правильный способ сделать это?

Я также не понимаю, что происходит с КИ, например, как K также требует два аргумента и получает только я. Правильно ли мое решение или я должен действовать по-другому?

Answer 1

Я думаю об этом так, что S (KK) I - это функция, которая принимает единственный аргумент - вызовите его. Что происходит, когда мы вызываем эту функцию с произвольным?

      S(KK)Iz -> KKz(Iz) -> Kz

Таким образом, вызов S (KK) I с помощью точно такой же, как вызов K с помощью z. Следовательно, S (KK) I и K - одна и та же функция.

Answer 2

Самый простой способ решить ваш вопрос - это использование eta-конвертации. А именно, каждый терм M ведет себя как терм (λx.M x) (конечно, x не может быть свободным в M). Таким образом, если комбинаторы, которые вы хотите оценить, не имеют некоторых аргументов, вы можете преобразовать термин и затем применить эти комбинаторы.

В вашем примере вам нужно два eta-преобразования. Ниже приведены сокращения после первого.

S(KK)I -> λx.S(KK)Ix -> λx.KKx(Ix) -> λx.K(Ix) 

Теперь у вас есть внешний комбинатор K, у которого отсутствует второй аргумент. Если вы преобразуете в eta самый внешний член: λy.(Λx.K(I x)) y, вы получите λy.K(I y), что не очень забавно. Но вы можете применить eta-преобразование к подтермингу термина, например, к основной части лямбда-абстракции. Таким образом, вы можете преобразовать λx.K(I x) в λx. (Λy.K(I x) y). Это приводит к λx.λy.I x, который сводится к λx.λy.x, и этот термин является определением комбинатора K. Вуаля!

Фактически, вы можете доказать эквивалентность комбинаторов без использования eta-преобразования, но тогда вам нужно использовать некоторые не очень удобные аксиомы в качестве правил переписывания (подробности см. В главе 7 Хенка П. Барендрегта (1984). Лямбда-исчисление: Его синтаксис и семантика).