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=a74e125da6d29f39933f380fd6b0f91e9e4e3791 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