Scott numeral

A Scott numeral is a natural number encoded into lambda calculus using Mogensen–Scott encoding. In contrast to the better-known Church numerals, Scott numerals have a different performance profile and can be a better choice for certain applications.

Definition

Scott numerals have the following wikipedia:System F type signature:

ΛX. (ΛR. (X → R) → (R → R)) → (X → X)

Intuitively, Scott encoding provides one input argument per constructor of the equivalent data type. This signature is the encoding of the recursive type:

data Nat = Succ Nat | Zero

If the numeral is a zero, then it can return the identity function; otherwise, it can pass another Scott numeral to the successor function. The caller chooses the type X where the zeros and other concrete natural numbers are interpreted; the numeral chooses the type R where the successor operation is performed, including the common choice R = X for purely numeric behavior.

Examples

numbers

0 = λs.λz.z
1 = λs.λz.s 0 = λs.λz.s (λs.λz.z)
2 = λs.λz.s 1 = λs.λz.s (λs.λz.s (λs.λz.z))

successor function and predecessor function

succ = λn.λs.λz.s n
pred = λn.n (λx.x) 0

Arithmetic

First,we need a fixed point combinator

fix = (λx.x x)(λf.λx.x(f f x))

additive function

add = fix (λf.λx.λy.y (λn.succ (f x n)) x)

subtraction function

sub = fix (λf.λx.λy.y (λn.pred (f x n)) x)

multiplication function

mul = fix (λf.λx.λy.y (λn.add x (f x n)) 0)

division function

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

Predicate

First,we need boolean.

true = λt.λf.t
false = λt.λf.f

test if a number is zero

isZero = λn.n (λx.false) true

test if a number is less than or equal to another number

leq = λx.λy.isZero (sub x y)

test if a number is equal to another number

eq = λx.λy.(leq x y) (leq y x) false

test if a number is less than another number

lt = λx.λy.(eq x y) false (leq x y)

test if a number is even

even = λn.isZero (sub n (mul 2 (div n 2)))

Convert between Church numeral

First,we need church succ and church pred.

cSucc = λn.λs.λz.s(n s z)
cPred = λn.(n (λp.λx.x (p false) (succ (p false))) (λx.x 0 0)) true

convert to church numeral

toChurch = fix (λf.λx.x (λn.cSucc (f n)) (λs.λz.z))

convert from church numeral

fromChurch = λn.n succ 0