Home » forums » LtU Forum

"Very linear" lambda calculus

What 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))
=\abc.B a (B b c)
=\ab.B (B a) (B b)
=\a.B (B (B a)) B

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))
=\abc.B (B a b) c
=\ab.B (B a b)
=\a.B B (B a)
=B (B B) B

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

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Read proof-theoretically,

composition and identity are the Cut and the Identity principles of an intuitionistic (ie, single-conclusion) sequent calculus, and the arrow is some kind implication (i.e., an internalized entailment). Since presumably you're okay with currying, it seems like you want a multiple-hypothesis calculus.

However, if you want to think about banishing exchange in addition to weakening and contraction, then you should look at a fragment of the Lambek calculus. Here's one -- the loss of exchange means the context here isn't merely linear, it's also ordered.

A ::= P | A -o B


------- Ident
P |- P

 Gamma, A |- B
----------------  -oR
 Gamma |- A -o B

Gamma |- A   B, Delta |- C
-------------------------- -oL 
A -o B, Gamma, Delta |- C

Cut is an admissible principle for this calculus (email me if you want
the proof):

Gamma |- A   A, Gamma' |- B
---------------------------- Cut
     Gamma, Gamma' |- B

Now, the trick is to try and translate derivations into combinator expressions -- and I ran into trouble in the -oL case:

[[D :: Ident]]                 = I
[[-oR(D') :: Gamma |- A -o B]] = [[D']]
[[-oL(D1,D2) :: Gamma, A -o B, Gamma' |- C]] = 
    Note D1 :: Gamma |- A
    Note D2 :: B, Gamma' |- C
    So  [[D1]] :: (Gamma -o A) 
    and [[D2]] :: (B -o Gamma' -o C) 
    So we want some d : (A -o B) -o Gamma -o Gamma' -o C. 
    So if we define:
        LEFT == \d2 d1 f : A -o B. d2 o f o d1
    Then we can define the translation to yield:
       LEFT [[D2]] [[D1]]

Note in the last case the left combinator permutes the order of its variables -- f is bound last, but it's used second in the combinator above. So to do bracket abstraction on LEFT, you really need the C combinator. However, if we also had the reverse composition operator, then we could write:

LEFT d2 d1 f = d2 o (d1; f)

and then

[[-oL(D1,D2) :: Gamma, A -o B, Gamma' |- C]] = LEFT [[D2]] [[D1]]

and bracket abstraction could give a good term for this.

There might be some more clever trick than this, but I'm not a combinator expert, so this is all I've got. :)

By neelk at Thu, 2008-09-18 07:27 | login or register to post comments