Page 1 of 1

Church encoding

Posted: Sun Jul 21, 2019 2:59 pm
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 :-)

Re: Church encoding

Posted: Mon Jul 22, 2019 10:13 am
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.

Re: Church encoding

Posted: Mon Jul 22, 2019 10:21 am
by cameyo
@kosh: thanks. I'll study it as soon as possible.