Intensional properties of polygraphs

Abstract

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 and non-deterministic polynomial time functions.

Proceedings of TERMGRAPH 2007, Electronic Notes in Computer Science (to appear), 12 pages, minor changes from previous version

References in corpus (3)

• Termination orders for 3-dimensional rewriting
• The three dimensions of proofs
• Polygraphs for termination of left-linear term rewriting systems

Cited by in corpus (2)

• Higher-dimensional categories with finite derivation type
• Polygraphic programs and polynomial-time functions