Feasible Functions over Co-inductive Data

13 years 10 months ago
Feasible Functions over Co-inductive Data
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 coinductive 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+ ∗ .
Ramyaa Ramyaa, Daniel Leivant
Added 11 Jul 2010
Updated 11 Jul 2010
Type Conference
Year 2010
Authors Ramyaa Ramyaa, Daniel Leivant
Comments (0)