zbMATH — the first resource for mathematics

Feasible functions over co-inductive data. (English) Zbl 1305.68088
Dawar, Anuj (ed.) et al., Logic, language, information and computation. 17th international workshop, WoLLIC 2010, Brasilia, Brazil, July 6–9, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13823-2/pbk). Lecture Notes in Computer Science 6188. Lecture Notes in Artificial Intelligence, 191-203 (2010).
Summary: Proof theoretic characterizations of complexity classes are of considerable interest because they link levels of conceptual abstraction to computational complexity. We consider here the provability of functions over co-inductive data in a highly expressive, yet proof-theoretically weak, variant of second order logic \(L^{+}_{*}\), which we believe captures the notion of feasibility more broadly than previously considered pure-logic formalisms.
Our main technical result is that every basic feasible functional (i.e. functional in the class BFF, believed to be the most adequate definition of feasibility for second-order functions) is provable in \(L^{+}_{*}\).
For the entire collection see [Zbl 1196.03005].

68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)
03B15 Higher-order logic; type theory (MSC2010)
03F10 Functionals in proof theory
Full Text: DOI