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 2008-09-17 17:57 | LtU Forum | previous forum topic | next forum topic | other blogs | 4858 reads
|
Browse archivesActive forum topics |
Recent comments
7 weeks 3 days ago
7 weeks 4 days ago
7 weeks 6 days ago
14 weeks 6 days ago
20 weeks 4 days ago
20 weeks 5 days ago
21 weeks 4 days ago
24 weeks 2 days ago
25 weeks 5 days ago
25 weeks 5 days ago