Parigot numeral

A Parigot numeral is a natural number encoded into lambda calculus using Parigot encoding. One way to understand Parigot numerals is by relation with Church numerals, considering primitive recursion and recursion schemes; if Church numerals are like initial katamorphisms for the natural numbers, then Parigot numerals are like initial paramorphisms, with access to the numeral at each stage of recursion.

The Parigot numerals can be recursively defined by:

0 g h = h
(succ n) g h = g n (n g h)

and letting R(g,h) be a primitive recursive function with one parameter, then

R(g,h)(0) = h()
R(g,h)(S(xn)) = g(xn,(R(g,h)(xn)))

It can be observed that R is equivalent to the Parigot numeral λg.λh.λn.n g h.

Examples

numbers

0 = λg.λh.h
1 = λg.λh.g 0 h
2 = λg.λh.g 1 (g 0 h)
3 = λg.λh.g 2 (g 1 (g 0 h))
(numbers require exponential space)

successor function and predecessor function

succ = λn.λg.λh.g n (n g h)
pred = λn.n (λa.λb.a) 0

Arithmetic

additive function

add = λx.λy.y (λa.λb.succ b) x

subtraction function

sub = λx.λy.y (λa.λb.pred b) x

multiplication function

mul = λx.λy.y (λa.λb.add x b) 0

division function

fix = (λx.x x)(λf.λx.x (f f x))
div = fix (λf.λx.λy.(succ (sub x y))(λa.λb.succ (f (sub x y) y)) 0)

(or use the minimalization)

Mu = (λx.x x 0)(λmu.λx.λf.(f x)(λa.λb.f f (succ x)) x)
div = λx.λy.Mu (λn.(pred (sub (mul (succ n) y) x))(λa.λb.0) 1)

convert between Church numeral

First,we need church succ

cSucc = λn.λs.λz.s (n s z)

convert to church numeral

toChurch = λn.n (λa.λb.cSucc b)(λs.λz.z)

convert from church numeral

fromChurch = λn.n succ 0