13
$\begingroup$

I was thinking about proofs and ran into an interesting observation. So proofs are equivalent to programs via the Curry-Howard Isomorphism, and circular proofs correspond to infinite recursion. But we know from the halting problem that in general testing whether an arbitrary program recurses forever is undecidable. By Curry-Howard, does that mean there is no "proof checker" that can determine if a proof uses circular reasoning?

I've always thought that proofs are supposed to be composed of easily-checkable steps (which correspond to applications of inference rules), and checking all the steps gives you confidence that the conclusion follows. But now I'm wondering: maybe it is actually impossible to write such a proof checker, because there is no way for it to get around the halting problem and detect circular reasoning?

|cite|improve this question
$\endgroup$
15
$\begingroup$

The vast majority of proof systems don't allow for infinite, circular proofs, but they do so by making their langauges non-Turing complete.

In a normal functional language, the only way to make a program go on forever is with recursion, and in terms of theory, usually we look at recursion as the $Y$ combinator, a program of type $\forall a \ldotp (a \to a) \to a$: that is, it takes a function which makes calls to some other "self" argument, and turns it into a single recursive function.

Now, apply the Curry-Howard isomorphism to this: we now have a proof that, for any proposition $a$, if $a$ implies itself, then we can prove $a$. We can prove anything this way!

The key here is that the Y-combinator is built-in to a language, it's taken as an axiom. So if you want it not to cause you problems, just get rid of it as an axiom!

Most formal proof systems, because of this, require your recursion to be well founded. They only accept functions that they can prove will halt. And as a result, they reject some programs that do halt, but which they can't prove it for.

Coq does this in a fairly limited way: it just requires that any recursive functions have an argument where any recursive calls only use strictly smaller versions of that argument. Agda does something similar, but with a little more fancy checking to accept a few more programs.

|cite|improve this answer
$\endgroup$
  • 1
    $\begingroup$ Does Coq rule out some legitimate theorems you could otherwise prove? Or are there always workarounds for when the totality checker is too conservative? (I assume the answer is the same for other proof assistants based on dependent type theory?) $\endgroup$ – boyers May 31 '16 at 12:05
  • 1
    $\begingroup$ @boyers FWIW, in Coq one can use Function or Program Fixpointconstructions to prove some function is total if the totality checker fails. A simple example is the merge-sort function on lists. One needs to prove manually we split lists (of length > 1) into strictly smaller sublists. $\endgroup$ – Anton Trunov May 31 '16 at 15:36
  • $\begingroup$ @boyers Yes, there have to be things that you can't prove in Coq, by Gödel's first theorem. In practice it's rare to encounter them, but there's always the diagonal argument: Coq can't prove Coq itself, it can only prove a subset (a very large subset, mind, including all the features but with a lower limit on how much recursion it can handle). I remember reading that Coq's theory is equivalent to the Peano axioms plus the existence of a certain large ordinal (and so proofs that assume an even larger ordinal can't fit), but I can't find the reference now. $\endgroup$ – Gilles May 31 '16 at 20:59
  • $\begingroup$ @AntonTrunov In this context, Program and the like are a red herring. They don't change the theory. What they do is syntactic sugar to use a measure in a proof: rather than reasoning that the object you're interested in gets smaller, you add a level of indirection: calculate some other object gets smaller (e.g. some size) and prove that it gets smaller. See the Wf library. $\endgroup$ – Gilles May 31 '16 at 21:01
  • $\begingroup$ @Gilles I assumed the context was about the practical (concrete) side, like when Coq's heuristics fail... Could you please try finding the paper you mentioned? A link would be much appreciated. $\endgroup$ – Anton Trunov May 31 '16 at 21:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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