User loginNavigation 
"Very linear" lambda calculusWhat portion of linear lambda calculus corresponds to using only the B and I combinators (composition and identity)? I have a hunch that it's all lambda terms that use their input variables exactly once and without permuting them, but I'm finding it hard to prove that. The standard abstraction elimination algorithm doesn't work to give a combinator: \abcd.a(b(cd)) and to eliminate the variable "a" here, I need to use the C combinator. But there is a combinator that is extensionally equivalent that doesn't use C: \abcd.a(b(cd)) It depends on using the associativity of composition. How can I tell which linear terms are in the span of B and I? By mikestay at 20080917 17:57  LtU Forum  previous forum topic  next forum topic  other blogs  3498 reads

Browse archivesActive forum topics 
Recent comments
3 hours 58 min ago
3 hours 58 min ago
4 hours 10 min ago
10 hours 16 min ago
10 hours 53 min ago
11 hours 45 sec ago
14 hours 7 min ago
16 hours 51 min ago
18 hours 9 min ago
18 hours 46 min ago