Using program schemes to logically capture polynomial-time on certain classes of structures
Iain A. Stewart · 2013
We continue the study of the expressive power of certain classes of program schemes on finite structures, in relation to more mainstream logics studied in finite model theory and to computational complexity. We show that there exists a program scheme, whose constructs are assignments and while-loops with quantifier-free tests and which has access to a stack, that can solve a P-complete problem, the deterministic path system problem, even in the absence of non-determinism so long as problem instances are presented in a functional style. Our proof leans heavily on Cook's proof that the classes of formal languages accepted by deterministic and non-deterministic pushdown automata coincide. However, we then show how our program scheme in the above rather esoteric result can be used to build a successor relation in certain classes of structures, namely: the class of strongly-connected locally ordered digraphs; the class of connected planar embeddings; and the class of triangulations, with the...