We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution (following [Gir95a]) into which proofs of Elementary Linear Logic can be interpreted. In order to extend geometry of interaction computation (Execution) to more programs of the algebra than just those coming from proofs, we dene 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.
CITATION STYLE
Baillot, P., & Pedicini, M. (1999). Elementary complexity and geometry of interaction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1581, pp. 25–39). Springer Verlag. https://doi.org/10.1007/3-540-48959-2_4
Mendeley helps you to discover research relevant for your work.