double =
fix (lambda f : Nat -> Nat. lambda n : Nat.
if iszero n then
0
else
succ (succ (f (pred n))));
/* Basic binary arithmetic */
ZPNat = Rec X. ;
zpone = as ZPNat;
zpx0 = lambda n : ZPNat. as ZPNat;
zpx1 = lambda n : ZPNat. as ZPNat;
zptwo = zpx0 zpone;
zpthree = zpx1 zpone;
natzp =
fix (lambda f : ZPNat -> Nat. lambda n : ZPNat.
case n of
==> 1
| ==> double (f p)
| ==> succ (double (f p)));
zpsucc = fix (lambda f : ZPNat -> ZPNat. lambda n : ZPNat.
case n of
==> zptwo
| ==> as ZPNat
| ==> as ZPNat);
zpdm1 = fix (lambda f : ZPNat -> ZPNat. lambda n : ZPNat.
case n of
==> as ZPNat
| ==> as ZPNat
| ==> as ZPNat);
zppluscp =
fix (lambda f : ZPNat -> {p : ZPNat -> ZPNat, c : ZPNat -> ZPNat}.
lambda n : ZPNat.
case n of
==> {p = lambda m : ZPNat.
case m of
==> as ZPNat
| ==> as ZPNat
| ==> zptwo,
c = lambda m : ZPNat.
case m of
==> as ZPNat
| ==> as ZPNat
| ==> zpthree}
| ==> {p = lambda m : ZPNat.
case m of
==> as ZPNat
| ==> as ZPNat
| ==> as ZPNat,
c = lambda m : ZPNat.
case m of
==> as ZPNat
| ==> as ZPNat
| ==> as ZPNat}
| ==> {p = lambda m : ZPNat.
case m of
==> as ZPNat
| ==> as ZPNat
| ==> as ZPNat,
c = lambda m : ZPNat.
case m of
==> as ZPNat
| ==> as ZPNat
| ==> as ZPNat});
zpplus = lambda n : ZPNat. (zppluscp n).p;
ZNat = ;
zzero = as ZNat;
zone = as ZNat;
ztwo = as ZNat;
zthree = as ZNat;
ziszero =
lambda n : ZNat.
case n of
==> true
| ==> false;
zsucc =
lambda n : ZNat.
case n of
==> zone
| ==> as ZNat;
znat =
fix (lambda f : Nat -> ZNat. lambda n : Nat.
if iszero n then
zzero
else
zsucc (f (pred n)));
natz =
lambda n : ZNat.
case n of
==> 0
| ==> natzp p;
zplus =
lambda n : ZNat. lambda m : ZNat.
case n of
==> m
| ==> (case m of
==> n
| ==> as ZNat);
ZInt = ;
zix0 =
lambda n : ZInt.
case n of
==> as ZInt
| ==> as ZPNat> as ZInt
| ==> as ZPNat> as ZInt;
zix1 =
lambda n : ZInt.
case n of
==> as ZInt
| ==> as ZPNat> as ZInt
| ==> as ZPNat> as ZInt;
zidm2 =
lambda n : ZPNat.
case n of
==> as ZInt
| ==> as ZPNat> as ZInt
| ==> as ZPNat> as ZPNat> as ZInt;
zpminuscp =
fix (lambda f : ZPNat -> {m : ZPNat -> ZInt, c : ZPNat -> ZInt}.
lambda n : ZPNat.
case n of
==> {m = lambda m : ZPNat.
case m of
==> as ZInt
| ==> as ZInt
| ==> as ZInt,
c = lambda m : ZPNat.
case m of
==> as ZInt
| ==> as ZInt
| ==> as ZInt}
| ==> {m = lambda m : ZPNat.
case m of
==> zix1 ((f np).c mp)
| ==> zix0 ((f np).m mp)
| ==> as ZInt,
c = lambda m : ZPNat.
case m of
==> zix0 ((f np).c mp)
| ==> zix1 ((f np).c mp)
| ==> zidm2 np}
| ==> {m = lambda m : ZPNat.
case m of
==> zix0 ((f np).m mp)
| ==> zix1 ((f np).m mp)
| ==> as ZInt,
c = lambda m : ZPNat.
case m of
==> zix1 ((f np).c mp)
| ==> zix0 ((f np).m mp)
| ==> as ZInt});
zpminus = lambda n : ZPNat. (zpminuscp n).m;
zpmask = lambda n : ZNat.
case n of
==> as ZInt
| ==> as ZInt;
znmask = lambda n : ZNat.
case n of
==> as ZInt
| ==> as ZInt;
zminus = lambda n : ZNat. lambda m : ZNat.
case n of
==> znmask m
| ==> (case m of
==> zpmask n
| ==> zpminus np mp);
zdivides =
lambda m : ZNat.
fix (lambda f : ZNat -> Bool. lambda n : ZNat.
case zminus n m of
==> true
| ==> f ( as ZNat)
| ==> ziszero n);
/* Lists */
NatList = Rec X. ;
nil = as NatList;
cons =
lambda h : Nat. lambda t : NatList.
as NatList;
/* Streams */
ZNatStream = Rec X. Unit -> {hd : ZNat, tl : X};
ZNatStreamCell = {hd : ZNat, tl : ZNatStream};
/* Stream to list */
take =
fix (lambda f : Nat -> ZNatStream -> NatList.
lambda n : Nat. lambda s : ZNatStream.
if iszero n then
nil
else
let c = s unit in
cons (natz c.hd) (f (pred n) c.tl));
/* Sieve of Eratosthenes */
nats =
fix (lambda f : ZNat -> ZNatStream. lambda n : ZNat.
lambda u : Unit. {hd = n, tl = f (zsucc n)});
filter =
lambda p : ZNat.
fix (lambda f : ZNatStream -> ZNatStream. lambda s : ZNatStream.
lambda u : Unit.
let c = s unit in
if zdivides p c.hd then
f c.tl unit
else
{hd = c.hd, tl = f c.tl});
sieve =
fix (lambda f : ZNatStream -> ZNatStream. lambda s : ZNatStream.
lambda u : Unit.
let c = s unit in
{hd = c.hd, tl = f (filter c.hd c.tl)});
primes = sieve (nats ztwo);
take 25 primes;