Characterizing polynomial and exponential complexity classes in elementary lambda-calculus

In this paper an implicit characterization of the complexity classes k - EXP and k - FEXP, for k ≥ 0, is given, by a type assignment system for a stratified λ-calculus, where types for programs are witnesses of the corresponding complexity class. Types are formulae of Elementary Linear Logic (ELL), and the hierarchy of complexity classes k - EXP is characterized by a hierarchy of types.

Authors

• Patrick Baillot
• Erika De Benedetti
• Simona Ronchi Della Rocca

Keywords

• Implicit computational complexity
• Linear logic
• Lambda-calculus