complexity

• To: linear@cs.stanford.edu
• Subject: complexity
• From: lafont@lmd7.univ-mrs.fr
• Date: Sun, 31 Oct 93 13:25:34 +0100
• Approved: types@dcs.gla.ac.uk

Does anybody know the complexity of provability for non commutative  
multiplicative linear logic with units but without atoms?

 The formulae are built from Unit and Bottom using Times and Par.
 The rules are:

                    |- GAMMA, A, GAMMA'    |- DELTA, B, DELTA' 

    -------         ------------------------------------------
    |- Unit         |- DELTA, GAMMA, A Times B, DELTA', GAMMA'

        |- GAMMA, GAMMA'              |- GAMMA, A, B, GAMMA'
    ------------------------         -------------------------
    |- GAMMA, Bottom, GAMMA'         |- GAMMA, A Par B, GAMMA'

 In the Times rule, GAMMA' or DELTA must be empty.

Yves Lafont <lafont@lmd.univ-mrs.fr>.

• Prev: Parametricity and Local Variables
• Next: lambda - a program for solving lambda definability problems
• Index(es):
  • Main
  • Thread