The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus which is guaranteed to halt.
Constructive logic only differs from classical logic in that it omits LEM.
There seems to be a deep connection here between LEM and the non-halting behavior of Turing machines.
It was recently said to me by a prominent mathematician, who I deeply deeply respect, to the effect that they have never seen any benefit to denying LEM for any question which they care about.
I am not a mathematician, but everything I know about the Curry-Howard correspondence, mathematical proof checkers, Homotopy Type Theory, etc is based on constructive logic which in turn only differs from classical logic in that it explicitly omits LEM.
I'm having trouble squaring my own understanding and this mathematicians statement without falling back to that I must be missing something.
So my questions:
-
Is it correct that the omission of LEM is the distinguishing
characteristic of constructive logic as opposed to classical? -
Is it correct that the Curry-Howard correspondence is conditioned on
the omission of LEM? -
Is it correct that were LEM used in the heart of CoQ and LEAN that in
turn these proof checkers would not be proven to halt? -
Is it correct that therefore to conclude that it is LEM that is at the
heart of the halting problem? -
Is it correct that what distinguishes the untyped lambda calculus
(which can model turing machines) from the simply typed lambda
calculus (which is guaranteed to always halt) must at the heart be
LEM?
It is my understanding that LEM is at the heart of the halting problem precisely because it allows double negation elimination aka indirect proof. It allows to assign a positive truth value to something indirectly by showing its opposite leads to contradiction. Modern proof assistants always halt precisely because they do not allow this indirect proof.
I've always conjectured that the only programs that do not halt are ones that try and make use of indirect proof. Ascribing an affirmative truth value only through showing its opposite leads to contradiction. That while the simply typed lambda calculus is strictly weaker than the untyped lambda calculus (and thus not turing complete) it is only those programs that use indirect proof that are omitted.
The conjecture is based on the following:
- They key distinguishing characteristic of the simply typed lambda calculus and untyped lambda calculus is that the former halts, but the latter is not guaranteed to.
- The key thing that makes the simply typed lambda calculus guaranteed to always halt is the type checker.
- The type checker is based on the Curry-Howard correspondence where types have to be built constructively aka proven.
- The type checker is therefore programmed using the rules of constructive logic.
- The key distinguishing characteristic of constructive logic is the omission of double negation elimination (aka indirect proof).
- Therefore it is the omission/inclusion of double negation elimination that distinguishes systems that always halt versus ones that are not guaranteed to halt.
Thus double negation elimination aka indirect proof is at the heart of the halting problem.
What am I missing?
Thanks.
Best Answer
I'm in a hurry but will try to answer a couple of your questions:
Yes!
In a basic version of the Curry–Howard correspondence, you are quite right: There is no program of the type corresponding to LEM. That would be a kind of oracle which is able, for any type $A$, to either produce a value of $A$ or else produce a procedure $A \to \bot$. In particular, with such an oracle there would be an algorithm deciding the halting problem.
Astoundingly, there are more refined versions of the Curry–Howard correspondence which interpret LEM just fine. Every constructive proof gives rise to a pure program while every classical proof gives rise to a program with side effects. Which side effects exactly, depends on the amount of classical axioms used. For interpreting LEM, to have continuations as side effects is enough. For interpreting countable or dependent choice, other side effects are required. You find some references in these slides.
Literally speaking: No. Coq and Lean support LEM just fine as an unproven assumption and still their proof checking terminates.
Yes in some sense and no in some other.
Yes: Without LEM, it becomes possible for all functions $\mathbb{N} \to \mathbb{N}$ to be computable (by a Turing machine or equivalently by an untyped lambda term). The halting function, which maps a number $n$ to $0$ or $1$ depending on whether the $n$-th Turing machine terminates, is no longer a total function $\mathbb{N} \to \mathbb{N}$ in such a world. (Instead, its domain of definition is the subset consisting of those numbers $n$ such that the $n$-th Turing machine terminates or does not terminate.) Accordingly, the question whether there is a Turing machine computing this no-longer-existing gadget loses a bit of its relevance. There are lots of worlds like this, for instance the "effective topos", I tried to give an introduction here.
No: There is a metatheorem stating that every PA-proof of termination of a Turing machine can be mechanically transformed into a HA-proof, and similarly with ZFC and IZF. (PA is Peano Arithmetic, HA is its constructive cousin without LEM; ZFC is Zermelo–Fraenkel set theory with the axiom of choice, IZF is its constructive cousin without LEM and without choice.) So LEM will never be crucial in proving termination of a Turing machine. LEM might be crucial for abstract tools helping with termination proofs, but in the end LEM can always be eliminated from concrete termination results. Keywords to lookup are "Friedman's trick", "continuation trick" or "Barr's theorem".