## Topics by content ##
-* [[Introduction to functional programming|topics/week1 kapulet intro]]
+* Functional Programming
+
+ * [[Introduction|topics/week1 kapulet intro]]
+ * [[Week 1 Advanced notes|topics/week1 kapulet advanced]]
+ * [["Rosetta Stone" page #1 for Kaupulet, Scheme, OCaml, Haskell|rosetta1]]
+ * Offsite links for help on [[learning Scheme]], [[OCaml|learning OCaml]], and [[Haskell|learning Haskell]]
+ * List Comprehensions
+
+* Order, "static versus dynamic"
+
+ * [[Order in programming languages and natural language|topics/week1 order]]
+ * Reduction Strategies and Normal Forms in the Lambda Calculus
+
+* The Lambda Calculus
+
+ * [[Introduction to the Lambda Calculus|topics/week2 lambda intro]]
+ * [[Advanced notes on the Lambda Calculus|topics/week2 lambda advanced]]
+ * Encoding data types in the Lambda Calculus
+ * [[Booleans|topics/week2 encodings#booleans]]
+ * [[Tuples|topics/week2 encodings#tuples]]
+ * [[Lists|topics/week2 encodings#lists]], v1 (as right-folds)
+ * [[Numbers|topics/week2 encodings#numbers]], v1 ("Church's encoding")
+ * How to get the `tail` of v1 lists?
+ * Reduction Strategies and Normal Forms
+
+
+* Combinatorial Logic
-* [[Order: static versus dynamic|topics/week1 order]]
## Topics by week ##
Week 1:
-* [[Order in programming languages and natural language|topics/week1 order]]
+* [[Order in programming languages and natural language|topics/week1 order]]
This discussion considers conjunction in a language that recognized presupposition failure.
-* [[Introduction to functional programming|topics/week1 kapulet intro]]
+* [[Introduction to functional programming|topics/week1 kapulet intro]]
Basics of functional programming: `let`, `case`, pattern matching, and
recursion. Definitions of factorial.
-* [[Advanced notes on functional programming|topics/week1 kapulet advanced]]
-* [[Homework for week 1|exercises/assignment1]]
+* [[Advanced notes on functional programming|topics/week1 kapulet advanced]]
+* [[Homework for week 1|exercises/assignment1]] ([[Answers|exercises/assignment1_answers]])
Week 2:
-* [[Introduction to the Lambda Calculus|topics/week2 lambda intro]]
-* [[Advanced notes on the Lambda Calculus|topics/week2 lambda advanced]]
-* [[Encoding Booleans, Tuples, Lists, and Numbers|topics/week2 encodings]];
-* [[Homework for week 2|exercises/assignment2]]
+* [[Introduction to the Lambda Calculus|topics/week2 lambda intro]]
+* [[Advanced notes on the Lambda Calculus|topics/week2 lambda advanced]]
+* [[Encoding Booleans, Tuples, Lists, and Numbers|topics/week2 encodings]]
+* [[Homework for week 2|exercises/assignment2]]
Week 3:
-* More on Lists
-Introduces list comprehensions, shows how to encode `tail` in the Lambda Calculus
-* Combinatorial Logic
-* Homework for week 3
+* More on Lists
+Introduces list comprehensions, discusses how to get the `tail` of lists in the Lambda Calculus
+* Combinatorial Logic
+* Reduction Strategies and Normal Forms
+* Homework for week 3
--- /dev/null
+Syntax
+------
+
+Insert all the implicit `( )`s and <code>λ</code>s into the following abbreviated expressions.
+
+1. `x x (x x x) x`
+ <code><b>(((</b>x x<b>)</b> (<b>(</b>x x<b>)</b> x)<b>)</b> x<b>)</b></code>
+2. `v w (\x y. v x)`
+ <code><b>((</b>v w<b>)</b> (\x <b>(\</b>y <b>(</b>v x<b>))</b>)<b>)</b></code>
+3. `(\x y. x) u v`
+ <code><b>((</b>(\x <b>(\</b>y x<b>)</b>) u<b>)</b> v<b>)</b></code>
+4. `w (\x y z. x z (y z)) u v`
+ <code><b>(((</b>w (\x <b>(\</b>y <b>(\</b>z <b>((</b>x z<b>)</b> (y z)<b>)))</b>)<b>)</b> u<b>)</b> v<b>)</b></code>
+
+Mark all occurrences of `(x y)` in the following terms:
+
+5. <code>(\x y. <u>x y</u>) x y</code>
+6. <code>(\x y. <u>x y</u>) (<u>x y</u>)</code>
+7. <code>\x y. <u>x y</u> (<u>x y</u>)</code>
+
+Reduction
+---------
+
+Find "normal forms" for the following---that is, reduce them until no more reductions are possible. As mentioned in the notes, we'll write <code>λx</code> as `\x`. If we ever say "reduce" without qualifications, we mean just "beta-reduce" (as opposed to "(beta + eta)-reduce").
+
+8. `(\x \y. y x) z` ~~> `\y. y z`
+9. `(\x (x x)) z` ~~> `z z`
+10. `(\x (\x x)) z` ~~> `\x x`
+11. `(\x (\z x)) z` ~~> `\y z`, be sure to change `\z` to a different variable so as not to "capture" `z`
+12. `(\x (x (\y y))) (\z (z z))` ~~> `\y y`
+13. `(\x (x x)) (\x (x x))` umm..., reductions will forever be possible, they just don't "do" much
+14. `(\x (x x x)) (\x (x x x))` that's just mean
+
+
+
+Booleans
+--------
+
+For these questions, and the ones on triples below, we're setting them up so as to encourage you to experiment with Racket and to formulate your answer in Scheme/Racket syntax. But you can answer in Lambda Calculus syntax if you prefer.
+
+Recall our definitions of true and false.
+
+> **true** is defined to be `\t f. t`
+> **false** is defined to be `\t f. f`
+
+In Racket, these functions can be defined like this:
+
+ (define true (lambda (t) (lambda (f) t)))
+ (define false (lambda (t) (lambda (f) f)))
+
+(Note that they are different from Racket's *primitive* boolean values `#t` and `#f`.)
+
+
+15. Define a `neg` operator that negates `true` and `false`.
+
+ Expected behavior:
+
+ (((neg true) 10) 20)
+
+ evaluates to `20`, and
+
+ (((neg false) 10) 20)
+
+ evaluates to `10`.
+
+ (define neg (lambda (p) ((p false) true)))
+
+16. Define an `or` operator.
+
+ (define or (lambda (p) (lambda (q) ((p p) q))))
+
+ or:
+
+ (define or (lambda (p) (lambda (q) ((p true) q))))
+
+
+17. Define an `xor` operator. If you haven't seen this term before, here's a truth table:
+
+ true xor true == false
+ true xor false == true
+ false xor true == true
+ false xor false == false
+
+ <!-- -->
+
+ (define xor (lambda (p) (lambda (q) ((p (neg q)) q))))
+
+
+Triples
+-------
+
+Recall our definitions of ordered triples.
+
+> the triple **(**a**, **b**, **c**)** is defined to be `\f. f a b c`
+
+To extract the first element of a triple `t`, you write:
+
+ t (\fst snd trd. fst)
+
+Here are some definitions in Racket:
+
+ (define make-triple (lambda (fst) (lambda (snd) (lambda (trd) (lambda (f) (((f fst) snd) trd))))))
+ (define fst_of_three (lambda (fst) (lambda (snd) (lambda (trd) fst))))
+ (define snd_of_three (lambda (fst) (lambda (snd) (lambda (trd) snd))))
+
+Now we can write:
+
+ (define t (((make-triple 10) 20) 30))
+ (t fst_of_three) ; will evaluate to 10
+ (t snd_of_three) ; will evaluate to 20
+
+If you're puzzled by having the triple to the left and the function that
+operates on it come second, think about why it's being done this way: the triple
+is a package that takes a function for operating on its elements *as an
+argument*, and returns *the result of* operating on its elements with that
+function. In other words, the triple is a higher-order function.
+
+
+18. Define the `swap12` function that permutes the elements of a triple. Expected behavior:
+
+ (define t (((make-triple 10) 20) 30))
+ ((t swap12) fst_of_three) ; evaluates to 20
+ ((t swap12) snd_of_three) ; evaluates to 10
+
+ Write out the definition of `swap12` in Racket.
+
+ (define swap12 (lambda (x) (lambda (y) (lambda (z)
+ (lambda (f) (((f y) x) z))))))
+
+
+19. Define a `dup3` function that duplicates its argument to form a triple
+whose elements are the same. Expected behavior:
+
+ ((dup3 10) fst_of_three) ; evaluates to 10
+ ((dup3 10) snd_of_three) ; evaluates to 10
+
+ <!-- -->
+
+ (define dup3 (lambda (x)
+ (lambda (f) (((f x) x) x))))
+
+20. Define a `dup27` function that makes
+twenty-seven copies of its argument (and stores them in a data structure of
+your choice).
+
+ OK, then we will store them in a triply-nested triple:
+
+ (define dup27 (lambda (x) (dup3 (dup3 (dup3 x)))))
+
+Folds and Lists
+---------------
+
+21. Using Kapulet syntax, define `fold_left`.
+
+ # fold_left (f, z) [a, b, c] == f (f (f z a) b) c
+ letrec
+ fold_left (f, z) xs = case xs of
+ [] then z;
+ x' & xs' then fold_left (f, f (z, x')) xs'
+ end
+ in fold_left
+
+
+22. Using Kapulet syntax, define `filter` (problem 7 in last week's homework) in terms of `fold_right` and other primitive syntax like `lambda`, `&`, and `[]`. Don't use `letrec`! All the `letrec`-ing that happens should come from the one inside the definition of `fold_right`.
+
+ let
+ filter (p, xs) = fold_right ((lambda (y, ys). if p y then y & ys else ys), []) xs
+ in filter
+
+23. Using Kapulet syntax, define `&&` in terms of `fold_right`. (To avoid trickiness about the infix syntax, just call it `append`.) As with problem 22 (the previous problem), don't use `letrec`!
+
+ let
+ xs && ys = fold_right ((&), ys) xs
+ # or append (xs, ys) = ...
+ in (&&)
+
+24. Using Kapulet syntax, define `head` in terms of `fold_right`. When applied to a non-empty list, it should give us the first element of that list. When applied to an empty list, let's say it should give us `'err`. As with problem 22, don't use `letrec`!
+
+ let
+ head xs = fold_right ((lambda (y, _). y), 'err) xs
+ in head
+
+25. We mentioned in the Encoding notes that `fold_left (flipped_cons, []) xs` would give us the elements of `xs` but in the reverse order. So that's how we can express `reverse` in terms of `fold_left`. How would you express `reverse` in terms of `fold_right`? As with problem 22, don't use `letrec`!
+
+ See the [[hint|assignment2 hint]].
+
+
+Numbers
+-------
+
+26. Given that we've agreed to Church's encoding of the numbers:
+
+ <code>0 ≡ \f z. z</code>
+ <code>1 ≡ \f z. f z</code>
+ <code>2 ≡ \f z. f (f z)</code>
+ <code>3 ≡ \f z. f (f (f z))</code>
+ <code>...</code>
+
+ How would you express the `succ` function in the Lambda Calculus?
+
+ let succ = \n. \f z. f (n f z) in ...
+
+ Compare the definition of `cons`, which has an additional element:
+
+ <code>let cons = \<u>d</u> ds. \f z. f <u>d</u> (ds f z) in ...</code>
--- /dev/null
+1. Define a function `zero?` that expects a single number as an argument, and returns `'true` if that number is `0`, else returns `'false`.
+
+ let
+ zero? match lambda x. case x of
+ 0 then 'true;
+ y then 'false
+ end
+ in zero?
+
+
+2. Define a function `empty?` that expects a sequence of values as an argument (doesn't matter what type of values), and returns `'true` if that sequence is the empty sequence `[]`, else returns `'false`.
+
+ let
+ empty? match lambda xs. case xs of
+ [] then 'true;
+ _ & _ then 'false
+ end
+ in empty?
+
+ The second `case` clause could also just be `_ then 'false`.
+
+3. Define a function `tail` that expects a sequence of values as an argument (doesn't matter what type of values), and returns that sequence with the first element (if any) stripped away. (Applying `tail` to the empty sequence `[]` can just give us back the empty sequence.)
+
+ let
+ tail match lambda xs. case xs of
+ [] then [];
+ _ & xs' then xs'
+ end
+ in tail
+
+
+4. Define a function `drop` that expects two arguments, in the form (*number*, *sequence*), and works like this:
+
+ drop (0, [10, 20, 30]) # evaluates to [10, 20, 30]
+ drop (1, [10, 20, 30]) # evaluates to [20, 30]
+ drop (2, [10, 20, 30]) # evaluates to [30]
+ drop (3, [10, 20, 30]) # evaluates to []
+ drop (4, [10, 20, 30]) # evaluates to []
+
+ <!-- -->
+
+ letrec
+ drop match lambda (n, xs). case (n, xs) of
+ (0, _) then xs;
+ (_, []) then [];
+ (_, _ & xs') then drop (n-1, xs')
+ end
+ in drop
+
+ What is the relation between `tail` and `drop`?
+
+ let
+ tail xs = drop (1, xs)
+ in ...
+
+ That uses [[the shorthand explained here|topics/week1_kapulet_advanced#funct-declarations]], which I will continue to use below.
+
+5. Define a function `take` that expects two arguments, in the same form as `drop`, but works like this instead:
+
+ take (0, [10, 20, 30]) # evaluates to []
+ take (1, [10, 20, 30]) # evaluates to [10]
+ take (2, [10, 20, 30]) # evaluates to [10, 20]
+ take (3, [10, 20, 30]) # evaluates to [10, 20, 30]
+ take (4, [10, 20, 30]) # evaluates to [10, 20, 30]
+
+ <!-- -->
+
+ letrec
+ take (n, xs) = case (n, xs) of
+ (0, _) then [];
+ (_, []) then [];
+ (_, x' & xs') then x' & take (n-1, xs')
+ end
+ in take
+
+
+6. Define a function `split` that expects two arguments, in the same form as `drop` and `take`, but this time evaluates to a pair of results. It works like this:
+
+ split (0, [10, 20, 30]) # evaluates to ([], [10, 20, 30])
+ split (1, [10, 20, 30]) # evaluates to ([10], [20, 30])
+ split (2, [10, 20, 30]) # evaluates to ([10, 20], [30])
+ split (3, [10, 20, 30]) # evaluates to ([10, 20, 30], [])
+ split (4, [10, 20, 30]) # evaluates to ([10, 20, 30], [])
+
+ <!-- -->
+
+ letrec
+ split (n, xs) = case (n, xs) of
+ (0, _) then ([], xs);
+ (_, []) then ([], []);
+ (_, x' & xs') then let
+ (ys, zs) match split (n-1, xs')
+ in (x' & ys, zs)
+ end
+ in split
+
+7. Write a function `filter` that expects two arguments. The second argument will be a sequence `xs` with elements of some type *t*, for example numbers. The first argument will be a function `p` that itself expects arguments of type *t* and returns `'true` or `'false`. What `filter` should return is a sequence that contains exactly those members of `xs` for which `p` returned `'true`.
+
+ letrec
+ filter (p, xs) = case xs of
+ [] then [];
+ x' & xs' when p x' then x' & filter (p, xs');
+ _ & xs' then filter (p, xs')
+ end
+ in filter
+
+ The above solution uses [[pattern guards|/topics/week1_kapulet_advanced#guards]].
+
+
+8. Write a function `partition` that expects two arguments, in the same form as `filter`, but this time evaluates to a pair of results. It works like this:
+
+ partition (odd?, [11, 12, 13, 14]) # evaluates to ([11, 13], [12, 14])
+ partition (odd?, [11]) # evaluates to ([11], [])
+ partition (odd?, [12, 14]) # evaluates to ([], [12, 14])
+
+ <!-- -->
+
+ letrec
+ partition (p, xs) = case xs of
+ [] then ([], []);
+ x' & xs' then let
+ (ys, zs) match partition (p, xs')
+ in if p x' then (x' & ys, zs) else (ys, x' & zs)
+ end
+ in partition
+
+
+9. Write a function `double` that expects one argument which is a sequence of numbers, and returns a sequence of the same length with the corresponding elements each being twice the value of the original element.
+
+ letrec
+ double xs = case xs of
+ [] then [];
+ x' & xs' then (2*x') & double xs'
+ end
+ in double
+
+
+10. Write a function `map` that generalizes `double`. This function expects a pair of arguments, the second being a sequence `xs` with elements of some type *t*, for example numbers. The first argument will be a function `f` that itself expects arguments of type *t* and returns some type *t'* of result. What `map` should return is a sequence of the results, in the same order as the corresponding original elements. The result should be that we could say:
+
+ letrec
+ map match lambda (f, xs). case xs of
+ [] then [];
+ x' & xs' then (f x') & map (f, xs')
+ end;
+ double match lambda xs. map ((lambda x. 2*x), xs)
+ in ...
+
+11. Write a function `map2` that generalizes `map`. This function expects a triple of arguments: the first being a function `f` as for `map`, and the second and third being two sequences. In this case `f` is a function that expects *two* arguments, one from the first of the sequences and the other from the corresponding position in the other sequence. The result should behave like this:
+
+ map2 ((lambda (x,y). 10*x + y), [1, 2, 3], [4, 5, 6]) # evaluates to [14, 25, 36]
+
+ <!-- -->
+
+ letrec
+ map2 (f, xs, ys) = case (xs, ys) of
+ ([], _) then [];
+ (_, []) then [];
+ (x' & xs', y' & ys') then (f x' y') & map2 (f, xs', ys')
+ end
+ in map2
+
+
+###Extra credit problems###
+
+* In class I mentioned a function `&&` which occupied the position *between* its arguments, rather than coming before them (this is called an "infix" function). The way that it works is that `[1, 2, 3] && [4, 5]` evaluates to `[1, 2, 3, 4, 5]`. Define this function, making use of `letrec` and the simpler infix operation `&`.
+
+ letrec
+ xs && ys = case xs of
+ [] then ys;
+ x' & xs' then x' & (xs' && ys)
+ end
+ in (&&)
+
+ This solution is using a variation of [[the shorthand explained here|topics/week1_kapulet_advanced#funct-declarations]]. We didn't expect you'd know how to deal with the special syntax of `&&`. You might have just defined this using a regular name, like `append`.
+
+* Write a function `unmap2` that is something like the inverse of `map2`. This function expects two arguments, the second being a sequence of elements of some type *t*. The first is a function `g` that expects a single argument of type *t* and returns a *pair* of results, rather than just one result. We want to collate these results, the first into one sequence, and the second into a different sequence. Then `unmap2` should return those two sequences. Thus if:
+
+ g z1 # evaluates to (x1, y1)
+ g z2 # evaluates to (x2, y2)
+ g z3 # evaluates to (x3, y3)
+
+ Then `unmap2 (g, [z1, z2, z3])` should evaluate to `([x1, x2, x3], [y1, y2, y3])`.
+
+ letrec
+ unmap2 (g, zs) = case zs of
+ [] then ([], []);
+ z' & zs' then let
+ (x, y) match g z';
+ (xs, ys) match unmap2 (g, zs')
+ in (x & xs, y & ys)
+ end
+ in unmap2
+
+* Write a function `takewhile` that expects a `p` argument like `filter`, and also a sequence. The result should behave like this:
+
+ takewhile ((lambda x. x < 10), [1, 2, 20, 4, 40]) # evaluates to [1, 2]
+
+ Note that we stop "taking" once we reach `20`, even though there are still later elements in the sequence that are less than `10`.
+
+ letrec
+ takewhile (p, xs) = case xs of
+ [] then [];
+ x' & xs' then if p x' then x' & takewhile (p, xs')
+ else []
+ end
+ in takewhile
+
+* Write a function `dropwhile` that expects a `p` argument like `filter`, and also a sequence. The result should behave like this:
+
+ dropwhile ((lambda x. x < 10), [1, 2, 20, 4, 40]) # evaluates to [20, 4, 40]
+
+ Note that we stop "dropping" once we reach `20`, even though there are still later elements in the sequence that are less than `10`.
+
+ letrec
+ dropwhile (p, xs) = case xs of
+ x' & xs' when p x' then dropwhile (p, xs');
+ _ & _ then xs;
+ [] then []
+ end
+ in dropwhile
+
+ Unlike the previous solution, this one uses [[pattern guards|/topics/week1_kapulet_advanced#guards]], merely for variety. (In this solution the last two `case` clauses could also be replaced by the single clause `_ then xs`.)
+
+* Write a function `reverse` that returns the reverse of a sequence. Thus, `reverse [1, 2, 3, 4]` should evaluate to `[4, 3, 2, 1]`.
+
+ letrec
+ aux (ys, xs) = case xs of
+ [] then ys;
+ x' & xs' then aux (x' & ys, xs')
+ end;
+ reverse xs = aux ([], xs)
+ in reverse
+
21. Using Kapulet syntax, define `fold_left`.
-22. Using Kapulet syntax, define `filter` (problem 7 in last week's homework) in terms of `fold_right` and other primitive syntax like `lambda`, `&`, and `[]`. Don't use `letrec`!
+22. Using Kapulet syntax, define `filter` (problem 7 in last week's homework) in terms of `fold_right` and other primitive syntax like `lambda`, `&`, and `[]`. Don't use `letrec`! All the `letrec`-ing that happens should come from the one inside the definition of `fold_right`.
-23. Using Kapulet syntax, define `&&` in terms of `fold_right`. (To avoid trickiness about the infix syntax, just call it `append`.)
+23. Using Kapulet syntax, define `&&` in terms of `fold_right`. (To avoid trickiness about the infix syntax, just call it `append`.) As with problem 22 (the previous problem), don't use `letrec`!
-24. Using Kapulet syntax, define `head` in terms of `fold_right`. When applied to a non-empty list, it should give us the first element of that list. When applied to an empty list, let's say it should give us `'err`.
+24. Using Kapulet syntax, define `head` in terms of `fold_right`. When applied to a non-empty list, it should give us the first element of that list. When applied to an empty list, let's say it should give us `'err`. As with problem 22, don't use `letrec`!
-25. We mentioned in the Encoding notes that `fold_left (flipped_cons, []) xs` would give us the elements of `xs` but in the reverse order. So that's how we can express `reverse` in terms of `fold_left`. How would you express `reverse` in terms of `fold_right`?
+25. We mentioned in the Encoding notes that `fold_left (flipped_cons, []) xs` would give us the elements of `xs` but in the reverse order. So that's how we can express `reverse` in terms of `fold_left`. How would you express `reverse` in terms of `fold_right`? As with problem 22, don't use `letrec`!
This problem does have an elegant and concise solution, but it may be hard for you to figure it out. We think it will a useful exercise for you to try, anyway. We'll give a [[hint|assignment2 hint]]. Don't look at the hint until you've gotten really worked up about the problem. Before that, it probably will just be baffling. If your mind has really gotten its talons into the problem, though, the hint might be just what you need to break it open.
2. What does `[ 10*x + y | y from [4], x from [1, 2, 3] ]` evalaute to?
-3. Using either Kapulet's or Haskell's list comprehension syntax, write an expression that transforms `[3, 1, 0, 2]` into `[3, 3, 3, 1, 2, 2]`. [[Here is a hint|assignment3 hints]], if you need it.
+3. Using either Kapulet's or Haskell's list comprehension syntax, write an expression that transforms `[3, 1, 0, 2]` into `[3, 3, 3, 1, 2, 2]`. [[Here is a hint|assignment3 hint1]], if you need it.
## Lists
6. Continuing to encode lists in terms of their left-folds, what should `last` be, where `last [a, b, c]` should result in `c`. Let `last []` result in whatever `err` is bound to.
-7. Continuing to encode lists in terms of their left-folds, how should we write `head`? This is challenging. [[Here is a hint|assignment3 hints]], if you need it.
+7. Continuing to encode lists in terms of their left-folds, how should we write `head`? This is challenging. [[Here is a solution|assignment3 hint2]], if you need help.
## Numbers
--- /dev/null
+## Comprehensions
+
+3. Using either Kapulet's or Haskell's list comprehension syntax, write an expression that transforms `[3, 1, 0, 2]` into `[3, 3, 3, 1, 2, 2]`.
+
+*Here is a hint*
+
+Define a function `dup (n, x)` that creates a list of *n* copies of `x`. Then use list comprehensions to transform `[3, 1, 0, 2]` into `[[3, 3, 3], [1], [], [2, 2]]`. Then use `join` to "flatten" the result.
-## Comprehensions
-
-3. Using either Kapulet's or Haskell's list comprehension syntax, write an expression that transforms `[3, 1, 0, 2]` into `[3, 3, 3, 1, 2, 2]`.
-
-*Here is a hint*
-
-Define a function `dup (n, x)` that creates a list of *n* copies of `x`. Then use list comprehensions to transform `[3, 1, 0, 2]` into `[[3, 3, 3], [1], [], [2, 2]]`. Then use `join` to "flatten" the result.
-
## Lists
7. Continuing to encode lists in terms of their left-folds, how should we write `head`? This is challenging.
> Also, if you're reading the Hankin book, try reading Chapters 1-3. You will most likely need to come back again and read it multiple times; but this would be a good time to make the first attempt.
+> We posted [[answers to Week 1's homework|exercises/assignment1_answers]].
<!--
We've added a [[Monad Library]] for OCaml.
--- /dev/null
+Combinators and Combinatorial Logic
+===================================
+
+Lambda expressions that have no free variables are known as **combinators**. Here are some common ones:
+
+> **I** is defined to be `\x x`
+
+> **K** is defined to be `\x y. x`. That is, it throws away its
+ second argument. So `K x` is a constant function from any
+ (further) argument to `x`. ("K" for "constant".) Compare K
+ to our definition of `true`.
+
+> **S** is defined to be `\f g x. f x (g x)`. This is a more
+ complicated operation, but is extremely versatile and useful
+ (see below): it copies its third argument and distributes it
+ over the first two arguments.
+
+> **get-first** was our function for extracting the first element of an ordered pair: `\fst snd. fst`. Compare this to K and `true` as well.
+
+> **get-second** was our function for extracting the second element of an ordered pair: `\fst snd. snd`. Compare this to our definition of `false`.
+
+> **B** is defined to be: `\f g x. f (g x)`. (So `B f g` is the composition `\x. f (g x)` of `f` and `g`.)
+
+> **C** is defined to be: `\f x y. f y x`. (So `C f` is a function like `f` except it expects its first two arguments in swapped order.)
+
+> **W** is defined to be: `\f x . f x x`. (So `W f` accepts one argument and gives it to `f` twice. What is the meaning of `W multiply`?)
+
+> **ω** (that is, lower-case omega) is defined to be: `\x. x x`
+
+It's possible to build a logical system equally powerful as the lambda calculus (and readily intertranslatable with it) using just combinators, considered as atomic operations. Such a language doesn't have any variables in it: not just no free variables, but no variables at all.
+
+One can do that with a very spare set of basic combinators. These days
+the standard base is just three combinators: S, K, and I.
+(Though we'll see shortly that the behavior of I can be exactly
+simulated by a combination of S's and K's.) But it's possible to be
+even more minimalistic, and get by with only a single combinator (see
+links below for details). (And there are different single-combinator
+bases you can choose.)
+
+There are some well-known linguistic applications of Combinatory
+Logic, due to Anna Szabolcsi, Mark Steedman, and Pauline Jacobson.
+They claim that natural language semantics is a combinatory system: that every
+natural language denotation is a combinator.
+
+For instance, Szabolcsi 1987 argues that reflexive pronouns are argument
+duplicators.
+
+ everyone hit himself
+ S/(S!NP) (S!NP)/NP (S!NP)!((S!NP)/NP)
+ \fAx[fx] \y\z[HIT y z] \h\u[huu]
+ ---------------------------------
+ S!NP \u[HIT u u]
+ --------------------------------------------
+ S Ax[HIT x x]
+
+Here, "A" is our crude markdown approximation of the universal quantifier.
+Notice that the semantic value of *himself* is exactly `W`.
+The reflexive pronoun in direct object position combines with the transitive verb. The result is an intransitive verb phrase that takes a subject argument, duplicates that argument, and feeds the two copies to the transitive verb meaning.
+
+Note that `W <~~> S(CI)`:
+
+<pre><code>S(CI) ≡
+S((\fxy.fyx)(\x.x)) ~~>
+S(\xy.(\x.x)yx) ~~>
+S(\xy.yx) ≡
+(\fgx.fx(gx))(\xy.yx) ~~>
+\gx.(\xy.yx)x(gx) ~~>
+\gx.(gx)x ≡
+W</code></pre>
+
+Ok, here comes a shift in thinking. Instead of defining combinators as equivalent to certain lambda terms,
+we can define combinators by what they do. If we have the I combinator followed by any expression X,
+I will take that expression as its argument and return that same expression as the result. In pictures,
+
+ IX ~~> X
+
+Thinking of this as a reduction rule, we can perform the following computation
+
+ II(IX) ~~> IIX ~~> IX ~~> X
+
+The reduction rule for K is also straightforward:
+
+ KXY ~~> X
+
+That is, K throws away its second argument. The reduction rule for S can be constructed by examining
+the defining lambda term:
+
+<pre><code>S ≡ \fgx.fx(gx)</code></pre>
+
+S takes three arguments, duplicates the third argument, and feeds one copy to the first argument and the second copy to the second argument. So:
+
+ SFGX ~~> FX(GX)
+
+If the meaning of a function is nothing more than how it behaves with respect to its arguments,
+these reduction rules capture the behavior of the combinators S, K, and I completely.
+We can use these rules to compute without resorting to beta reduction.
+
+For instance, we can show how the I combinator is equivalent to a
+certain crafty combination of Ss and Ks:
+
+ SKKX ~~> KX(KX) ~~> X
+
+So the combinator `SKK` is equivalent to the combinator I.
+
+These reduction rule have the same status with respect to Combinatory
+Logic as beta reduction and eta reduction, etc., have with respect to
+the lambda calculus: they are purely syntactic rules for transforming
+one sequence of symbols (e.g., a redex) into another (a reduced
+form). It's worth noting that the reduction rules for Combinatory
+Logic are considerably more simple than, say, beta reduction. Since
+there are no variables in Combiantory Logic, there is no need to worry
+about variable collision.
+
+Combinatory Logic is what you have when you choose a set of combinators and regulate their behavior with a set of reduction rules. As we said, the most common system uses S, K, and I as defined here.
+
+###The equivalence of the untyped lambda calculus and combinatory logic###
+
+We've claimed that Combinatory Logic is equivalent to the lambda
+calculus. If that's so, then S, K, and I must be enough to accomplish
+any computational task imaginable. Actually, S and K must suffice,
+since we've just seen that we can simulate I using only S and K. In
+order to get an intuition about what it takes to be Turing complete,
+recall our discussion of the lambda calculus in terms of a text editor.
+A text editor has the power to transform any arbitrary text into any other arbitrary text. The way it does this is by deleting, copying, and reordering characters. We've already seen that K deletes its second argument, so we have deletion covered. S duplicates and reorders, so we have some reason to hope that S and K are enough to define arbitrary functions.
+
+We've already established that the behavior of combinatory terms can
+be perfectly mimicked by lambda terms: just replace each combinator
+with its equivalent lambda term, i.e., replace I with `\x.x`, replace
+K with `\fxy.x`, and replace S with `\fgx.fx(gx)`. So the behavior of
+any combination of combinators in Combinatory Logic can be exactly
+reproduced by a lambda term.
+
+How about the other direction? Here is a method for converting an
+arbitrary lambda term into an equivalent Combinatory Logic term using
+only S, K, and I. Besides the intrinsic beauty of this mapping, and
+the importance of what it says about the nature of binding and
+computation, it is possible to hear an echo of computing with
+continuations in this conversion strategy (though you wouldn't be able
+to hear these echos until we've covered a considerable portion of the
+rest of the course). In addition, there is a direct linguistic
+appliction of this mapping in chapter 17 of Barker and Shan 2014,
+where it is used to establish a correpsondence between two natural
+language grammars, one of which is based on lambda-like abstraction,
+the other of which is based on Combinatory Logic like manipulations.
+
+Assume that for any lambda term T, [T] is the equivalent combinatory logic term. The we can define the [.] mapping as follows:
+
+ 1. [a] a
+ 2. [(M N)] ([M][N])
+ 3. [\a.a] I
+ 4. [\a.M] KM assumption: a does not occur free in M
+ 5. [\a.(M N)] S[\a.M][\a.N]
+ 6. [\a\b.M] [\a[\b.M]]
+
+It's easy to understand these rules based on what S, K and I do. The first rule says
+that variables are mapped to themselves.
+The second rule says that the way to translate an application is to translate the
+first element and the second element separately.
+The third rule should be obvious.
+The fourth rule should also be fairly self-evident: since what a lambda term such as `\x.y` does it throw away its first argument and return `y`, that's exactly what the combinatory logic translation should do. And indeed, `Ky` is a function that throws away its argument and returns `y`.
+The fifth rule deals with an abstract whose body is an application: the S combinator takes its next argument (which will fill the role of the original variable a) and copies it, feeding one copy to the translation of \a.M, and the other copy to the translation of \a.N. This ensures that any free occurrences of a inside M or N will end up taking on the appropriate value. Finally, the last rule says that if the body of an abstract is itself an abstract, translate the inner abstract first, and then do the outermost. (Since the translation of [\b.M] will not have any lambdas in it, we can be sure that we won't end up applying rule 6 again in an infinite loop.)
+
+[Fussy notes: if the original lambda term has free variables in it, so will the combinatory logic translation. Feel free to worry about this, though you should be confident that it makes sense. You should also convince yourself that if the original lambda term contains no free variables---i.e., is a combinator---then the translation will consist only of S, K, and I (plus parentheses). One other detail: this translation algorithm builds expressions that combine lambdas with combinators. For instance, the translation of our boolean false `\x.\y.y` is `[\x[\y.y]] = [\x.I] = KI`. In the intermediate stage, we have `\x.I`, which mixes combinators in the body of a lambda abstract. It's possible to avoid this if you want to, but it takes some careful thought. See, e.g., Barendregt 1984, page 156.]
+
+[Various, slightly differing translation schemes from combinatorial
+logic to the lambda calculus are also possible. These generate
+different metatheoretical correspondences between the two
+calculii. Consult Hindley and Seldin for details. Also, note that the
+combinatorial proof theory needs to be strengthened with axioms beyond
+anything we've here described in order to make [M] convertible with
+[N] whenever the original lambda-terms M and N are convertible. But
+then, we've been a bit cavalier about giving the full set of reduction
+rules for the lambda calculus in a similar way. For instance, one
+issue is whether reduction rules (in either the lambda calculus or
+Combinatory Logic) apply to embedded expressions. Generally, we want
+that to happen, but making it happen requires adding explicit axioms.]
+
+Let's check that the translation of the false boolean behaves as expected by feeding it two arbitrary arguments:
+
+ KIXY ~~> IY ~~> Y
+
+Throws away the first argument, returns the second argument---yep, it works.
+
+Here's a more elaborate example of the translation. The goal is to establish that combinators can reverse order, so we use the **T** combinator, where <code>T ≡ \x\y.yx</code>:
+
+ [\x\y.yx] = [\x[\y.yx]] = [\x.S[\y.y][\y.x]] = [\x.(SI)(Kx)] = S[\x.SI][\x.Kx] = S(K(SI))(S[\x.K][\x.x]) = S(K(SI))(S(KK)I)
+
+We can test this translation by seeing if it behaves like the original lambda term does.
+The orginal lambda term lifts its first argument (think of it as reversing the order of its two arguments):
+
+ S(K(SI))(S(KK)I) X Y ~~>
+ (K(SI))X ((S(KK)I) X) Y ~~>
+ SI ((KK)X (IX)) Y ~~>
+ SI (KX) Y ~~>
+ IY (KXY) ~~>
+ Y X
+
+Voilà: the combinator takes any X and Y as arguments, and returns Y applied to X.
+
+One very nice property of combinatory logic is that there is no need to worry about alphabetic variance, or
+variable collision---since there are no (bound) variables, there is no possibility of accidental variable capture,
+and so reduction can be performed without any fear of variable collision. We haven't mentioned the intricacies of
+alpha equivalence or safe variable substitution, but they are in fact quite intricate. (The best way to gain
+an appreciation of that intricacy is to write a program that performs lambda reduction.)
+
+Back to linguistic applications: one consequence of the equivalence between the lambda calculus and combinatory
+logic is that anything that can be done by binding variables can just as well be done with combinators.
+This has given rise to a style of semantic analysis called Variable Free Semantics (in addition to
+Szabolcsi's papers, see, for instance,
+Pauline Jacobson's 1999 *Linguistics and Philosophy* paper, "Towards a variable-free Semantics").
+Somewhat ironically, reading strings of combinators is so difficult that most practitioners of variable-free semantics
+express their meanings using the lambda-calculus rather than combinatory logic; perhaps they should call their
+enterprise Free Variable Free Semantics.
+
+A philosophical connection: Quine went through a phase in which he developed a variable free logic.
+
+ Quine, Willard. 1960. "Variables explained away" <cite>Proceedings of the American Philosophical Society</cite>. Volume 104: 343--347. Also in W. V. Quine. 1960. <cite>Selected Logical Papers</cite>. Random House: New
+ York. 227--235.
+
+The reason this was important to Quine is similar to the worries that Jim was talking about
+in the first class in which using non-referring expressions such as Santa Claus might commit
+one to believing in non-existant things. Quine's slogan was that "to be is to be the value of a variable."
+What this was supposed to mean is that if and only if an object could serve as the value of some variable, we
+are committed to recognizing the existence of that object in our ontology.
+Obviously, if there ARE no variables, this slogan has to be rethought.
+
+Quine did not appear to appreciate that Shoenfinkel had already invented combinatory logic, though
+he later wrote an introduction to Shoenfinkel's key paper reprinted in Jean
+van Heijenoort (ed) 1967 <cite>From Frege to Goedel, a source book in mathematical logic, 1879--1931</cite>.
+
+Cresswell has also developed a variable-free approach of some philosophical and linguistic interest
+in two books in the 1990's.
+
+A final linguistic application: Steedman's Combinatory Categorial Grammar, where the "Combinatory" is
+from combinatory logic (see especially his 2000 book, <cite>The Syntactic Processs</cite>). Steedman attempts to build
+a syntax/semantics interface using a small number of combinators, including T ≡ `\xy.yx`, B ≡ `\fxy.f(xy)`,
+and our friend S. Steedman used Smullyan's fanciful bird
+names for the combinators, Thrush, Bluebird, and Starling.
+
+Many of these combinatory logics, in particular, the SKI system,
+are Turing complete. In other words: every computation we know how to describe can be represented in a logical system consisting of only a single primitive operation!
+
+Here's more to read about combinatorial logic.
+Surely the most entertaining exposition is Smullyan's [[!wikipedia To_Mock_a_Mockingbird]].
+Other sources include
+
+* [[!wikipedia Combinatory logic]] at Wikipedia
+* [Combinatory logic](http://plato.stanford.edu/entries/logic-combinatory/) at the Stanford Encyclopedia of Philosophy
+* [[!wikipedia SKI combinatory calculus]]
+* [[!wikipedia B,C,K,W system]]
+* [Chris Barker's Iota and Jot](http://semarch.linguistics.fas.nyu.edu/barker/Iota/)
+* Jeroen Fokker, "The Systematic Construction of a One-combinator Basis for Lambda-Terms" <cite>Formal Aspects of Computing</cite> 4 (1992), pp. 776-780.
+<http://people.cs.uu.nl/jeroen/article/combinat/combinat.ps>
We need to do some work to show how to represent some of the functions
we've become acquainted with.
-
+<a id=booleans></a>
## Booleans ##
We'll start with the `if ... then ... else ...` construction we saw last week:
You should also be experimenting with this site's [[lambda evaluator|code/lambda evaluator]].
+<a id=tuples></a>
## Tuples ##
In class, we also showed you how to encode a tuple in the Lambda Calculus. We did it with an ordered triple, but the strategy generalizes in a straightforward way. (Some authors just use this strategy to define *pairs*, then define triples as pairs whose second member is another pair, and so on. Yech. If you keep a firm grip on your wits, that can also be made to work, but it's extremely likely that people who code in that way are going to lose their grip at some point and get themselves in a corner where they'll regret having made that decision about how to encode triples. And they will be forced to add further complexities at later points, that they're probably not anticipating now. The strategy presented here is as elegant as it first looks, and will help you program more hygienically even when your attention lapses.)
Our proposal was to define the triple `(a, b, c)` as:
- \f. f a b c
+ \h. h a b c
To extract the first element of this, you'd write:
- (\f. f a b c) fst_of_three
+ (\h. h a b c) fst_of_three
where `fst_of_three` is the function `\x y z. x`:
- (\f. f a b c) (\x y z. x) ~~>
+ (\h. h a b c) (\x y z. x) ~~>
(\x y z. x) a b c ~~>
(\y z. a) b c ~~>
(\z. a) c ~~>
Here are the corresponding definitions in Scheme (Racket):
(define make-triple (lambda (a) (lambda (b) (lambda (c)
- (lambda (f) (((f a) b) c))))))
+ (lambda (h) (((h a) b) c))))))
(define fst_of_three (lambda (x) (lambda (y) (lambda (z) x))))
(define snd_of_three (lambda (x) (lambda (y) (lambda (z) y))))
If you really want to, you can disguise what's going on like this:
- (define lifted-fst_of_three (lambda (p) (p fst_of_three)))
+ (define lifted-fst_of_three (lambda (trip) (trip fst_of_three)))
Then you could say:
- (lifted-fst_of_three p)
+ (lifted-fst_of_three t)
instead of:
- (p fst_of_three)
+ (t fst_of_three)
Of course, the last is still what's happening under the hood.
(Remark: `(lifted-f (((make-triple 10) 20) 30))` stands to `((((make-triple 10) 20) 30) f)` as
`((((make-triple 10) 20) 30) f)` stands to `(((f 10) 20) 30)`.)
+
+### Curried and Uncurried functions in the Lambda Calculus ###
+
+As we've explained before, an *uncurried* function is one that takes multiple arguments in a single bundle, as a tuple, like this:
+
+ f (x, y, z)
+
+Whereas a *curried* function is one that takes multiple arguments in sequence, like this:
+
+ g x y z
+
+That is, `g` is a function expecting one argument (here `x`), that evaluates to a second function, that itself expects another argument (here `y`), and so on. (So `g` is a *higher-order function*: the result of applying it to argument `x` returns another function.) In discussing Kapulet and Scheme and OCaml and Haskell, we sometimes worked with uncurried functions, and other times with curried ones. Now that you've seen how to build and work with tuples in the Lambda Calculus, you can write uncurried functions there too. That is, you can write functions `f` that will expect arguments of the form `\h. h x y z`. But in the end, `f` is going to have to apply that argument to some auxiliary handler function `g` anyway, where `g` takes *its* arguments in curried form. So if you can, in the Lambda Calculus it's easiest to just work with curried functions like `g` in the first place, rather than uncurried, tuple-expecting arguments like `f`.
+
+In some cases you can't do this, because you'll be partaking of some general pattern that only makes room for a single argument --- like the "starting value" `z` in the `fold_right` function discussed below; yet you're performing some task that really requires you to stuff a couple of values into that position. Tuples are ideal for that purpose. But in for run-of-the-mill functions you're defining in the Lambda Calculus, if multiple arguments need to be passed to a function, and it's up to you whether to pass them in curried or uncurried/tuple style, you should default to the curried style (as in, `g x y z`). That's the more idiomatic, native style for passing arguments in the Lambda Calculus.
+
+
+<a id=lists></a>
## Lists ##
There are multiple ways to encode lists, and also multiple ways to encode numbers. We are going to start with what we think are the most natural and elegant encodings. Historically these were the first encodings of numbers but not of lists.
\f z. f a (f b (f c z))
-Here we work with curried functions, because that's how the Lambda Calculus does things. You wouldn't want to build up a tuple using the mechanisms described above, and then supply `f` as an argument to that tuple, and so on. That would be a lot of red tape for no benefit. In the Lambda Calculus, it's simpler to just work with curried functions as our natural idiom.
+Here we assume `f` to be a curried function, taking its arguments in the form `f c z` rather that `f (c, z)` (that is, `f (\h. h c z)`), because as we explained at the end of the section on Tuples, the curried form is the idiomatic and native style for passing multiple arguments in the Lambda Calculus.
So if `[a, b, c]` should be the displayed higher-order function above, what should `[c]` be? Evidently:
which looks like what we want, a higher-order function that will take an `f` and a `z` as arguments and then return the right fold of those arguments over `[g a, g b, g c]`, which is `map g [a, b, c]`.
+<a id=numbers></a>
## Numbers ##
Armed with the encoding we developed for lists above, Church's method for encoding numbers in the Lambda Calculus is very natural. But this is not the order that these ideas were historically developed.