From 82558787dab095c164d4a6d2cdfceebc9b335698 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sun, 19 Sep 2010 18:47:13 -0400 Subject: [PATCH] week2: ~~>_eta Signed-off-by: Jim Pryor --- week2.mdwn | 2 ++ 1 file changed, 2 insertions(+) diff --git a/week2.mdwn b/week2.mdwn index 1e3aa2bc..eedc6de0 100644 --- a/week2.mdwn +++ b/week2.mdwn @@ -318,6 +318,8 @@ will eta-reduce by n steps to: \x. M +When we add eta-reduction to our proof system, we end up reconstruing the meaning of `~~>` and `<~~>` and "normal form", all in terms that permit eta-reduction as well. Sometimes these expressions will be annotated to indicate whether only beta-reduction is allowed (~~>β) or whether both beta- and eta-reduction is allowed (~~>βη). + The logical system you get when eta-reduction is added to the proof system has the following property: > if `M`, `N` are normal forms with no free variables, then M ≡ N iff `M` and `N` behave the same with respect to every possible sequence of arguments. -- 2.11.0