Церковные цифры в лямбда-исчислении

Question

Мне нужно найти функцию P такую, что (используя бета-редукцию)

P(g, h, i) ->* (h, i, i+1).

Мне разрешено использовать функцию-преемник succ. Из википедии я получил

succ = λn.λf.λx.f(n f x)

Мой ответ P = λx.λy.λz.yz(λz.λf.λu.f(z f u))z

но я не совсем уверен в этом. Моя логика заключалась в том, что λx будет эффективно избавляться от термина g, тогда λy. λz будет вводить h и i через yz. Тогда функция succ выдаст i+1 последним. Я просто не знаю, действительно ли моя функция повторяет это.

Любая оказанная помощь приветствуется

Answer 1

@ melpomene указывает на то, что этот вопрос не может быть решен без конкретной реализации (например, для кортежей). Я собираюсь предположить , что ваш кортеж реализован как:

T = λabcf.f a b c

Или, если вы предпочитаете не-стенографию:

T = (λa.(λb.(λc.(λf.f a b c))))

То есть функция, которая закрывает a, b и c и ожидает, пока функция f не передаст эти переменные.

Если это имеет в виду реализацию и предполагается, что используются обычные церковные цифры, то указанная вами функция:

P(g, h, i) ->* (h, i, i+1)

Необходимо:

1. взять тройку (с уже примененными a, b и c)
2. построить новую тройку, с
   • второе значение старой тройки
   • третье значение старой тройки
   • succ третьего значения старой тройки

Вот такая функция P:

P = λt.t (λghi.T h i (succ i))

Или еще раз, если вы предпочитаете не сокращенную запись:

P = (λt.t(λg.(λh.(λi.T h i (succ i)))))

Это можно частично очистить с помощью некоторых вспомогательных функций:

SND = λt.t (λabc.b)
TRD = λt.t (λabc.c)

В этом случае мы можем написать P как:

P = λt.T (SND t) (TRD t) (succ (TRD t))