4
$\begingroup$

An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length polynomial to the formula being proven) for all tautologies could be constructed iff $coNP$ = $NP$. Other results deal with specific propositional calculus proof systems, showing that they all have superpolynomial proof lower-bounds. Is there any work relating type systems and type inference rules to the proof systems as defined in this theory?

In general, a cursory examination reveals that most discussions of type systems discuss computability (decidability/undecidability) with little discussion of finer complexity bounds (which may well exist in many finite models). Is there a reason why this is so (if indeed it is so)?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Not an expert on proof complexity, but the type systems that type theorists discuss tend to be much more expressive than the classes that complexity theorists are interested in. E.g. the simply-typed λ-calculus with primitive recursion is probably the least expressive system type theory looks at, but every recursive function whose totality can be proved in first order logic (starting from the usual axioms for the elementary data types, eg Peano for natural numbers) can be expressed. The field of "implicit computational complexity" seeks to combine type theory with complexity theory. $\endgroup$
    – Martin Berger
    May 8, 2016 at 12:50

1 Answer 1

Reset to default
6
$\begingroup$

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories like Cook's theory $\mathsf{PV}$ (standing for polynomial-time verifiable), Buss's theory $\mathsf{S}^1_2$, ...

Cook and Urquhart used Cook's theory $\mathsf{PV}$ to define a theory of higher-types polynomial-time computable functions $\mathsf{PV}^\omega$ in the following paper:

There has been some follow up work which you can find by looking at articles citing this paper.

Implicit complexity theory that Martin mentions is also influenced by this work. Check out Simone Martini's survey slides and Ugo Dal Lago's survey article to get a picture of what is implicit complexity theory and its history.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thank you! The Cook-Urquhart paper is indeed the kind of work I was asking about. I also found the survey paper on implicit complexity enlightening, although I disagree with the (implied) characterization of machine-independent complexity as more fundamental than language-independent complexity, especially in light of the extended Church-Turing hypothesis, that -- efficient quantum computation algorithms aside -- still holds for the most interesting computational classes. If anything, the results show that both models are equivalent enough for the classical formulation to remain canonical. $\endgroup$
    – pron
    May 9, 2016 at 6:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.