-
-
-
-
-
-(list?)
-nil
-cons
-nil?, (pair?)
-head
-tail
-
-Chris's lists:
- nil = (t,N) = \f. f true N
- [a] = (f,(a,nil))
- [b,a] = (f,(b,[a]))
-
-isnil = get-first
-head = L get-second get-first
-tail = L get-second get-second
-
-
-
-Lists 2:
- nil = false
- [a] = (a,nil)
-
-L (\h\t.K deal_with_h_and_t) if-nil
-
-We've already seen enumerations: true | false, red | green | blue
-What if you want one or more of the elements to have associated data? e.g. red | green | blue <how-blue>
-
-could handle like this:
- the-value if-red if-green (\n. handler-if-blue-to-degree-n)
-
- then red = \r \g \b-handler. r
- green = \r \g \b-handler. g
- make-blue = \degree. \r \g \b-handler. b-handler degree
-
-A list is basically: empty | non-empty <head,tail>
-
- empty = \non-empty-handler \if-empty. if-empty = false
- cons = \h \t. \non-empty-handler \if-empty. non-empty-handler h t
-
- so [a] = cons a empty = \non-empty-handler \_. non-empty-handler a empty
-
-
-
-Lists 3:
-[a; tl] isnil == (\f. f a tl) (\h \t.false) a b ~~> false a b
-
-nil isnil == (\f. M) (\h \t. false) a b ~~> M[f:=isnil] a b == a
-
- so M could be \a \b. a, i.e. true
- so nil = \f. true == K true == K K = \_ K
-
- nil = K true
- [a] = (a,nil)
- [b,a] = (b,[a])
-
-isnil = (\x\y.false)
-
-nil tail = K true tail = true = \x\y.x = \f.f? such that f? = Kx. there is no such.
-nil head = K true head = true. could mislead.
-
-
-
-Church figured out how to encode integers and arithmetic operations
-using lambda terms. Here are the basics:
-
-0 = \f\x.fx
-1 = \f\x.f(fx)
-2 = \f\x.f(f(fx))
-3 = \f\x.f(f(f(fx)))
-...
-
-Adding two integers involves applying a special function + such that
-(+ 1) 2 = 3. Here is a term that works for +:
-
-+ = \m\n\f\x.m(f((n f) x))
-
-So (+ 0) 0 =
-(((\m\n\f\x.m(f((n f) x))) ;+
- \f\x.fx) ;0
- \f\x.fx) ;0
-
-~~>_beta targeting m for beta conversion
-
-((\n\f\x.[\f\x.fx](f((n f) x)))
- \f\x.fx)
-
-\f\x.[\f\x.fx](f(([\f\x.fx] f) x))
-
-\f\x.[\f\x.fx](f(fx))
-
-\f\x.\x.[f(fx)]x
-
-\f\x.f(fx)
-
-
-
-
-
-
-
-
-
-let t = <<fun y _ -> y>>
-let f = <<fun _ n -> n>>
-let b = <<fun f g x -> f (g x)>>
-let k = << $t$ >>
-let get1 = << $t$ >>
-let get2 = << $f$ >>
-let id = <<fun x -> x>>
-let w = <<fun f -> f f>>
-let w' = <<fun f n -> f f n>>
-let pair = <<fun x y theta -> theta x y>>
-
-let zero = <<fun s z -> z>>
-let succ = <<fun n s z -> s (n s z)>>
-let one = << $succ$ $zero$ >>
-let two = << $succ$ $one$ >>
-let three = << $succ$ $two$ >>
-let four = << $succ$ $three$ >>
-let five = << $succ$ $four$ >>
-let six = << $succ$ $five$ >>
-let seven = << $succ$ $six$ >>
-let eight = << $succ$ $seven$ >>
-let nine = << $succ$ $eight$ >>
-
-(*
-let pred = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) $id$ >>
-*)
-let pred = <<fun n s z -> n (fun u v -> v (u s)) ($k$ z) $id$ >>
-(* ifzero n withp whenz *)
-let ifzero = <<fun n -> n (fun u v -> v (u $succ$)) ($k$ $zero$) (fun n' withp
-whenz -> withp n') >>
-
-let pred' =
- let iszero = << fun n -> n (fun _ -> $f$) $t$ >> in
- << fun n -> n ( fun f z' -> $iszero$ (f $one$) z' ($succ$ (f z')) ) ($k$ $zero$) $zero$ >>
-
-(*
- so n = zero ==> (k zero) zero
- n = one ==> f=(k zero) z'=zero ==> z' i.e. zero
- n = two ==> g(g (k zero)) zero
- f = g(k zero) z'=zero
- f = fun z'->z' z'=zero ==> succ (f z') = succ(zero)
- n = three ==> g(g(g (k zero))) zero
- f = g(g(k zero)) z'=zero
- f = fun z' -> succ(i z') z'=zero
- ==> succ (f z') ==> succ(succ(z'))
-*)
-
-let pred'' =
- let shift = (* <n,_> -> <n+1,n> *)
- <<fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) d1) >> in
- <<fun n -> n $shift$ ($pair$ $zero$ $zero$) $get2$ >>
-
-
-
-let add = <<fun m n -> n $succ$ m>>
-(* let add = <<fun m n -> fun s z -> m s (n s z) >> *)
-let mul = << fun m n -> n (fun z' -> $add$ m z') $zero$ >>
-
-
-(* we create a pairs-list of the numbers up to m, and take the
- * head of the nth tail. the tails are in the form (k tail), with
- * the tail of mzero being instead (id). We unwrap the content by:
- * (k tail) tail_of_mzero
- * or
- * (id) tail_of_mzero
- * we let tail_of_mzero be the mzero itself, so the nth predecessor of
- * zero will still be zero.
- *)
-
-let sub =
- let mzero = << $pair$ $zero$ $id$ >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ >>
-
-let min' = <<fun m n -> $sub$ m ($sub$ m n) >>
-let max' = <<fun m n -> $add$ n ($sub$ m n) >>
-
-let lt' =
- let mzero = << $pair$ $zero$ $id$ >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun n m -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $t$) $f$ >>
-
-let leq' =
- let mzero = << $pair$ $zero$ $id$ >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $f$) $t$ >>
-
-let eq' =
- (* like leq, but now we make mzero have a self-referential tail *)
- let mzero = << $pair$ $zero$ ($k$ ($pair$ $one$ $id$)) >> in
- let msucc = << fun d -> d (fun d1 _ -> $pair$ ($succ$ d1) ($k$ d)) >> in
- let mtail = << fun d -> d $get2$ d >> in (* or could use d $get2$ $mzero$ *)
- <<fun m n -> n $mtail$ (m $msucc$ $mzero$) $get1$ (fun _ -> $f$) $t$ >>
-
-(*
-let divmod' = << fun n d -> n
- (fun f' -> f' (fun d' m' ->
- $lt'$ ($succ$ m') d ($pair$ d' ($succ$ m')) ($pair$ ($succ$ d') $zero$)
- ))
- ($pair$ $zero$ $zero$) >>
-let div' = <<fun n d -> $divmod'$ n d $get1$ >>
-let mod' = <<fun n d -> $divmod'$ n d $get2$ >>
-*)
-
-let divmod' =
- let triple = << fun d1 d2 d3 -> fun sel -> sel d1 d2 d3 >> in
- let mzero = << $triple$ $succ$ ($k$ $zero$) $id$ >> in
- let msucc = << fun d -> $triple$ $id$ $succ$ ($k$ d) >> in
- let mtail = (* open in dhead *)
- << fun d -> d (fun dz mz df mf drest ->
- fun sel -> (drest dhead) (sel (df dz) (mf mz))) >> in
- << fun n divisor ->
- ( fun dhead -> n $mtail$ (fun sel -> dhead (sel $zero$ $zero$)) )
- (divisor $msucc$ $mzero$ (fun _ _ d3 -> d3 _))
- (fun dz mz _ _ _ -> $pair$ dz mz) >>
-
-let div' = <<fun n d -> $divmod'$ n d $get1$ >>
-let mod' = <<fun n d -> $divmod'$ n d $get2$ >>
-
-(*
- ISZERO = lambda n. n (lambda x. false) true,
-
- LE = lambda x. lambda y. ISZERO (MONUS x y),
- { ? x <= y ? }
-
- MONUS = lambda a. lambda b. b PRED a,
- {NB. assumes a >= b >= 0}
-
- DIVMOD = lambda x. lambda y.
- let rec dm = lambda q. lambda x.
- if LE y x then {y <= x}
- dm (SUCC q) (MONUS x y)
- else pair q x
- in dm ZERO x,
-*)
-
-(* f n =def. phi n_prev f_prev *)
-let bernays = <<fun phi z n -> n (fun d -> $pair$ (d (fun n_prev f_prev -> $succ$ n_prev)) (d phi)) ($pair$ $zero$ z) (fun n f -> f)>>
-
-
-(*
-let pred_b = << $bernays$ $k$ $zero$ >>
-let fact_b = << $bernays$ (fun x p -> $mul$ ($succ$ x) p) $one$ >>
-
-(* if m is zero, returns z; else returns withp (pred m) *)
-let ifzero = <<fun z withp m -> $bernays$ (fun x p -> withp x) z m>>
-let ifzero = <<fun z withp m -> m ($k$ (withp ($pred$ m))) z>>
-*)
-
-let y = <<fun f -> (fun u -> f (u u)) (fun u -> f (u u))>>
-(* strict y-combinator from The Little Schemer, Crockford's http://www.crockford.com/javascript/little.html *)
-let y' = <<fun f -> (fun u -> f (fun n -> u u n)) (fun u -> f (fun n -> u u n))>>
-(*
-let y'' = <<fun f -> (fun u n -> f (u u n)) (fun u n -> f (u u n))>>
-*)
-
-let turing = <<(fun u f -> f (u u f)) (fun u f -> f (u u f))>>
-let turing' = <<(fun u f -> f (fun n -> u u f n)) (fun u f -> f (fun n -> u u f n))>>
-
-
-let fact_w = << $w$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f f
-p)) $one$)>>
-let fact_w' = <<(fun f n -> f f n) (fun f n -> $ifzero$ n (fun p ->
- $mul$ n (f f p)) $one$)>>
-let fact_w'' = let u = <<(fun f n -> $ifzero$ n (fun p -> $mul$ n (f f
-p)) $one$)>> in <<fun n -> $u$ $u$ n>>
-
-let fact_y = << $y$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-let fact_y' = << $y'$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-
-let fact_turing = << $turing$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-let fact_turing' = << $turing'$ (fun f n -> $ifzero$ n (fun p -> $mul$ n (f p)) $one$)>>
-
-
-
-let zero_ = <<fun s z -> z>>;;
-let succ_ = <<fun m s z -> s m (m s z)>>;;
-let one_ = << $succ_$ $zero_$ >>;;
-let two_ = << $succ_$ $one_$ >>;;
-let three_ = << $succ_$ $two_$ >>;;
-let four_ = << $succ_$ $three_$ >>;;
-let five_ = << $succ_$ $four_$ >>;;
-let six_ = << $succ_$ $five_$ >>;;
-let seven_ = << $succ_$ $six_$ >>;;
-let eight_ = << $succ_$ $seven_$ >>;;
-let nine_ = << $succ_$ $eight_$ >>;;
-
-let pred_ = <<fun n -> n (fun n' _ -> n') $zero_$ >>
-let add_ = <<fun m n -> n (fun _ f' -> $succ_$ f') m>>
-let mul_ = <<fun m n -> n (fun _ f' -> $add_$ m f') $zero_$ >>
-(* let pow_ = *)
-
-let sub_ = <<fun m n -> n (fun _ f' -> $pred_$ f') m>>
-let min_ = <<fun m n -> $sub_$ m ($sub_$ m n)>> (* m-max(m-n,0) = m+min(n-m,0) = min(n,m) *)
-let max_ = <<fun m n -> $add_$ n ($sub_$ m n)>> (* n+max(m-n,0) = max(m,n) *)
-
-let eq_ = <<fun m -> m (fun _ fm' n -> n (fun n' _ -> fm' n') $f$) (fun n -> n (fun _ _ -> $f$) $t$)>>
-let lt_ = <<fun m n -> ($sub_$ n m) (fun _ _ -> $t$) $f$ >>
-let leq_ = << fun m n -> ($sub_$ m n) (fun _ _ -> $f$) $t$ >>
-
-let divmod_ = << fun n d -> n
- (fun _ f' -> f' (fun d' m' ->
- $lt_$ ($succ_$ m') d ($pair$ d' ($succ_$ m')) ($pair$ ($succ_$ d') $zero_$)
- ))
- ($pair$ $zero_$ $zero_$) >>
-let div_ = <<fun n d -> $divmod_$ n d $get1$ >>
-let mod_ = <<fun n d -> $divmod_$ n d $get2$ >>
-