X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=week2.mdwn;h=0aa23fc0754fde6a702a4b5961a3343e8b5b6ab3;hp=b43576f0b0e8d688eabad988701eb82e3446d4b0;hb=0510616ec71c740ec9340b77b207e44e87a3ee2c;hpb=bd678a0313adab5841c9f346ea250b1de0d755ec 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