From 6abd50b9958bc175a407cc4f0fe0d2f5982f1d7c Mon Sep 17 00:00:00 2001 From: jim Date: Sat, 7 Feb 2015 17:38:40 -0500 Subject: [PATCH] final note --- topics/week2_encodings.mdwn | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/topics/week2_encodings.mdwn b/topics/week2_encodings.mdwn index c345ac04..5bb69d62 100644 --- a/topics/week2_encodings.mdwn +++ b/topics/week2_encodings.mdwn @@ -405,4 +405,19 @@ 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: + + [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: + + 3 succ 0 + +with the appropriate lambda terms substituted throughout? Since 3 is `\f z. f (f (f z))`, it should reduce to whatever: + + succ (succ (succ 0)) + +does. And if we define `succ` properly, we should expect that to give us the same lambda term that we used to encode `3` in the first place. + + We'll look at other encodings of lists and numbers later. -- 2.11.0