Church encoding

Started by cameyo, July 21, 2019, 07:59:33 AM

Previous topic - Next topic

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:
(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:
(setq f inc)
(setq x 0)
(zero f x)
;-> 0
(sei f x)
;-> 6

I have defined the successor function:
(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:
(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

#1
lambda.lsp: https://gist.github.com/kosh04/262332">https://gist.github.com/kosh04/262332



This is my newlisp snippet (Incomplete & Comments are written in japanese).

It may be useful something.

cameyo

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