Определите бинарный экспоненциальный оператор CARAT.в лямбда-исчислении CARAT

Question

Я пытаюсь определить бинарный экспоненциальный оператор в лямбда-исчислении, скажем, оператор CARAT. Например, этот оператор может принимать два аргумента: лямбда-кодировку числа 2 и лямбда-кодировку числа 4 и вычисляет лямбда-кодировку числа 16. Я не знаю, мой ответ правильный или неправильный, но мне потребовался день сделать это. Я использовал определение церковных цифр. Вот мой ответ. Пожалуйста, поправьте меня, если мой ответ неверен. Я не знаю, как сделать это правильно. Если кто-то знает, пожалуйста, помогите мне найти краткий ответ.

Функция-преемник next, которая добавляет единицу, может определять натуральные числа в терминах нуля и следующего:

1 = (next 0)    
2 = (next 1)
  = (next (next 0))    
3 = (next 2)
  = (next (next (next 0)))

Из приведенного выше заключения мы можем определить следующую функцию:

next = λ n. λ f. λ x.(f ((n f) x))
one  = (next zero)
     => (λ n. λ f. λ x.(f ((n f) x)) zero)
     => λ f. λ x.(f ((zero f) x))
     => λ f. λ x.(f ((λ g. λ y.y f) x)) -----> (* alpha conversion avoids clash *)
     => λ f. λ x.(f (λ y.y x))
     => λ f. λ x.(f x)

Таким образом, мы можем смело доказать, что…

zero = λ f. λ x.x
one = λ f. λ x.(f x)
two = λ f. λ x.(f (f x))
three = λ f. λ x.(f (f (f x)))
four = λ f. λ x.(f (f (f (f x))))
:
:
:
Sixteen = λ f. λ x.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))

Дополнение это просто итерация преемника. Теперь мы можем определить дополнение с точки зрения следующего:

m next n => λx.(nextm x) n => nextm n => m+n
add = λ m. λ n. λ f. λ x.((((m next) n) f) x)
four = ((add two) two)
     => ((λ m. λ n. λ f. λ x.((((m next) n) f) x) two) two)
     => (λ n. λ f. λ x.((((two next) n) f) x)two)
     => λ f. λ x.((((two next) two) f x)
     => λ f. λ x.(((( λ g. λ y.(g (g y)) next) two) f x)
     => λ f. λ x.((( λ y.(next (next y)) two) f) x)
     => λ f. λ x.(((next (next two)) f) x)
     => λ f. λ x.(((next (λ n. λ f. λ x.(f ((n f) x)) two)) f) x)

Подставив значения для "следующий", а затем "два", мы можем еще больше уменьшить вышеупомянутую форму до

     => λ f. λ x.(f (f (f (f x)))) 

то есть четыре.

Аналогично, Умножение - это итерация сложения. Таким образом, Умножение определяется следующим образом:

mul = λ m. λ n. λ x.(m (add n) x)
six = ((mul two) three)
 => ((λ m. λ n. λ x.(m (add n) x) two) three)
 => (λ n. λ x.(two (add n) x) three)
 => λ x.(two (add three) x
 => ( λf. λx.(f(fx)) add three) 
 =>( λx.(add(add x)) three)
 => (add(add 3))
 => ( λ m. λ n. λ f. λ x.((((m next) n) f) x)add three)
 => ( λ n. λ f. λ x.((( three next)n)f)x)add)
 => ( λ f. λ x.((three next)add)f)x)

После подстановки значений для "три", "следующий" и затем "добавить", а затем снова для "следующий", приведенная выше форма уменьшится до

 => λ f. λ x.(f (f (f (f (f (f x)))))) 

то есть шесть.

Наконец, возведение в степень может быть определено повторным умножением

Предположим, что функция возведения в степень называется CARAT

CARAT = λm.λn.(m (mul n) )
sixteen => ((CARAT four) two)
 => (λ m. λ n.(m (mul n) four) two)
 => (λ n.(two (mul n)four
 => (two (mul four))
 => ((λ f. λ x.(f (f x))))mul)four)
 => (λ x. (mul(mul x))four)
 => (mul(mul four))))
 => (((((λ m. λ n. λ x.(m (add n) x)mul)four)
 => ((((λ n. λ x.(mul(add n) x)four)
 => (λ x.(mul(add four) x))
 => (λ x (λ m. λ n. λ x.(m (add n) x add)four) x
 => (λ x (λ n. λ x. (add(add n) x)four)x
 => (λ x (λ x (add (add four) x) x)
 => (λ x (λ x (λ m. λ n. λ f. λ x((((m next) n) f) x)add )four) x) x)
 => (λ x (λ x (λ n. λ f. λ x(((add next)n)f)x)four)x)x)
 => (λ x (λ x (λ f. λ x((add next)four)f)x)x)x) 
 => (λ x (λ x (λ f. λ x((λ m. λ n. λ f. λ x((((m next) n) f) x)next)four)f)x)x)x)
 => (λ x (λ x (λ f. λ x((λ n. λ f. λ x.(((next next)n)f)x)four)f)x)x)x)
 => (λ x (λ x (λ f. λ x((λ f. λ x ((next next)four)f)x)f)x)x)x)
 => (λ x (λ x (λ f. λ x((λ f. λ x(((λ n. λ f. λ x.(f ((n f) x))next)four)f)x)f)x)x)x)

Теперь, уменьшив вышеприведенное выражение и подставив вместо 'next' и 'four' и дополнительно уменьшив, мы получим следующую форму

λ f. λ x.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))) 

то есть шестнадцать.

Answer 1

Прежде всего, переписать next = λ n. λ f. λ x.(f ((n f) x)) как

next = λ num. λ succ. λ zero. succ (num succ zero)

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

Как нам читать выше? Это лямбда-термин. Когда это применяется к некоторому другому лямбда-термину, скажем NUM, это приведет к лямбда-термину λ succ. λ zero. succ (NUM succ zero), Это будет непосредственный результат, представление следующего числа данного числа, представленного NUM, Мы можем прочитать это как сказать нам: "Я не знаю, как рассчитать преемника или что значит быть нулем, но если оба будут предоставлены мне, я получу некоторый результат в соответствии с ними, и в соответствии с лямбда-термы NUM который был использован для создания меня, предоставляя эти средства расчета NUM а затем снова применить его результат к функции-преемнику, как мне дано ".

Это, конечно, предполагало, что NUM уважает те же самые предположения и работает последовательными способами. Особенно, ZERO применительно к s и z должен вернуться z:

ZERO = λ s. λ z. z  ; == λ a. λ b. b == ...

Все остальное вытекает из этого.