# Scott Numerals as per March 8, 2006 revision of John Tromp's 
# paper, "Binary Lambda Calculus and Combinatory Logic".
# "The Scott Numerals [i] can be used to define arithmetic, as
# well as for indexing lists; M [i] select's the i'th element
# of a sequence M."
# $Id: scott.numerals,v 1.1 2011/11/18 23:39:52 bediger Exp $

eta on

define succ %c.%d.%e.(e c)
define case %f.%g.%h.f g h
define pred %i.(i (%j.%k.j) (%l.l))

def True \x.\y.x
def False \x.\y.y

def nil False
def sn0 True
def sn{*} *succ sn0  # Not in beta-normal form

# check pairing operator
define pair (\p.\q.\z.z p q)
normalize (pair true false) True == true
normalize (pair true false) False == false

# define a list, check that each incrementally composed Scott numeral works
def list (normalize (pair _zero (pair _one (pair _two (pair _three (pair _four (pair _five (pair _six nil))))))))

check_incremental_scott_numerals
normalize list sn0 == _zero
normalize list sn{1} == _one
normalize list sn{2} == _two
normalize list sn{3} == _three
normalize list sn{4} == _four
normalize list sn{5} == _five
normalize list sn{6} == _six

def Y (\x.\y.x y x)(\y.\x. y(x y x))
define R (\o.\n.\m.( case m n (o (succ n)) ))
define add (Y R)

check_added_scott_numerals
normalize list (add sn0 sn0) == _zero
normalize list (add sn0 sn{1}) == _one
normalize list (add sn{1} sn0) == _one
normalize list (add sn{1} sn{1}) == _two
normalize list (add sn{2} sn{1}) == _three
normalize list (add sn{1} sn{2}) == _three
normalize list (add sn{2} sn{2}) == _four
normalize list (add sn{2} sn{3}) == _five
normalize list (add sn{3} sn{3}) == _six
normalize list (add (add sn{2} sn{1}) (add sn{1} sn{2})) == _six