From: jim Date: Sat, 7 Feb 2015 22:41:18 +0000 (-0500) Subject: tweak final note X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=4ab26de71d9694f5a65a80cd87d11734cc6aa02b tweak final note --- diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn index 5bb69d62..6df82916 100644 --- a/topics/week2_encodings.mdwn +++ b/topics/week2_encodings.mdwn @@ -405,15 +405,17 @@ The encoding for `0` can also be written as `\f z. z`, which we've also proposed Given the above, can you figure out how to define the `succ` function? We already worked through the definition of `cons`, and this is just a simplification of that, so you should be able to do it. We'll make it a homework. -We saw that using the `cons` operation and `[]` as arguments to `fold_right` over a list gave us back that very same list. In the Lambda Calculus, that would come down to: +We saw that using the `cons` operation (Kapulet's `&`) and `[]` as arguments to `fold_right` over a list give us back that very same list. In the Lambda Calculus, that comes to the following: [a, b, c] cons [] -with the appropriate lambda terms substituted throughout, would just reduce to the same lambda term we used to encode `[a, b, c]`. What do you think this would reduce to: +with the appropriate lambda terms substituted throughout, just reduces to the same lambda term we used to encode `[a, b, c]`. + +In the same spirit, what do you expect this will reduce to: 3 succ 0 -with the appropriate lambda terms substituted throughout? Since 3 is `\f z. f (f (f z))`, it should reduce to whatever: +Since 3 is `\f z. f (f (f z))`, it should reduce to whatever: succ (succ (succ 0))