Church encoding

Q&A's, tips, howto's
Post Reply
cameyo
Posts: 101
Joined: Sun Mar 27, 2011 3:07 pm

Church encoding

Post by cameyo »

In the Church encoding of natural numbers, the number N is encoded by a function that applies its first argument N times to its second argument.
Church zero always returns the identity function, regardless of its first argument. In other words, the first argument is not applied to the second argument at all.
Church one applies its first argument f just once to its second argument x, yielding f(x)
Church two applies its first argument f twice to its second argument x, yielding f(f(x))
and each successive Church numeral applies its first argument one additional time to its second argument, f(f(f(x))), f(f(f(f(x)))) ... The Church numeral 4, for example, returns a quadruple composition of the function supplied as its first argument.
Arithmetic operations on natural numbers can be similarly represented as functions on Church numerals.
I have written the following functions:

Code: Select all

(define (zero f x) x)
(define (uno f x) (f x))
(define (due f x) (f (f x)))
(define (tre f x) (f (f (f x))))
(define (quattro f x) (f (f (f (f x)))))
(define (cinque f x) (f (f (f (f (f x))))))
(define (sei f x) (f (f (f (f (f (f x)))))))
(define (sette f x) (f (f (f (f (f (f (f x))))))))
(define (otto f x) (f (f (f (f (f (f (f (f x)))))))))
(define (nove f x) (f (f (f (f (f (f (f (f (f x))))))))))
(zero inc 0)
;-> 0
(uno inc 0)
;-> 1
(due inc 0)
;-> 2
Or:

Code: Select all

(setq f inc)
(setq x 0)
(zero f x)
;-> 0
(sei f x)
;-> 6
I have defined the successor function:

Code: Select all

(define (succ n f x) (f (f n x)))
(succ 0 inc 0)
;-> 1
(succ 3 inc 0)
;-> 4
(succ 2 inc 0)
;-> 3
Now the plus operation:

Code: Select all

(define (plus m n f x) (f m (f n x)))
(plus 3 2 inc 0)
;-> 5
(plus (due inc 0) 5 inc 0)
;-> 7
(plus (due f x) 5 f x)
;-> 7
Now, i have some problem to write the following function:
1) multiplication (mult)
2) predecessor (pred)
3) subtraction (minus)

Can anyone help me?
cameyo

p.s. I'm not sure if what I wrote is correct
p.p.s. I forgot to translate the numbers into English :-)

kosh
Posts: 69
Joined: Sun Sep 13, 2009 5:38 am
Location: Japan
Contact:

Re: Church encoding

Post by kosh »

lambda.lsp: https://gist.github.com/kosh04/262332

This is my newlisp snippet (Incomplete & Comments are written in japanese).
It may be useful something.

cameyo
Posts: 101
Joined: Sun Mar 27, 2011 3:07 pm

Re: Church encoding

Post by cameyo »

@kosh: thanks. I'll study it as soon as possible.

Post Reply