Define the binary exponential operator CARAT in Lambda Calculus

Question

I am trying to define binary exponential operator in lambda calculus say operator CARAT. For example, this operator may take two arguments, the lambda encoding of number 2 and the lambda encoding of number 4, and computes the lambda encoding of number 16. I don't my answer is right or wrong but It took a day for me to do so. I have used church numerals definition.

Here is my answer. Please correct me if my answer is wrong. I don't how to do it exactly in a right way. If someone knows then please help me to figure out short answer.

A successor function, next, which adds one, can define the natural numbers in terms of zero and next:

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

From the above conclusion, we can define the function next as follows:

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)

Thus, we can safely prove that….

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

Addition is just an iteration of successor. We are now in a position to define addition in terms of next:

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)

After substituting values for ‘next’ and subsequently ‘two’, we can further reduce the above form to

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

i.e. four.

Similarly, Multiplication is an iteration of addition. Thus, Multiplication is defined as follows:

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)

After substituting values for ‘three’, ‘next’ and subsequently ‘add’ and then again for ‘next’, the above form will reduce to

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

i.e. six.

Finally, exponentiation can be defined by iterated multiplication

Assume exponentiation function to be called 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)

Now, reducing the above expression and substituting for ‘next’ and ‘four’ and further reducing, we get the following form

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

i.e. sixteen.

Answer 1

First of all, re-write next = λ n. λ f. λ x.(f ((n f) x)) as

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

In lambda-calculus parentheses are used just for grouping; an application is signified by juxtaposition of terms, i.e. just by writing one term next to another, and associates to the left.

How are we to read the above? It's a lambda term. When it is applied to some other lambda term, say NUM, it will reduce to a lambda term λ succ. λ zero. succ (NUM succ zero). This will be the immediate result, a representation of the next number of a given number represented by NUM. We can read it as saying to us, "I don't know how to calculate the successor, or what it means to be a zero, but if both are supplied to me I will produce some result according to them, and according to the lambda-term NUM that was used to create me, by supplying those means of calculation to NUM and then applying its result again to the successor function as given to me".

This of course was assuming that NUM respects same assumptions and operates in consistent ways. In particular, ZERO, when applied to an s and a z, must return z:

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

Everything else follows from this.