church.lpro

% Combinators

I := x. x
K := x. y. x
K* := x. y. y
S := x. y. z. (x z) (y z)
w := x. x x
W := w w
Y := f. (x. f (x x)) (x. f (x x))

% Booleans

tt = K
ff = K*

? = I
& := p. q. p q ff
V := p. p tt
! := p. p ff tt

% Numerals

c0 := f. x. x
succ := n. f. x. f (n f x)
c1 = succ c0
c2 = succ c1
c3 = succ c2
c4 = succ c3
c5 = succ c4
c6 = succ c5
c7 = succ c6
c8 = succ c7
c9 = succ c8
+ := m. n. m succ n
* := m. n. m (+ n) c0
^ := m. n. n m
^^ := m. n. n (^ m) c1

zero? := n. n (& ff) tt
even? := n. n ! tt
odd? := n. n ! ff

% Pairs

<> := x. y. z. z x y

left = p. p K
right = p. p K*

% Lists

nil := v. f. v
cons := x. xs. v. f. f x (xs v f)

head = xs. xs bottom K
tail = xs. xs bottom K*

append := xs. ys. xs ys cons
foldr := v. f. xs. xs v f
map := f. xs. xs nil (x. ys. cons (f x) ys)
filter := p. xs. xs nil (x. xs. ? (p x) (cons x xs) xs)
length := xs. xs c0 (K (+ c1))
empty? := xs. z? (length xs)


% More numerals

pred := n. right (n (p. <> (succl p) (left p)) (<> c0 c0))
fact := n. right (n (p. <> (succl p) (* (succl p) (right p))) (<> c0 c1))
succl := p. succ (left p)
fib := n. left (n (p. <> (right p) (p +)) (<> c0 c1))