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  6338 reads

Browse archivesActive forum topics 
Recent comments
1 hour 19 min ago
1 hour 19 min ago
1 hour 55 min ago
3 hours 30 min ago
5 hours 48 min ago
8 hours 37 min ago
9 hours 13 min ago
10 hours 3 min ago
16 hours 40 min ago
16 hours 45 min ago