From 2025df5747686d386e61eaa0980a14835d8bf217 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Thu, 16 Sep 2010 20:57:15 -0400 Subject: [PATCH] tweak lists_and_numbers Signed-off-by: Jim Pryor --- lists_and_numbers.mdwn | 322 +------------------------------------------------ 1 file changed, 2 insertions(+), 320 deletions(-) diff --git a/lists_and_numbers.mdwn b/lists_and_numbers.mdwn index bde7c2f3..8175064f 100644 --- a/lists_and_numbers.mdwn +++ b/lists_and_numbers.mdwn @@ -295,8 +295,8 @@ Perhaps not as elegant as addition, but still decently principled. Multiplication is even more elegant. Consider that applying an arbitrary function s to a base value z *m × n* times is a matter of applying s to z *n* times, and then doing that again, and again, and so on...for *m* repetitions. In other words, it's a matter of applying the function (\z. n s z) to z *m* times. In other words, *m × n* can be represented as: -   \s z. m (\z. n s z) z - ~~> \s z. m n s z +
    \s z. m (\z. n s z) z
+~~> \s z. m n s z
which eta-reduces to: @@ -308,321 +308,3 @@ However, at this point the elegance gives out. The predecessor function is subst However, if on the other hand you do have some experience programming, consider how you might construct a predecessor function for numbers implemented in this way. Using only the resources we've so far discussed. (So you have no general facility for performing recursion, for instance.) - - - - - -(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 - -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 - - 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 = < y>> -let f = < n>> -let b = < f (g x)>> -let k = << $t$ >> -let get1 = << $t$ >> -let get2 = << $f$ >> -let id = < x>> -let w = < f f>> -let w' = < f f n>> -let pair = < theta x y>> - -let zero = < z>> -let succ = < 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 = < n (fun u v -> v (u $succ$)) ($k$ $zero$) $id$ >> -*) -let pred = < n (fun u v -> v (u s)) ($k$ z) $id$ >> -(* ifzero n withp whenz *) -let ifzero = < 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 = (* -> *) - < d (fun d1 _ -> $pair$ ($succ$ d1) d1) >> in - < n $shift$ ($pair$ $zero$ $zero$) $get2$ >> - - - -let add = < n $succ$ m>> -(* let add = < 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$ *) - < n $mtail$ (m $msucc$ $mzero$) $get1$ >> - -let min' = < $sub$ m ($sub$ m n) >> -let max' = < $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$ *) - < 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$ *) - < 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$ *) - < 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' = < $divmod'$ n d $get1$ >> -let mod' = < $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' = < $divmod'$ n d $get1$ >> -let mod' = < $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 = < 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 = < $bernays$ (fun x p -> withp x) z m>> -let ifzero = < m ($k$ (withp ($pred$ m))) z>> -*) - -let y = < (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 u -> f (fun n -> u u n)) (fun u -> f (fun n -> u u n))>> -(* -let y'' = < (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 < $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_ = < z>>;; -let succ_ = < 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_ = < n (fun n' _ -> n') $zero_$ >> -let add_ = < n (fun _ f' -> $succ_$ f') m>> -let mul_ = < n (fun _ f' -> $add_$ m f') $zero_$ >> -(* let pow_ = *) - -let sub_ = < n (fun _ f' -> $pred_$ f') m>> -let min_ = < $sub_$ m ($sub_$ m n)>> (* m-max(m-n,0) = m+min(n-m,0) = min(n,m) *) -let max_ = < $add_$ n ($sub_$ m n)>> (* n+max(m-n,0) = max(m,n) *) - -let eq_ = < m (fun _ fm' n -> n (fun n' _ -> fm' n') $f$) (fun n -> n (fun _ _ -> $f$) $t$)>> -let lt_ = < ($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_ = < $divmod_$ n d $get1$ >> -let mod_ = < $divmod_$ n d $get2$ >> - -- 2.11.0