From: Jim Pryor Date: Sun, 19 Sep 2010 18:50:51 +0000 (-0400) Subject: week2 tweaks X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=0510616ec71c740ec9340b77b207e44e87a3ee2c week2 tweaks Signed-off-by: Jim Pryor --- diff --git a/week2.mdwn b/week2.mdwn index b43576f0..0aa23fc0 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -321,7 +321,7 @@ This question highlights that there are different choices to make about how eval With regard to Q3, it should be intuitively clear that `\x. M x` and `M` will behave the same with respect to any arguments they are given. It can also be proven that no other functions can behave differently with respect to them. However, the logical system you get when eta-reduction is added to the proof theory is importantly different from the one where only beta-reduction is permitted. -If we answer Q2 by permitting reduction inside abstracts, and we also permit eta-reduction, then where none of y1, ..., yn occur free in M, this: +If we answer Q2 by permitting reduction inside abstracts, and we also permit eta-reduction, then where none of y1, ..., yn occur free in M, this: 
\x y1... yn. M y1... yn