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

Browse archivesActive forum topics 
Recent comments
1 hour 25 min ago
2 hours 29 min ago
4 hours 49 min ago
10 hours 21 min ago
11 hours 34 min ago
12 hours 4 min ago
13 hours 58 min ago
18 hours 3 min ago
19 hours 3 min ago
20 hours 29 min ago