Intensional properties of polygraphs

Guillaume Bonfante (1) , Yves Guiraud (2)

1 CARTE - Theoretical adverse computations, and safety
2 PROTHEO - Constraints, automatic deduction and software properties proofs

We present polygraphic programs, a subclass of Albert Burroni's polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We prove that the model is Turing complete. We use polygraphic interpretations, a termination proof method introduced by the second author, to characterize polygraphic programs that compute in polynomial time. We conclude with a characterization of polynomial time functions.

Mots clés: Polygraph; Polygraphic program; Polygraphic interpretation; Computability; Complexity; Polynomial time

Domaines: Logique en informatique [cs.LO]; Langage de programmation [cs.PL]; Catégories et ensembles [math.CT]

Guillaume Bonfante, Yves Guiraud. Intensional properties of polygraphs. 4th International Workshop on Computing with Terms and Graphs - TERMGRAPH 2007, Mar 2007, Braga, Portugal. ⟨10.1016/j.entcs.2008.03.034⟩. ⟨inria-00129391v3⟩