author jim Sat, 14 Feb 2015 18:12:08 +0000 (13:12 -0500) committer Linux User Sat, 14 Feb 2015 18:12:08 +0000 (13:12 -0500)
 topics/week3_church_arithmetic.mdwn [new file with mode: 0644] patch | blob

diff --git a/topics/week3_church_arithmetic.mdwn b/topics/week3_church_arithmetic.mdwn
new file mode 100644 (file)
index 0000000..9856043
--- /dev/null
@@ -0,0 +1,60 @@
+We're continuing to assume Church's encodings of the numbers:
+
+`0` &equiv; `\f z. z`, which is (convertible with) <code>\f z. f<sup>0</sup> z</code>
+`1` &equiv; `\f z. f z`, which is (syntactically identical to) <code>\f z. f<sup>1</sup> z</code>
+`2` &equiv; `\f z. f (f z)`, which is <code>\f z. f<sup>2</sup> z</code>
+`3` &equiv; `\f z. f (f (f z))`, which is <code>\f z. f<sup>3</sup> z</code>
+
+One of your homework problems for last week was to define `succ` for this encoding. Here is how we do it:
+
+    \n. \f z. f (n f z)
+
+Now how shall we define more advanced arithmetic functions, such as addition?
+
+Let's recall the structural similarity between this encoding of the numbers and our right-fold encoding of lists. If we feed the number `3` the `succ` function and `0` as its arguments, we get:
+
+    succ (succ (succ 0))
+
+as a result, and that will reduce to `\f z. f (f (f z))`, the same number with which we began. This parallels the fact that if we feed the `cons` function and `[]` as arguments to our encoded list `[a, b, c]`, we get:
+
+    cons a (cons b (cons c []))
+
+as a result, and that will reduce to `\f z. f a (f b (f c z))`, the same list with which we began. You may recall that if you supply `cons` plus a *non*-empty list as arguments to a right-fold operation, the result is
+
+    [a, b, c] cons [d, e] ~~>
+    cons a (cons b (cons c [d, e]))
+
+which will reduce to `[a, b, c] && [d, e]`, that is `[a, b, c, d, e]` or `\f z. f a (f b (f c (f d (f e z))))`. What if we did the analogous thing to our Church number? That is, what do we get if instead of `3 succ 0` we evaluate `3 succ 2`? That will be:
+
+    succ (succ (succ 2))
+
+or <code>succ<sup>3</sup> 2</code>, which will reduce to our encoding for `5`.
+
+In general, this can be our strategy for performing the addition `add 2 3`. We can define **add** as:
+
+    \l r. r succ l
+
+That lambda term cannot be further simplified, but we can prove inductively that when `l` and `r` have the form of Church-encoded numbers, the body of that abstract is convertible with `\f z. r f (l f z)`. So we can alternatively define **add** as:
+
+    \l r. \f z. r f (l f z)
+
+This corresponds to the natural extension of our "exponential" metalanguage shorthand:
+
+<code>f<sup>l<b>+</b>r</sup> z &equiv; f<sup>r</sup>(f<sup>l</sup> z)</code>
+
+(If you wonder why the `l`s and `r`s are in the specific orders they are here, the answer is that with `add` it doesn't matter, but the pattern begun here coheres better with the orders needed for other arithmetic functions to be described below.)
+
+If we knew how to encode `pred`, then we could define subtraction in a similar way: `sub l r` would just be <code>pred<sup>r</sup> l</code>, or `r pred l`. We'd have to decide what `pred 0` should reduce to. Perhaps some special error formula, or a free variable `err`, or perhaps just to `0` --- in the same spirit that it can be natural to make `tail []` just be `[]`. A more pressing issue is that we don't know yet how to define `pred`. And in fact, with Church's encoding of the numbers, this is not trivial. We discuss the issue and give you some guidance about how to do it in this week's homework. (With some other encodings of the numbers, it is more straightforward to define `pred`; but then those other encodings have other compensating disadvantages.)
+
+What about multiplication? Well, in general, `mul l r` should be the result of applying the (curried, partially applied) function `(add l)` to `0`, and then to apply `(add l)` again to the result, and again, ... for `r` times. In other words, it should be <code>(add l)<sup>r</sup> 0</code>. But given our encoding of `r`, that will just be `r (add l) 0`. And so we can define **mul** as:
+
+    \l r. r (add l) 0
+
+As with `add`, we can prove inductively that when `l` and `r` have the form of Church-encoded numbers, the body of that abstract is convertible with `\f z. r (l f) z`. So we can alternatively define **mul** as:
+
+    \l r. \f z. r (l f) z
+
+Interestingly, `mul l r` defined in this way eta-reduces to `\f. r (l f)`, which we also know as the *composition* <code>r &cir; l</code> of `r` with `l`.
+
+If we continue in this direction, we end up defining `l^r` (where `2^5` is `32`) either as `r (mul l) one` or as the *application* `r l` of `r` to `l`.
+