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;