Elementary Complexity and Geometry of Interaction

Issue title: Typed Lambda Calculi and Applications (TLCA'99)

Article type: Research Article

Authors: Baillot, Patrick | Pedicini, Marco

Abstract: We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution (following [10]) into which proofs of Elementary Linear Logic can be interpreted. In order to extend geometry of interaction computation (the so called execution formula) to a wider class of programs in the algebra than just those coming from proofs, we define a variant of execution (called weak execution). Its application to any program of clauses is shown to terminate with a bound on the number of steps which is elementary in the size of the program. We establish that weak execution coincides with standard execution on programs coming from proofs.

Keywords: Elementary Linear Logic, Geometry of interaction, Proof-nets, Complexity, Semantics

Journal: Fundamenta Informaticae, vol. 45, no. 1-2, pp. 1-31, 2001