Мне нужно найти функцию 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
последней. Я просто не знаю, действительно ли моя функция повторяет это.
Любая оказанная помощь приветствуется
(h, i, i+1)
кортежем? Как вы представляете кортежи в LC? - person melpomene   schedule 30.04.2018