From: Chris Barker Date: Mon, 4 Oct 2010 00:35:46 +0000 (-0400) Subject: edits X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=4cea4f69242f3a229292186c8fa652942f31f8b8;hp=2a61846bbb48e29385fc7639a47c76f82d70bb18 edits --- diff --git a/.gitignore b/.gitignore index 35f5b3c4..32e8d01d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,3 @@ /.ikiwiki /recentchanges -/.*.swp +.*.swp diff --git a/advanced_lambda.mdwn b/advanced_lambda.mdwn index 6760ae7f..d23245cf 100644 --- a/advanced_lambda.mdwn +++ b/advanced_lambda.mdwn @@ -3,31 +3,7 @@ #Version 4 lists: Efficiently extracting tails# -An advantage of the v3 lists and v3 (aka "Church") numerals is that they -have a recursive capacity built into their skeleton. So for many natural -operations on them, you won't need to use a fixed point combinator. Why is -that an advantage? Well, if you use a fixed point combinator, then the terms -you get -won't be strongly normalizing: whether their reduction stops at a normal form -will depend on what evaluation order you use. Our online [[lambda evaluator]] -uses normal-order reduction, so it finds a normal form if there's one to be -had. But if you want to build lambda terms in, say, Scheme, and you wanted to -roll your own recursion as we've been doing, rather than relying on Scheme's -native `let rec` or `define`, then you can't use the fixed-point combinators -`Y` or Θ. Expressions using them will have non-terminating -reductions, with Scheme's eager/call-by-value strategy. There are other -fixed-point combinators you can use with Scheme (in the [week 3 notes](/week3/#index7h2) they -were Y′ and Θ′. But even with -them, evaluation order still matters: for some (admittedly unusual) -evaluation strategies, expressions using them will also be non-terminating. - -The fixed-point combinators may be the conceptual stars. They are cool and -mathematically elegant. But for efficiency and implementation elegance, it's -best to know how to do as much as you can without them. (Also, that knowledge -could carry over to settings where the fixed point combinators are in -principle unavailable.) - -This is why the v3 lists and numbers are so lovely. However, one disadvantage +Version 3 lists and Church numerals are lovely, because they have their recursive capacity built into their very bones. However, one disadvantage to them is that it's relatively inefficient to extract a list's tail, or get a number's predecessor. To get the tail of the list `[a;b;c;d;e]`, one will basically be performing some operation that builds up the tail afresh: at diff --git a/assignment3.mdwn b/assignment3.mdwn index 8c22dfa4..289f818a 100644 --- a/assignment3.mdwn +++ b/assignment3.mdwn @@ -14,32 +14,30 @@ Recall that version 1 style lists are constructed like this (see let false = \x y. y in let and = \l r. l (r true false) false in - ; version 1 lists let make_pair = \f s g. g f s in - let fst = true in - let snd = false in + let get_fst = true in + let get_snd = false in let empty = make_pair true junk in - let isempty = \x. x fst in + let isempty = \x. x get_fst in let make_list = \h t. make_pair false (make_pair h t) in - let head = \l. isempty l err (l snd fst) in - let tail = \l. isempty l err (l snd snd) in - + let head = \l. isempty l err (l get_snd get_fst) in + let tail = \l. isempty l err (l get_snd get_snd) in + ; a list of numbers to experiment on let mylist = make_list 1 (make_list 2 (make_list 3 empty)) in - - ; a fixed-point combinator for defining recursive functions - let Y = \f. (\h. f (h h)) (\h. f (h h)) in - + ; church numerals let iszero = \n. n (\x. false) true in let succ = \n s z. s (n s z) in - let mult = \m n s. m (n s) in - let length = Y (\length l. isempty l 0 (succ (length (tail l)))) in - let pred = \n. iszero n 0 (length (tail (n (\p. make_list junk p) empty))) - in + let mul = \m n s. m (n s) in + let pred = (\shift n. n shift (make\_pair 0 0) get\_snd) (\p. p (\x y. make\_pair (succ x) x)) in let leq = \m n. iszero(n pred m) in let eq = \m n. and (leq m n)(leq n m) in - + + ; a fixed-point combinator for defining recursive functions + let Y = \f. (\h. f (h h)) (\h. f (h h)) in + let length = Y (\length l. isempty l 0 (succ (length (tail l)))) in + eq 2 2 yes no @@ -109,7 +107,7 @@ be your base case for your recursive functions that operate on these trees.
    -
  1. Write a function that sums the number of leaves in a tree. +
  2. Write a function that sums the values at the leaves in a tree. Expected behavior: diff --git a/assignment4.mdwn b/assignment4.mdwn index 34fb044d..9f566758 100644 --- a/assignment4.mdwn +++ b/assignment4.mdwn @@ -1,43 +1,89 @@ -Assignment 4 ------------- - #Reversing a list# -How would you define an operation to reverse a list? (Don't peek at the +
      +
    1. How would you define an operation to reverse a list? (Don't peek at the [[lambda_library]]! Try to figure it out on your own.) Choose whichever implementation of list you like. Even then, there are various strategies you can use. +(See [[hints/Assignment 4 hint 1]] if you need some hints.) +
    + #Comparing lists for equality# - + +
      +
    1. Suppose you have two lists of integers, `left` and `right`. You want to determine whether those lists are equal: that is, whether they have all the same members in the same order. (Equality for the lists we're working with is *extensional*, or parasitic on the equality of their members, and the list structure. Later in the course we'll see lists which aren't extensional in this way.) + +How would you implement such a list comparison? + +(See [[hints/Assignment 4 hint 2]] if you need some hints.) +
    + #Enumerating the fringe of a leaf-labeled tree# -[[Implementing trees]] +First, read this: [[Implementing trees]] + +
      +
    1. blah + +(See [[hints/Assignment 4 hint 3]] if you need some hints.) +
    + + +#Mutually-recursive functions# + +
      +
    1. (Challenging.) One way to define the function `even` is to have it hand off part of the work to another function `odd`: + + let even = \x. iszero x + ; if x == 0 then result is + true + ; else result turns on whether x's pred is odd + (odd (pred x)) + +At the same tme, though, it's natural to define `odd` in such a way that it hands off part of the work to `even`: + + let odd = \x. iszero x + ; if x == 0 then result is + false + ; else result turns on whether x's pred is even + (even (pred x)) + +Such a definition of `even` and `odd` is called **mutually recursive**. If you trace through the evaluation of some sample numerical arguments, you can see that eventually we'll always reach a base step. So the recursion should be perfectly well-grounded: + + even 3 + ~~> iszero 3 true (odd (pred 3)) + ~~> odd 2 + ~~> iszero 2 false (even (pred 2)) + ~~> even 1 + ~~> iszero 1 true (odd (pred 1)) + ~~> odd 0 + ~~> iszero 0 false (even (pred 0)) + ~~> false + +But we don't yet know how to implement this kind of recursion in the lambda calculus. + +The fixed point operators we've been working with so far worked like this: + + let X = Y T in + X <~~> T X + +Suppose we had a pair of fixed point operators, `Y1` and `Y2`, that operated on a *pair* of functions `T1` and `T2`, as follows: + + let X1 = Y1 T1 T2 in + let X2 = Y2 T1 T2 in + X1 <~~> T1 X1 X2 and + X2 <~~> T2 X1 X2 + +If we gave you such a `Y1` and `Y2`, how would you implement the above definitions of `even` and `odd`? + + +
    2. (More challenging.) Using our derivation of Y from the [[Week2]] notes as a model, construct a pair `Y1` and `Y2` that behave in the way described. +(See [[hints/Assignment 4 hint 4]] if you need some hints.) +
    diff --git a/assignment_3_evaluator.mdwn b/assignment_3_evaluator.mdwn index eb3c18b6..28693f43 100644 --- a/assignment_3_evaluator.mdwn +++ b/assignment_3_evaluator.mdwn @@ -6,23 +6,24 @@ let true = \x y. x in let false = \x y. y in let and = \l r. l (r true false) false in let or = \l r. l true r in -let make_pair = \f s g. g f s in -let get_fst = true in -let get_snd = false in -let empty = make_pair true junk in -let isempty = \x. x get_fst in -let make_list = \h t. make_pair false (make_pair h t) in -let head = \l. isempty l err (l get_snd get_fst) in -let tail = \l. isempty l err (l get_snd get_snd) in +; +let make\_pair = \f s g. g f s in +let get\_fst = true in +let get\_snd = false in +let empty = make\_pair true junk in +let isempty = \x. x get\_fst in +let make\_list = \h t. make\_pair false (make\_pair h t) in +let head = \l. isempty l err (l get\_snd get\_fst) in +let tail = \l. isempty l err (l get\_snd get\_snd) in ; ; a list of numbers to experiment on -let mylist = make_list 1 (make_list 2 (make_list 3 empty)) in +let mylist = make\_list 1 (make\_list 2 (make\_list 3 empty)) in ; ; church numerals let iszero = \n. n (\x. false) true in let succ = \n s z. s (n s z) in let mul = \m n s. m (n s) in -let pred = (\shift n. n shift (make_pair 0 0) get_snd) (\p. p (\x y. make_pair (succ x) x)) in +let pred = (\shift n. n shift (make\_pair 0 0) get\_snd) (\p. p (\x y. make\_pair (succ x) x)) in let leq = \m n. iszero(n pred m) in let eq = \m n. and (leq m n)(leq n m) in ; @@ -32,12 +33,12 @@ let Y = \f. (\h. f (h h)) (\h. f (h h)) in let length = Y (\length l. isempty l 0 (succ (length (tail l)))) in ; ; synonyms -let makePair = make_pair in -let fst = get_fst in -let snd = get_snd in +let makePair = make\_pair in +let fst = get\_fst in +let snd = get\_snd in let nil = empty in let isNil = isempty in -let makeList = make_list in +let makeList = make\_list in let isZero = iszero in let mult = mul in ; @@ -60,6 +61,7 @@ let tc = (make_list t1 (make_list t23 empty)) in ; length (tail mylist) + do eta-reductions too diff --git a/hints/assignment_4_hint_1.mdwn b/hints/assignment_4_hint_1.mdwn new file mode 100644 index 00000000..e95f96cc --- /dev/null +++ b/hints/assignment_4_hint_1.mdwn @@ -0,0 +1,42 @@ +Hints for reverse. + +* If left and right are two v3 lists, what is the result of: + + left make_list right + +* What is `reverse []`? What is `reverse [c]`? What is `reverse [b;c]`? How is it related to `reverse [c]`? + +* How is `reverse [a;b;c]` related to `reverse [b;c]`? + +* Getting any ideas? + + +Another strategy. + +* Our version 3 lists are _right_-folds. That is, `[a;b;c]` is implemented as: + + \f z. f a (f b (f c z)) + + which is the result of first combining the base value `z` with the rightmost element of the list, using `f`, then combining the result of that with the next element to the left, and so on. + + A _left_-fold on the same list would be: + + \f z. f (f (f z a) b) c + + which is the result of first combining the base value `z` with the leftmost element of the list, then combining the result of that with the next element to the right, and so on. + + It's conventional for `f` to take the accumulated value so far as its second argument when doing a right-fold, and for it to take it as its first argument when doing a left-fold. However, this convention could be ignored. We could also call this the left-fold of `[a;b;c]`: + + \f z. f c (f b (f a z)) + +* Getting any ideas? + +* Our `make_list` function for taking an existing, right-fold-based list, and a new element, and returning a new right-fold-based list, looks like this: + + let make_list = \hd tl. \f z. f hd (tl f z) + + How would you write a `make_left_list` function, that takes an existing, left-fold-based list, like `\f z. f c (f b z)`, and a new element, `a`, and returned the new, left-fold based list: + + \f z. f c (f b (f a z)) + + diff --git a/hints/assignment_4_hint_2.mdwn b/hints/assignment_4_hint_2.mdwn new file mode 100644 index 00000000..78cb1bd4 --- /dev/null +++ b/hints/assignment_4_hint_2.mdwn @@ -0,0 +1,25 @@ +Hints for list\_equal. + + diff --git a/hints/assignment_4_hint_3.mdwn b/hints/assignment_4_hint_3.mdwn new file mode 100644 index 00000000..48063d3a --- /dev/null +++ b/hints/assignment_4_hint_3.mdwn @@ -0,0 +1,2 @@ +Hints for enumerating a tree's fringe. + diff --git a/hints/assignment_4_hint_4.mdwn b/hints/assignment_4_hint_4.mdwn new file mode 100644 index 00000000..a30b4861 --- /dev/null +++ b/hints/assignment_4_hint_4.mdwn @@ -0,0 +1,2 @@ +Hints for Y1,Y2. + diff --git a/implementing_trees.mdwn b/implementing_trees.mdwn index 31dc3fd0..f83823a9 100644 --- a/implementing_trees.mdwn +++ b/implementing_trees.mdwn @@ -128,9 +128,9 @@ where the previous tree should be placed. However, when using trees as a computational tool, one usually does have latitude about how to structure a larger tree---in the same way that we had the -freedom to implement our sets with lists whose members were just appended in -the order we built the set up, or instead with lists whose members were ordered -numerically. +freedom to implement our [sets](/week4/#index9h1) with lists whose members were +just appended in the order we built the set up, or instead with lists whose +members were ordered numerically. When building a new tree, one strategy for where to put the new element and where to put the existing tree would be to always lean towards a certain side. diff --git a/index.mdwn b/index.mdwn index 3a4584ab..40de9d1c 100644 --- a/index.mdwn +++ b/index.mdwn @@ -59,7 +59,7 @@ it, and get assistance completing it if you need it, sooner. * We'll shortly be posting another assignment, assignment 4, which will be "due" on the Sunday before our next seminar. That is, on Sunday Oct 17. -(There's no seminar this coming Monday.) +(There's no seminar on Monday Oct 11.) The assignments will tend to be quite challenging. Again, you should by all means talk amongst yourselves, and to us, about strategies and @@ -87,25 +87,31 @@ what you think you need in order to solve the problem. (13 Sept) Lecture notes for [[Week1]]; [[Assignment1]]. -Topics: Applications; Basics of Lambda Calculus; Comparing Different Languages +> Topics: [[Applications]], including [[Damn]]; Basics of Lambda Calculus; Comparing Different Languages (20 Sept) Lecture notes for [[Week2]]; [[Assignment2]]. -Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; Lists and Numbers +> Topics: Reduction and Convertibility; Combinators; Evaluation Strategies and Normalization; Decidability; [[Lists and Numbers]] (27 Sept) Lecture notes for [[Week3]]; [[Assignment3]]; an evaluator with the definitions used for homework 3 preloaded is available at [[assignment 3 evaluator]]. -Topics: Recursion with Fixed Point Combinators +> Topics: [[Evaluation Order]]; Recursion with Fixed Point Combinators -(4 Oct) Lecture notes for Week 4 +(4 Oct) Lecture notes for [[Week4]]; Assignment4 - +> Topics: More on Fixed Points; Sets; Aborting List Traversals; [[Implementing Trees]] + + +(18 Oct) Lecture notes for Week 5 + +> Topics: Types, Polymorphism [[Upcoming topics]] +[Advanced Lambda Calculus Topics](/advanced lambda) + ##[[Offsite Reading]]## @@ -288,5 +294,4 @@ All wikis are supposed to have a [[SandBox]], so this one does too. This wiki is powered by [[ikiwiki]]. -[[Test]] diff --git a/lambda_library.mdwn b/lambda_library.mdwn index ff363756..5623b9fa 100644 --- a/lambda_library.mdwn +++ b/lambda_library.mdwn @@ -27,8 +27,8 @@ and all sorts of other places. Others of them are our own handiwork. ; 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 + let get_fst = \x y. x in ; aka true + let get_snd = \x y. y in ; aka false ; triples let make_triple = \x y z f. f x y z in @@ -50,7 +50,7 @@ and all sorts of other places. Others of them are our own handiwork. 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) + let tail = \lst. (\shift. lst shift (make_pair empty tail_empty) get_snd) ; 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 @@ -82,10 +82,10 @@ and all sorts of other places. Others of them are our own handiwork. 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 isempty = \lst. lst get_fst in + let head = \lst. isempty lst err (lst get_snd get_fst) in let tail_empty = empty in - let tail = \lst. isempty lst tail_empty (lst get_2nd get_2nd) in + let tail = \lst. isempty lst tail_empty (lst get_snd get_snd) in ; more math with Church numerals @@ -104,7 +104,7 @@ and all sorts of other places. Others of them are our own handiwork. ; three strategies for predecessor let pred_zero = zero in - let pred = (\shift n. n shift (make_pair zero pred_zero) get_2nd) + let pred = (\shift n. n shift (make_pair zero pred_zero) get_snd) ; 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 @@ -127,15 +127,15 @@ and all sorts of other places. Others of them are our own handiwork. ; more efficient comparisons, Oleg's gt provided some simplifications - let leq = (\base build consume. \m n. n consume (m build base) get_1st) + let leq = (\base build consume. \m n. n consume (m build base) get_fst) ; 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 + (\p. p get_fst p (p get_snd)) in let lt = \m n. not (leq n m) in - let eq = (\base build consume. \m n. n consume (m build base) get_1st) + let eq = (\base build consume. \m n. n consume (m build base) get_fst) ; 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 @@ -144,7 +144,7 @@ and all sorts of other places. Others of them are our own handiwork. ; and build is (\p. make_pair false (K p)) ; and consume is - (\p. p get_2nd p) in + (\p. p get_snd p) in ; -n is a fixedpoint of \x. add (add n x) x @@ -161,13 +161,13 @@ and all sorts of other places. Others of them are our own handiwork. (make_triple (succ cur) false (succ sofar)) ; continue )) in ; or - let sub = (\base build consume. \m n. n consume (m build base) get_1st) + let sub = (\base build consume. \m n. n consume (m build base) get_fst) ; 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 + (\p. p get_snd p) in let min = \m n. sub m (sub m n) in @@ -208,8 +208,8 @@ and all sorts of other places. Others of them are our own handiwork. ; 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 + let div = \n d. divmod n d get_fst in + let mod = \n d. divmod n d get_snd in ; sqrt n is a fixedpoint of \x. div (div (add n (mul x x)) 2) x @@ -259,13 +259,13 @@ and all sorts of other places. Others of them are our own handiwork.