--- /dev/null
+Here are a bunch of pre-tested operations for the untyped lambda calculus. In some cases multiple versions are offered.
+
+ ; booleans
+ let true = \y n. y in ; aka K
+ let false = \y n. n in ; aka K I
+ let and = \p q. p q false in ; or
+ let and = \p q. p q p in ; aka S C I
+ let or = \p q. p true q in ; or
+ let or = \p q. p p q in ; aka M
+ let not = \p. p false true in ; or
+ let not = \p y n. p n y in ; aka C
+ let xor = \p q. p (not q) q in
+ let iff = \p q. not (xor p q) in ; or
+ let iff = \p q. p q (not q) in
+
+ ; pairs
+ let make_pair = \x y f. f x y in
+ let get_1st = \x y. x in ; aka true
+ let get_2nd = \x y. y in ; aka false
+
+ ; triples
+ let make_triple = \x y z f. f x y z in
+
+
+ ; Church numerals: basic operations
+
+ let zero = \s z. z in ; aka false
+ let one = \s z. s z in ; aka I
+ let succ = \n s z. s (n s z) in
+ ; for any Church numeral n > zero : n (K y) z ~~> y
+ let iszero = \n. n (\x. false) true in
+
+
+ ; version 3 lists
+
+ let empty = \f z. z in
+ let make_list = \h t f z. f h (t f z) in
+ let isempty = \lst. lst (\h sofar. false) true in
+ let head = \lst. lst (\h sofar. h) junk in
+ let tail_empty = empty in
+ let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_2nd)
+ ; where shift is
+ (\h p. p (\t y. make_pair (make_list h t) t)) in
+ let length = \lst. lst (\h sofar. succ sofar) 0 in
+ let map = \f lst. lst (\h sofar. make_list (f h) sofar) empty in
+ let filter = \f lst. lst (\h sofar. f h (make_list h sofar) sofar) empty in ; or
+ let filter = \f lst. lst (\h. f h (make_list h) I) empty in
+ let singleton = \x f z. f x z in
+ ; append [a;b;c] [x;y;z] ~~> [a;b;c;x;y;z]
+ let append = \left right. left make_list right in
+ ; very inefficient but correct reverse
+ let reverse = \lst. lst (\h sofar. append sofar (singleton h)) empty in ; or
+ ; more efficient reverse builds a left-fold instead
+ ; (make_left_list a (make_left_list b (make_left_list c empty)) ~~> \f z. f c (f b (f a z))
+ let reverse = (\make_left_list lst. lst make_left_list empty) (\h t f z. t f (f h z)) in
+ ; zip [a;b;c] [x; y; z] ~~> [(a,x);(b,y);(c,z)]
+ let zip = \left right. (\base build. reverse left build base (\x y. reverse x))
+ ; where base is
+ (make_pair empty (map (\h u. u h) right))
+ ; and build is
+ (\h sofar. sofar (\x y. isempty y
+ sofar
+ (make_pair (make_list (\u. head y (u h)) x) (tail y))
+ )) in
+ let all = \f lst. lst (\h sofar. and sofar (f h)) true in
+ let any = \f lst. lst (\h sofar. or sofar (f h)) false in
+
+
+ ; version 1 lists
+
+ let empty = make_pair true junk in
+ let make_list = \h t. make_pair false (make_pair h t) in
+ let isempty = \lst. lst get_1st in
+ let head = \lst. isempty lst err (lst get_2nd get_1st) in
+ let tail_empty = empty in
+ let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in
+
+
+ ; more math with Church numerals
+
+ let add = \m n. m succ n in ; or
+ let add = \m n s z. m s (n s z) in
+ let mul = \m n. m (\z. add n z) zero in ; or
+ let mul = \m n s. m (n s) in
+ let pow = \b exp. exp (mul b) one in ; or
+ ; b succ : adds b
+ ; b (b succ) ; adds b b times, ie adds b^2
+ ; b (b (b succ)) ; adds b^2 b times, ie adds b^3
+ ; exp b succ ; adds b^exp
+ let pow = \b exp s z. exp b s z in
+
+
+ ; three strategies for predecessor
+ let pred_zero = zero in
+ let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd)
+ ; where shift is
+ (\p. p (\x y. make_pair (succ x) x)) in ; or
+ ; from Oleg; observe that for any Church numeral n: n I ~~> I
+ let pred = \n. iszero n zero
+ ; else
+ (n (\x. x I ; when x is the base term, this will be K zero
+ ; when x is a Church numeral, it will be I
+ (succ x))
+ ; base term
+ (K (K zero))
+ ) in
+ ; from Bunder/Urbanek
+ let pred = \n s z. n (\u v. v (u s)) (K z) I in ; or
+
+
+ ; inefficient but simple comparisons
+ let leq = \m n. iszero (n pred m) in
+ let lt = \m n. not (leq n m) in
+ let eq = \m n. and (leq m n) (leq n m) in ; or
+
+
+ ; more efficient comparisons, Oleg's gt provided some simplifications
+ let leq = (\base build consume. \m n. n consume (m build base) get_1st)
+ ; where base is
+ (make_pair true junk)
+ ; and build is
+ (\p. make_pair false p)
+ ; and consume is
+ (\p. p get_1st p (p get_2nd)) in
+ let lt = \m n. not (leq n m) in
+ let eq = (\base build consume. \m n. n consume (m build base) get_1st)
+ ; 2nd element of a pair will now be of the form (K sthg) or I
+ ; we supply the pair being consumed itself as an argument
+ ; getting back either sthg or the pair we just consumed
+ ; base is
+ (make_pair true (K (make_pair false I)))
+ ; and build is
+ (\p. make_pair false (K p))
+ ; and consume is
+ (\p. p get_2nd p) in
+
+
+ ; -n is a fixedpoint of \x. add (add n x) x
+ ; but unfortunately Y that_function doesn't normalize
+ ; instead:
+ let sub = \m n. n pred m in ; or
+ ; how many times we can succ n until m <= result
+ let sub = \m n. (\base build. m build base (\cur fin sofar. sofar))
+ ; where base is
+ (make_triple n false zero)
+ ; and build is
+ (\t. t (\cur fin sofar. or fin (leq m cur)
+ (make_triple cur true sofar) ; enough
+ (make_triple (succ cur) false (succ sofar)) ; continue
+ )) in
+ ; or
+ let sub = (\base build consume. \m n. n consume (m build base) get_1st)
+ ; where base is
+ (make_pair zero I) ; see second defn of eq for explanation of 2nd element
+ ; and build is
+ (\p. p (\x y. make_pair (succ x) (K p)))
+ ; and consume is
+ (\p. p get_2nd p) in
+
+
+ let min = \m n. sub m (sub m n) in
+ let max = \m n. add n (sub m n) in
+
+
+ ; (m/n) is a fixedpoint of \x. add (sub (mul n x) m) x
+ ; but unfortunately Y that_function doesn't normalize
+ ; instead:
+ ; how many times we can sub n from m while n <= result
+ let div = \m n. (\base build. m build base (\cur go sofar. sofar))
+ ; where base is
+ (make_triple m true zero)
+ ; and build is
+ (\t. t (\cur go sofar. and go (leq n cur)
+ (make_triple (sub cur n) true (succ sofar)) ; continue
+ (make_triple cur false sofar) ; enough
+ )) in
+ ; what's left after sub n from m while n <= result
+ let mod = \m n. (\base build. m build base (\cur go. cur))
+ ; where base is
+ (make_pair m true)
+ ; and build is
+ (\p. p (\cur go. and go (leq n cur)
+ (make_pair (sub cur n) true) ; continue
+ (make_pair cur false) ; enough
+ )) in
+
+ ; or
+ let divmod = (\base build mtail. \m n.
+ (\dhead. m (mtail dhead) (\sel. dhead (sel 0 0)))
+ (n build base (\x y z. z junk))
+ (\t u x y z. make_pair t u) )
+ ; where base is
+ (make_triple succ (K 0) I) ; see second defn of eq for explanation of 3rd element
+ ; and build is
+ (\t. make_triple I succ (K t))
+ ; and mtail is
+ (\dhead d. d (\dz mz df mf drest sel. drest dhead (sel (df dz) (mf mz))))
+ in
+ let div = \n d. divmod n d get_1st in
+ let mod = \n d. divmod n d get_2nd in
+
+
+ ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x
+ ; but unfortunately Y that_function doesn't normalize
+
+
+ ; (log base b of m) is a fixedpoint of \x. add (sub (pow b x) m) x
+ ; but unfortunately Y that_function doesn't normalize
+ ; instead:
+ ; how many times we can mul b by b while result <= m
+ let log = \m b. (\base build. m build base (\cur go sofar. sofar))
+ ; where base is
+ (make_triple b true 0)
+ ; and build is
+ (\t. t (\cur go sofar. and go (leq cur m)
+ (make_triple (mul cur b) true (succ sofar)) ; continue
+ (make_triple cur false sofar) ; enough
+ )) in
+
+
+ ; Rosenbloom's fixed point combinator
+ let Y = \f. (\h. f (h h)) (\h. f (h h)) in
+ ; Turing's fixed point combinator
+ let Theta = (\u f. f (u u f)) (\u f. f (u u f)) in
+
+
+ ; length for version 1 lists
+ let length = Y (\self lst. isempty lst 0 (succ (self (tail lst)))) in
+
+
+ ; numhelper 0 f z ~~> z
+ ; when n > 0: numhelper n f z ~~> f (pred n)
+ ; compare Bunder/Urbanek pred
+ let numhelper = \n. n (\u v. v (u succ)) (K 0) (\p f z. f p) in
+
+ ; accepts fixed point combinator as a parameter, so you can use different ones
+ let fact = \y. y (\self n. numhelper n (\p. mul n (self p)) 1) in
+
+
+
+ fact Theta 3 ; returns 6
+
+
+<!--
+ ; my original efficient comparisons
+ let leq = (\base build consume. \m n. n consume (m build base) get_1st (\x. false) true)
+ ; where base is
+ (make_pair zero I) ; supplying this pair as an arg to its 2nd term returns the pair
+ ; and build is
+ (\p. p (\x y. make_pair (succ x) (K p))) ; supplying the made pair as an arg to its 2nd term returns p (the previous pair)
+ ; and consume is
+ (\p. p get_2nd p) in
+ let lt = \m n. not (leq n m) in
+ let eq = (\base build consume. \m n. n consume (m build base) true (\x. false) true)
+ ; where base is
+ (make_pair zero (K (make_pair one I)))
+ ; and build is
+ (\p. p (\x y. make_pair (succ x) (K p)))
+ ; and consume is
+ (\p. p get_2nd p) in ; or
+-->
+
+<!--
+ gcd
+ pow_mod
+
+
+ show Oleg's definition of integers:
+ church_to_int = \n sign. n
+ church_to_negint = \n sign s z. sign (n s z)
+
+ ; int_to_church
+ abs = \int. int I
+
+ sign_case = \int ifpos ifzero ifneg. int (K ifneg) (K ifpos) ifzero
+
+ negate_int = \int. sign_case int (church_to_negint (abs int)) zero (church_to_int (abs int))
+
+ for more, see http://okmij.org/ftp/Computation/lambda-arithm-neg.scm
+
+-->
Once again, the lambda evaluator will make working through this
assignment much faster and more secure.
-##Writing recursive functions on version 1 style lists##
+#Writing recursive functions on version 1 style lists#
-Recall that version 1 style lists are constructed like this:
+Recall that version 1 style lists are constructed like this (see
+[[lists and numbers]]):
<pre>
; booleans
let succ = \n s z. s (n s z) in
let mult = \m n s. m (n s) in
let length = Y (\length l. isNil l 0 (succ (length (tail l)))) in
-let predecessor = \n. length (tail (n (\p. makeList meh p) nil)) in
-let leq = ; (leq m n) will be true iff m is less than or equal to n
- Y (\leq m n. isZero m true (isZero n false (leq (predecessor m)(predecessor n)))) in
+let pred = \n. isZero n 0 (length (tail (n (\p. makeList meh p) nil)))
+in
+let leq = \m n. isZero(n pred m) in
let eq = \m n. and (leq m n)(leq n m) in
-eq 3 3
+eq 2 2 yes no
</pre>
Then `length mylist` evaluates to 3.
-1. Warm-up: What does `head (tail (tail mylist))` evaluate to?
+1. What does `head (tail (tail mylist))` evaluate to?
2. Using the `length` function as a model, and using the predecessor
function, write a function that computes factorials. (Recall that n!,
interpreter; web pages are not supposed to be that computationally
intensive).
-
-3. Write a function `listLenEq` that returns true just in case two lists have the
+3. (Easy) Write a function `listLenEq` that returns true just in case
+two lists have the
same length. That is,
- listLenEq mylist (makeList meh (makeList meh (makeList meh nil))) ~~> true
+ listLenEq mylist (makeList meh (makeList meh (makeList meh nil)))
+ ~~> true
listLenEq mylist (makeList meh (makeList meh nil))) ~~> false
-4. Now write the same function, but don't use the length function (hint: use `leq` as a model).
-##Trees##
+4. (Still easy) Now write the same function, but don't use the length
+function.
+
+5. In assignment 2, we discovered that version 3-type lists (the ones
+that
+work like Church numerals) made it much easier to define operations
+like `map` and `filter`. But now that we have recursion in our
+toolbox,
+reasonable map and filter functions for version 1 lists are within our
+reach. Give definitions for `map` and a `filter` for verson 1 type
+lists.
+
+#Computing with trees#
-Since we'll be working with linguistic objects, let's approximate
-trees as follows: a tree is a version 1 list
-a Church number is a tree, and
-if A and B are trees, then (make-pair A B) is a tree.
+Linguists analyze natural language expressions into trees.
+We'll need trees in future weeks, and tree structures provide good
+opportunities for learning how to write recursive functions.
+Making use of the resources we have at the moment, we can approximate
+trees as follows: instead of words, we'll use Church numerals.
+Then a tree will be a (version 1 type) list in which each element is
+itself a tree. For simplicity, we'll adopt the convention that
+a tree of length 1 must contain a number as its only element.
+Then we have the following representations:
+<pre>
+ (a) (b) (c)
+ .
+ /|\ /\ /\
+ / | \ /\ 3 1 /\
+ 1 2 3 1 2 2 3
+
+[[1];[2];[3]] [[[1];[2]];[3]] [[1];[[2];[3]]]
+</pre>
+Limitations of this scheme include the following: there is no easy way
+to label a constituent with a syntactic category (S or NP or VP,
+etc.), and there is no way to represent a tree in which a mother has a
+single daughter.
+When processing a tree, you can test for whether the tree contains
+only a numeral (in which case the tree is leaf node) by testing for
+whether the length of the list is less than or equal to 1. This will
+be your base case for your recursive functions that operate on these
+trees.
-[The following should be correct, but won't run in my browser:
+1. Write a function that sums the number of leaves in a tree.
-let factorial = Y (\fac n. isZero n 1 (mult n (fac (predecessor n)))) in
+Expected behavior:
<pre>
-let reverse =
- Y (\rev l. isNil l nil
- (isNil (tail l) l
- (makeList (head (rev (tail l)))
- (rev (makeList (head l)
- (rev (tail (rev (tail l))))))))) in
-
-reverse (makeList 1 (makeList 2 (makeList 3 nil)))
+let t1 = (makeList 1 nil) in
+let t2 = (makeList 2 nil) in
+let t3 = (makeList 3 nil) in
+let t12 = (makeList t1 (makeList t2 nil)) in
+let t23 = (makeList t2 (makeList t3 nil)) in
+let ta = (makeList t1 t23) in
+let tb = (makeList t12 t3) in
+let tc = (makeList t1 (makeList t23 nil)) in
+
+sum-leaves t1 ~~> 1
+sum-leaves t2 ~~> 2
+sum-leaves t3 ~~> 3
+sum-leaves t12 ~~> 3
+sum-leaves t23 ~~> 5
+sum-leaves ta ~~> 6
+sum-leaves tb ~~> 6
+sum-leaves tc ~~> 6
</pre>
-It may require more resources than my browser is willing to devote to
-JavaScript.]
+2. Write a function that counts the number of leaves.
var res = left, x;
while (stack.length) {
x = stack.shift();
- res = new Lambda_app(res, x.eval_loop([], eta));
+ // res = new Lambda_app(res, x.eval_loop([], eta));
+ res = new Lambda_app(res, reduce(x, eta, false));
}
return res;
}
- return unwind(this, stack);
+ // return unwind(this, stack);
+ // trampoline to, args
+ return [null, unwind(this, stack)];
};
this.eval_cbv = function (aggressive) {
return this;
this.eval_loop = function (stack, eta) {
var new_stack = stack.slice(0);
new_stack.unshift(this.right);
- return this.left.eval_loop(new_stack, eta);
+ // return this.left.eval_loop(new_stack, eta);
+ // trampoline to, args
+ return [this.left, new_stack, eta];
};
this.eval_cbv = function (aggressive) {
var left = this.left.eval_cbv(aggressive);
};
this.eval_loop = function (stack, eta) {
if (stack.length === 0) {
- var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
- if (eta) {
- return term.check_eta();
- } else {
- return term;
- }
+ // var term = new Lambda_lam(this.bound, this.body.eval_loop([], eta));
+ var term = new Lambda_lam(this.bound, reduce(this.body, eta, false));
+ if (eta) {
+ return [null, term.check_eta()];
+ } else {
+ return [null, term];
+ }
} else {
var x = stack[0];
var xs = stack.slice(1);
- return subst(this.bound, x, this.body).eval_loop(xs, eta);
+ // return subst(this.bound, x, this.body).eval_loop(xs, eta);
+ // trampoline to, args
+ return [subst(this.bound, x, this.body), xs, eta];
}
};
this.eval_cbv = function (aggressive) {
if (cbv) {
return expr.eval_cbv(cbv > 1);
} else {
- return expr.eval_loop([], eta);
+ // return expr.eval_loop([], eta);
+ var to_eval = expr, res = [[], eta];
+ while (to_eval !== null) {
+ res = to_eval.eval_loop.apply(to_eval, res);
+ to_eval = res.shift();
+ }
+ return res[0];
}
}
for (;;) {
c = this.charAt(i);
if ((c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') ||
- (c >= '0' && c <= '9') || c === '_' || c === '-') {
+ (c >= '0' && c <= '9') || c === '_' || c === '-' || c === '/') {
str += c;
i += 1;
} else if (c === '?' || c === '!') {
i += 1;
// make sure next character is not an identifier
if ((c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') ||
- (c >= '0' && c <= '9') || c === '_' || c === '-' || c === '?' || c === '!') {
+ (c >= '0' && c <= '9') || c === '_' || c === '-' || c === '/' || c === '?' || c === '!') {
str += c;
i += 1;
make('name', str).error("Bad identifier");
--- /dev/null
+This discussion elaborates on the discussion of evaluation order in the
+class notes from week 2. It makes use of the reduction diagrams drawn
+in class, which makes choice of evaluation strategy a choice of which
+direction to move through a network of reduction links.
+
+
+Some lambda terms can be reduced in different ways:
+
+<pre>
+ ((\x.x)((\y.y) z))
+ / \
+ / \
+ / \
+ / \
+ ((\y.y) z) ((\x.x) z)
+ \ /
+ \ /
+ \ /
+ \ /
+ \ /
+ \ /
+ z
+</pre>
+
+But because the lambda calculus is confluent (has the diamond
+property, named after the shape of the diagram above), no matter which
+lambda you choose to target for reduction first, you end up at the
+same place. It's like travelling in Manhattan: if you walk uptown
+first and then head east, you end up in the same place as if you walk
+east and then head uptown.
+
+But which lambda you target has implications for efficiency and for
+termination. (Later in the course, it will have implications for
+the order in which side effects occur.)
+
+First, efficiency:
+
+<pre>
+ ((\x.w)((\y.y) z))
+ \ \
+ \ ((\x.w) z)
+ \ /
+ \ /
+ \ /
+ \ /
+ w
+</pre>
+
+If a function discards its argument (as `\x.w` does), it makes sense
+to target that function for reduction, rather than wasting effort
+reducing the argument only to have the result of all that work thrown
+away. So in this situation, the strategy of "always reduce the
+leftmost reducible lambda" wins.
+
+But:
+
+<pre>
+ ((\x.xx)((\y.y) z))
+ / \
+ (((\y.y) z)((\y.y) z) ((\x.xx) z)
+ / | /
+ / (((\y.y)z)z) /
+ / | /
+ / | /
+ / | /
+ (z ((\y.y)z)) | /
+ \ | /
+ -----------.---------
+ |
+ zz
+</pre>
+
+This time, the leftmost function `\x.xx` copies its argument.
+If we reduce the rightmost lambda first (rightmost branch of the
+diagram), the argument is already simplified before we do the
+copying. We arrive at the normal form (i.e., the form that cannot be
+further reduced) in two steps.
+
+But if we reduce the rightmost lambda first (the two leftmost branches
+of the diagram), we copy the argument before it has been evaluated.
+In effect, when we copy the unreduced argument, we double the amount
+of work we need to do to deal with that argument.
+
+So when the function copies its argument, the "always reduce the
+rightmost reducible lambda" wins.
+
+So evaluation strategies have a strong effect on how many reduction
+steps it takes to arrive at a stopping point (e.g., normal form).
+
+Now for termination:
+
+<pre>
+(\x.w)((\x.xxx)(\x.xxx))
+ | \
+ | (\x.w)((\x.xxx)(\x.xxx)(\x.xxx))
+ | / \
+ | / (\x.w)((\x.xxx)(\x.xxx)(\x.xxx)(\x.xxx))
+ | / / \
+ .----------------- etc.
+ |
+ w
+</pre>
+
+Here we have a function that discards its argument on the left, and a
+non-terminating term on the right. It's even more evil than Omega,
+because it not only never reduces, it generates more and more work
+with each so-called reduction. If we unluckily adopt the "always
+reduce the rightmost reducible lambda" strategy, we'll spend our days
+relentlessly copying out new copies of \x.xxx. But if we even once
+reduce the leftmost reducible lambda, we'll immediately jump to the
+normal form, `w`.
+
+We can roughly associate the "leftmost always" strategy with call by
+name (normal order), and the "rightmost always" strategy with call by
+value (applicative order). There are fine-grained distinctions among
+these terms of art that we will not pause to untangle here.
+
+If a term has a normal form (a reduction such that no further
+reduction is possible), then a leftmost-always reduction will find it.
+(That's why it's called "normal order": it's the evaluation order that
+guarantees finding a normal form if one exists.)
+
+Preview: if the evaluation of a function has side effects, then the
+choice of an evaluation strategy will make a big difference in which
+side effect occur and in which order.
Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; Lists and Numbers
-(27 Sept) ...(Notes to come)
+(27 Sept) Lecture notesfor [[Week3]]; [[Assignment3]].
+
Topics: Recursion with Fixed Point Combinators
<!-- Introducing the notion of a "continuation", which technique we'll now already have used a few times
+[[!toc]]
+
Building Lists
==============
* [Penn lambda calculator](http://www.ling.upenn.edu/lambda/) Pedagogical software developed by Lucas Champollion, Josh Tauberer and Maribel Romero.<p>
<!-- Haskell Curry had ideas that he felt were validated upon reading a 1924 paper by M. Schönfinkel "Uber die Bausteine der mathematischen Logik" which used combinators in a similar way to his own ideas. Haskell then wrote "An analysis of logical substitution" which appeared in the American Journal of Mathematics in 1929. -->
+
* [[!wikipedia Moses Schönfinkel]]
* [[!wikipedia Haskell Curry]]
* [[!wikipedia Alonzo Church]]<p>
<http://people.cs.uu.nl/jeroen/article/combinat/combinat.ps>
* [Chris Barker's Iota and Jot](http://semarch.linguistics.fas.nyu.edu/barker/Iota/)<p>
+* [To Dissect a Mockingbird](http://dkeenan.com/Lambda/index.htm)
+
## Evaluation Order ##
* [[!wikipedia Evaluation strategy]]
* [Y Combinator for Dysfunctional Non-Schemers](http://rayfd.wordpress.com/2007/05/06/y-combinator-for-dysfunctional-non-schemers/)
* [The Y Combinator](http://www.ece.uc.edu/~franco/C511/html/Scheme/ycomb.html)
* [The Y Combinator](http://dangermouse.brynmawr.edu/cs245/ycomb_jim.html) derives the applicative-order Y-combinator from scratch, in Scheme. This derivation is similar in flavor to the derivation found in The Little Schemer, but uses a slightly different starting approach...
-
+* [The church of the least fixed point, by Sans Pareil](http://www.springerlink.com/content/n4t2v573m58g2755/)
## Types ##
+++ /dev/null
-let empty = (\f (\z z)) in
-let ml = (\h (\t (\f (\z ((f h) ((t f) z)))))) in
-let list = ((ml a) ((ml b) ((ml c) ((ml d) ((ml e) empty))))) in
-let map = (\f (\l (l (\h (\t ((ml (f h)) t)))))) in
-
-(
-
-list
-
-((map (\x x)) list)
-
-)
-
+++ /dev/null
-<textarea id="INPUT" style="border: 2px solid black; color: black; font-family: monospace; height: 3in; overflow: auto; padding: 0.5em; width: 100%;">
-let true = \x y. x in
-let false = \x y. y in
-let and = \l r. l r false in
-(
- (and true true yes no)
- (and true false yes no)
- (and false true yes no)
- (and false false yes no)
-)
-</textarea>
-<input id="PARSE" value="Normalize" type="button">
-<input id="ETA" type="checkbox">do eta-reductions too
-<noscript><p>You may not see it because you have JavaScript turned off. Uffff!</p></noscript>
-<script src="/code/lambda.js"></script>
-<script src="/code/tokens.js"></script>
-<script src="/code/parse.js"></script>
-<script src="/code/json2.js"></script>
-<pre id="OUTPUT">
-</pre>
-<script>
-/*jslint evil: true */
-
-/*members create, error, message, name, prototype, stringify, toSource,
- toString, write
-*/
-
-/*global JSON, make_parse, parse, source, tree */
-
-// Make a new object that inherits members from an existing object.
-
-if (typeof Object.create !== 'function') {
- Object.create = function (o) {
- function F() {}
- F.prototype = o;
- return new F();
- };
-}
-
-// Transform a token object into an exception object and throw it.
-
-Object.prototype.error = function (message, t) {
- t = t || this;
- t.name = "SyntaxError";
- t.message = message;
- throw t;
-};
-
-
-(function () {
- var parse = make_parse();
-
- function go(source) {
- var string, tree, expr, eta;
- try {
- tree = parse(source);
- // string = JSON.stringify(tree, ['key', 'name', 'message', 'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);
- expr = tree.handler();
- // string = JSON.stringify(expr, ['key', 'name', 'message', 'value', 'arity', 'first', 'second', 'tag', 'variable', 'left', 'right', 'bound', 'body' ], 4);
-// string = expr.to_string() + "\n\n~~>\n\n";
- string = '';
- eta = document.getElementById('ETA').checked;
- string = string + reduce(expr, eta, false).to_string();
- } catch (e) {
- string = JSON.stringify(e, ['name', 'message', 'from', 'to', 'key',
- 'value', 'arity', 'first', 'second', 'third', 'fourth'], 4);
- }
- document.getElementById('OUTPUT').innerHTML = string
- .replace(/&/g, '&')
- .replace(/[<]/g, '<');
- }
-
- document.getElementById('PARSE').onclick = function (e) {
- go(document.getElementById('INPUT').value);
- };
-}());
-
-</script>
+[[!toc]]
+
+##More on evaluation strategies##
+
+Here are notes on [[evaluation order]] that make the choice of which
+lambda to reduce next the selection of a route through a network of
+links.
+
+
##Computing the length of a list##
How could we compute the length of a list? Without worrying yet about what lambda-calculus implementation we're using for the list, the basic idea would be to define this recursively:
##Fixed-point Combinators Are a Bit Intoxicating##
-
+
There's a tendency for people to say "Y-combinator" to refer to fixed-point combinators generally. We'll probably fall into that usage ourselves. Speaking correctly, though, the Y-combinator is only one of many fixed-point combinators.
that is similar, but expressed in terms of non-well-founded sets
rather than recursive functions.
-HOWEVER, you should be cautious about feeling too comfortable with
+##However...##
+
+You should be cautious about feeling too comfortable with
these results. Thinking again of the truth-teller paradox, yes,
<code>Ω</code> is *a* fixed point for `I`, and perhaps it has
some a privileged status among all the fixed points for `I`, being the
