Определить бинарный экспоненциальный оператор CARAT.in lambda calculus CARAT

Question

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

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

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)))) 

т.е. 4.

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

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) 

Теперь, снижающую выше выражение и заменяющий «рядом» и «четыре» и дальнейшее сокращение , мы получаем следующий вид:

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

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

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 == ... 

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