Elementary complexity and geometry of interaction

• Autorzy: Baillot P. , Pedicini M.
• Języki publikacji: EN

Abstrakty

EN

We introduce a geometry of interaction model given by an algebra of clauses equipped with resolution 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.

Słowa kluczowe

EN

Elementary Linear Logic; geometry of interaction; proof nets; complexity; semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2001
• Tom: Vol. 45, nr 1,2
• Strony: 1--31
• Opis fizyczny: bibliogr. 16 poz.

Twórcy

autor

Baillot P.

autor

Pedicini M.

• Université Aix-Marseille II CMI(LIM-FRE 2246) 39 rue Joilot-Curie, 13453 Marseille Cedex 13, France,