Polygraphic programs and polynomial-time functions

Abstract

We study the computational model of polygraphs. For that, we consider polygraphic programs, a subclass of these objects, as a formal description of first-order functional programs. We explain their semantics and prove that they form a Turing-complete computational model. Their algebraic structure is used by analysis tools, called polygraphic interpretations, for complexity analysis. In particular, we delineate a subclass of polygraphic programs that compute exactly the functions that are Turing-computable in polynomial time.

Logical Methods in Computer Science (to appear), 37 pages, 1 colour picture, corrected typos

References in corpus (5)

• Light types for polynomial time computation in lambda-calculus
• Termination orders for 3-dimensional rewriting
• The three dimensions of proofs
• Two polygraphic presentations of Petri nets
• Intensional properties of polygraphs

Cited by in corpus (1)

• Data Structures for Topologically Sound Higher-Dimensional Diagram Rewriting