nLab bounded linear logic

Idea

Bouded Linear Logic (BLL) is a refinement of linear logic (LL) where derelictions are annotated with a natural number indicating the number of times the associated resource can be used.

This way, well-typed functions do not only satisfy the basic input/output specification (as in the simply-typed lambda calculus), but also a temporal specification, without the need for a Turing machine with a clock.

Theorem. A function from dyadic integers to dyadic integers is computable in polynomial time in the length of its input if and only if it is typable in BLL.

The expressive power of BLL thus lies between that of rudimentary linear logic? (RLL)—which is sequent calculus without the weakening rule and without the contraction rule—and full linear logic.

Related logical systems

Ugo dal Lago and Martin Hofmann have proposed a variant of BLL called QBAL, which allows for quantification over resource variables and is also sound and complete for polynomial time.

When the derelictions are annotated with an element of a(n ordered) semiring $\mathcal{S}$, we obtain graded linear logic ($\mathrm{G}_\mathcal{S}\mathrm{LL}$).

Related concepts

• complexity class
• graded modality

References

• Jean-Yves Girard, Andre Scedrov, Philip J. Scott, Bounded linear logic: a modular approach to polynomial-time computability, Theoretical Computer Science Volume 97, Issue 1, 20 April 1992, Pages 1-66 (doi:10.1016/0304-3975(92)90386-T)

• Ugo Dal Lago, Martin Hofmann, Bounded Linear Logic, Revisited, Logical Methods in Computer Science, Volume 6, Issue 4 (December 18, 2010) lmcs:1064 (arXiv:0904.2675)

• Bounded Linear Logic Workshop, Fontainebleau, 2-4 December 2013, (webpage)