User loginNavigation 
Î², Î·, Î¾ âŠ¢ Î±?I was just struck with a minor revelation. The informal explanation for Î±equivalence in Î»calculus is that a function "does the same thing" regardless of the particular names that we might choose for its internal variables. But this seems like just a particular case of the general extensionality principle! Technically, Î±conversion means that a bound variable may be renamed to another one as long as no free variables are captured: y âˆ‰ FV(e) â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€• (Î±) Î»x. e = Î»y. e[y/x] And indeed, it turns out that in the presence of the Î·rule, which expresses the extensionality principle, the above rule is derivable: y âˆ‰ FV(e) â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€• â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€• (Î²) y âˆ‰ FV(Î»x. e) (Î»x. e) y = e[y/x] â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€• (Î·) â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€•â€• (Î¾) Î»x. e = Î»y. (Î»x. e) y = Î»y. e[y/x] This is of course quite trivial. However, I've read a fair number of tutorials to Î»calculus, and I don't recall having ever seen this particular tidbit mentioned anywhere. I'm unsure whether this is because I just haven't read the right papers, or the matter is so trivial that no one bothers mentioning it explicitly, or there's something wrong with my reasoning. So, just to ease my mind, could someone please either direct me to some respectable source where the redundancy of Î± in the presence of Î· is confirmed, or else point out what I'm missing here? Thanks. By Lauri Alanko at 20081108 20:56  LtU Forum  previous forum topic  next forum topic  other blogs  6659 reads

Browse archivesActive forum topics 
Recent comments
58 min 9 sec ago
1 day 1 hour ago
1 day 2 hours ago
1 day 8 hours ago
2 days 1 hour ago
2 days 10 hours ago
2 days 21 hours ago
2 days 22 hours ago
2 days 22 hours ago
2 days 23 hours ago