Technical Perspective: When Proofs Meet Programs: An Extension of Dependent Type Theory with Church’s Thesis

What is a mathematical proof? It can be described as a sequence of logical steps and calculations that serve as evidence of the correctness of a statement. The steps must follow rules that are accepted as correct by the community. One might think there is a set of universal rules. However, this is far from being the case. Gödel’s incompleteness theorem tells us that no “reasonable” system will allow us to prove everything that is “true.”

Instead of searching for ever more powerful theories, one can, on the contrary, restrict the rules of the game to extract more information from the proofs. Let’s look at an example. If a formula $\exists x,P\left(x\right)$ is true in a certain “world,” then, by definition, there exists an element $t$ in the model such that the formula $P\left(x\right)$ is true for $x=t$. What happens at the proof level? If we have proven the formula $\exists x,P\left(x\right)$, does there exist a “witness” $t$ and a proof of $P\left(t\right)$?

This property is characteristic of so-called “constructive” logics but is not satisfied by usual logic. Indeed, mathematicians classically do not distinguish between the property “there exists x such that P” and its negative version: “it is impossible for P to always be false.” To illustrate the difference, let’s consider a function f on natural numbers. This function reaches a minimum point (otherwise, one could build an infinite decreasing sequence starting from $f\left(0\right))$. But this proof does not give us any clue on how to actually construct the minimum of any particular function f.

Some “natural” logics preserve the “constructive” nature of the existential quantifier and thus guarantee the existence of witnesses associated with existence proofs. These logics have a strong connection with computer science, as the proofs will not only give us a way to designate the witness but also a way to compute it.

The representation of proofs by expressions corresponding to functional programs is known as the Curry-Howard correspondence. This is an essential tool for understanding the dynamics of proofs (very useful in automated theorem proving to restrict the search space). It is also the foundation of several proof assistants, in particular, Coq/Rocq, Agda, and Lean. The interactive proof process ultimately produces an explicit term to represent the proof, which is then verified a posteriori by a program acting as an uncompromising reviewer. The same functional framework is used to represent calculations commonly used in mathematical modeling and proofs.

The resulting languages form privileged frameworks both for formalizing mathematics and for representing computational objects. They are grouped under the term “type theory” to distinguish them from the “set theory” traditionally claimed as the foundation of mathematics.

The accompanying paper, “Upon This Quote I Will Build My Church Thesis” by Pédrot, is set within Martin-Löf’s type theory, which is the system underlying a proof tool like Agda. In this theory, proofs and computations are described in the same functional language. One can establish that any functional expression from natural numbers to natural numbers is a computable function. We also have an important property that any expression (without a free variable) representing a natural number will evaluate to a numeral: 2, 4, 45000, and so on.

The question posed in the accompanying paper is whether we can internalize in the logic the fact that “every represented function corresponds to the code of a computable function.” This property, known as “Church’s Thesis,” is particularly useful for formalizing decidability results. The question of whether we can add this property to a system like Agda is delicate. It is necessary not only to ensure the coherence of the resulting system but also to maintain its good evaluation properties.

The paper provides a very elegant and general solution to this problem. Martin-Löf’s theory is extended with three constants to represent the code of functions, the number of calculation steps in the evaluation on an argument, and the proof that the evaluation returns the expected value. Reduction rules are proposed for these new objects, preserving the property that an expression without free variables representing a natural number can be evaluated to an effective value.

The meta-theoretical properties of such a system are technical and complex. A major contribution of the paper is to propose a completely formalized version of the definitions and results in the Coq proof assistant, which offers an additional guarantee. The text includes links to the formalized counterpart for each definition and lemma, allowing for easy navigation between a general explanation and technical details.

The paper remarkably illustrates the fine properties of proof systems and their deep connections with the theory of computable functions. Type theory is both the subject of study and the tool that ensures the correctness of the mathematical results and that facilitates their reuse in other contexts. It highlights the elegance and importance of this logical framework.