Typing Total Recursive Functions in Coq

Abstract

We present a (relatively) short mechanized proof that Coq types any recursive function which is provably total in Coq. The well-founded (and terminating) induction scheme, which is the foundation of Coq recursion, is maximal. We implement an unbounded minimization scheme for decidable predicates. It can also be used to reify a whole category of undecidable predicates. This development is purely constructive and requires no axiom. Hence it can be integrated into any project that might assume additional axioms.

Work partially supported by the TICAMORE project (ANR grant 16-CE91-0002).

1 Introduction

This paper contains a mechanization in Coq of the result that any total recursive function can be represented by a Coq term. A short slogan could be Coq types any total recursive function, but that would be a bit misleading because the term total might also refer to the meta-theoretical level (see Sect. 7).

The theory of partial recursive (or $\mu$-recursive) functions describes the class of recursive functions by an inductive scheme: it is the least set of partial functions $\mathbb N^k{{-}\!{\rightharpoondown }\,}\mathbb N$ containing constant functions, zero, successor and closed under composition, recursion and unbounded minimization [9]. Forbidding minimization (implemented by the $\mu$ operator) leads to the sub-class of primitive recursive functions which are total functions $\mathbb N^k{{-}\!{\rightarrow }\,}\mathbb N$. Coq has all the recursive schemes except unbounded minimization so it is relatively straightforward to show that any primitive recursive function $f:\mathbb N^k{{-}\!{\rightarrow }\,}\mathbb N$ can be represented by a Coq term $t_f\,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$ where $\mathcal {N}$ is a short notation for the Coq type ${\mathtt {nat}}$ of Peano natural numbers. To represent all partial recursive functions $\mathbb N^k{{-}\!{\rightharpoondown }\,}\mathbb N$ by Coq terms, we would first need to deal with partiality and change the type into $\mathcal {N}^{k}\mathbin {\rightarrow }{\mathtt {option}}~\mathcal {N}$ (for instance) because (axiom-free) Coq only contains total functions; so here the term ${\mathtt {None}}\,{:}\,{\mathtt {option}}~\mathcal {N}$ represents the undefined value. Unfortunately, this does not work because Coq (axiom-free) meta-level normalization would transform such an encoding into a solution of the Halting problem.

Then, from a theoretical standpoint one question remains: which are the functions that Coq can represent in the type $\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$. In this paper, we give a mechanized proof that formally answers of half of the question:

The type $\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$ contains every recursive function of arity k which can be proved total in Coq.

Such a result was hinted in [2] but we believe that mechanizing the suggested approach implies a lot of work (see Sect. 2). This property of totality of Coq can compared to the characterization of System $\mathrm F$ definable functions as those which are provably total in $\mathrm {AF}_2$ [5]. Besides the fact that $\mathrm {AF}_2$ and Coq are different logical frameworks, the main difference here is that we mechanize the result inside of Coq itself whereas the $\mathrm {AF}_2$ characterization is proved at the meta-theoretical level.

Before the detailed description of our contributions, we want to insist on different meanings of the notion of function that should not be confused:

• The $\mu$-recursive schemes are the constructors of an inductive type of algorithms which are the “source code” and can be interpreted as partial function $\mathbb N^k{{-}\!{\rightharpoondown }\,}\mathbb N$ in Set theory or as predicates $\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ in Coq;

• The Set-theoretic notion of partial function is a graph/relation between elements and their images. $\mu$-recursive functions should not be understood independently of the algorithm that implements theses relations: it is impossible to recover an algorithm from the data of the graph alone;

• Then Coq has function types $A\mathbin {\rightarrow }B$ which is a related but nevertheless entirely different notion of function and we rather call them predicates here.

Now let us give a more detailed description of the result we have obtained. We define a dependent family of types $\mathcal {A}_{k}$ representing recursive algorithms of arity $k\,{:}\,\mathcal {N}$. An algorithm $f\,{:}\,\mathcal {A}_{k}$ defines a (partial) recursive function denoted $\llbracket {f}\rrbracket$ and which is represented in Coq as a predicate $\llbracket {f}\rrbracket \,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$:

The proposition $\llbracket {f}\rrbracket \;\varvec{v}\;x$ reads as: the computation of the algorithm f from the input k-tuple $\varvec{v}$ terminates and results in x.

The implementation of the relation $\llbracket {f}\rrbracket$ is a simple exercise. It is more difficult to show that whenever the relation $(\varvec{v},x)\,{\mapsto }\,\llbracket {f}\rrbracket ~\varvec{v}~x$ between the input $\varvec{v}$ and the result x is total, then there is a term $t_f\,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$ (effectively computable from f) such that the result of the computation of f on the input $\varvec{v}$ is $(t_f~\varvec{v})$ for any $\varvec{v}\,{:}\,\mathcal {N}^{k}$. This is precisely what we show in the following formal statement:

$$\begin{aligned} \forall (k\,{:}\,\mathcal {N}) (f \,{:}\,\mathcal {A}_{k}),~ \bigl (\forall \varvec{v}, \exists x, \llbracket {f}\rrbracket ~\varvec{v}~x\bigr ) \mathbin {\rightarrow }\bigl \{t_f \,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}\bigm | \forall \varvec{v}, \llbracket {f}\rrbracket ~\varvec{v}~(t_f~\varvec{v})\bigr \} \end{aligned}$$

(CiT)

The statement means that if $\llbracket {f}\rrbracket$ represents a total function ($\forall \varvec{v}, \exists x, \llbracket {f}\rrbracket ~\varvec{v}~x$), then it can be effectively transformed into a Coq term $t_f\,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$ such that $(t_f~\varvec{v})$ is the value computed by the recursive function $\llbracket {f}\rrbracket$ on the input $\varvec{v}$.

As we already pointed out, “Coq is Total” (CiT) is only one half of the characterization of the predicates that are definable in the type $\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$. The other half of the characterization, i.e. any predicate of type $\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$ corresponds to a $\mu$-recursive function, while meta-theoretically provable for axiom-free Coq, cannot not be proved within Coq itself; see Sect. 7.

We will call reification the process of transforming a non-informative predicate like $P\,{:}\,\forall \varvec{v}, \exists x, \llbracket {f}\rrbracket \;\varvec{v}\;x$ into an informative predicate $Q\,{:}\,\forall \varvec{v}, \{x\mid \llbracket {f}\rrbracket \;\varvec{v}\;x\}$.¹ In its general form, reification is a map from ${\mathtt {inhabited}}\,X\,{:}\,{\mathtt {Prop}}$ to $X\,{:}\,{\mathtt {Type}}$; it transforms a non-informative proof of existence of a witness into an effective witness. In a proof system like HOL for instance, reification is built-in by Hilbert’s epsilon operator. On the contrary, because of its constructive design, Coq does not allow unrestricted reification. If needed in its full generality, it requires the addition of specific axioms as discussed in Sects. 3.1 and 8.

One of the originalities of this work is that the proof we develop is purely constructive (axiom free) and avoids the detour through small-step operational semantics, that is the use of a model of computation on an encoded representation of recursive functions. For instance, programs are represented by numbers (Gödel coding) in the proof of the S-m-n theorem [13]. It is also possible to use other models of computations such as register machines (or Turing machines) or even $\lambda$-calculus as in [8] or in our own dependently typed implementation [7] of Krivine’s reference textbook [6]; see Sect. 7.

In Sect. 2, we present an overview of the consequences of the use of small-step operational semantics and how we avoid it. In Sect. 3 we describe how to implement unbounded minimization of inhabited decidable predicates in Coq. Section 4 presents the inductive types we need for our development, most notably the dependent type $\mathcal {A}_{k}$ of recursive algorithms of arity k and Sect. 5 defines three different but equivalent semantics for $\mathcal {A}_{k}$, in particular a decidable cost aware big-step semantics which is the critical ingredient to avoid small-step semantics. Section 6 concludes with the formal statement of (CiT) and its proof. In Sect. 7, we discuss related work and/or alternative approaches. In Sect. 8, we describe how to reify undecidable predicates (under some assumptions of course), in particular, provability predicates, normalizability predicates and even arbitrary recursively enumerable predicates. Section 9 lists some details of the implementation and how it is split into different libraries.

To shorten notations, we recall that we denote by $\mathcal {N}$ the inductively defined Coq type ${\mathtt {nat}}$ of natural numbers. The $\mu$-recursive scheme of composition requires the use of k-tuples which we implement as vectors. Vectors are typeset in a bold font such as in $\varvec{v}\,{:}\,\mathcal {N}^{k}$ and they correspond to a polymorphic dependent type described in Sect. 4. $\varPi$-types are denoted with a $\forall$ symbol. We denote $\varSigma$-types with their usual Coq notations, which are $(\exists x, P~x)\,{:}\,{\mathtt {Prop}}$ for non-informative existential quantification, $\{x\mid P~x\}\,{:}\,{\mathtt {Set}}$ for informative existential quantification, or even $\{x\,{:}\,X\,{ \& }\,P~x\}\,{:}\,{\mathtt {Type}}$ when $P:X\mathbin {\rightarrow }{\mathtt {Type}}$ carries information as well. These $\varSigma$-types are inductively defined in modules ${\mathtt {Logic}}$ and ${\mathtt {Specif}}$ of the standard library. The interpretation of the different existential quantifiers of Coq is discussed in Sect. 3.1.

2 Avoiding Small-Step Operational Semantics

In this section we give a high level view of our strategy to obtain a mechanized proof of the typability of total recursive functions in Coq. Let us first discuss the approach which is outlined in [2] (Sect. 4.4, p. 685).

• 1. By Kleene’s normal form theorem [9], every recursive function can be obtained by the minimization of a primitive (hence total) recursive function;

• 2. Every primitive recursive function can directly be typed in Coq. The primitive recursion scheme is precisely the recursor ${\mathtt {nat\_rec}}$ corresponding to the inductive type ${\mathtt {nat}}$ (denoted $\mathcal {N}$ in this paper);

• 3. The outermost minimization could be implemented by a “specific minimization function” defined by mutual structural recursion.

Items 1 and 2 are results which should not come as a surprise to anyone knowledgeable of $\mu$-recursion theory and basic Coq programming. These observations were already made in [2]. Their approach to minimization (i.e. Item 3) seems² however distinct from what we propose as Item $3'$ here:

• 3$'$. Minimizations of inhabited and decidable predicates of type $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ can be implemented in (axiom free) Coq.

Item $3'$ could be considered as a bit surprising. Indeed, inductive type theory and hence Coq prohibits unbounded minimization. Hence we did not suspect that Coq could have such a property. When it first came to our attention, we realized that it provided a direct path towards a proof that Coq “had” any total recursive function. Critical for our approach, Item $3'$ is described in Sect. 3.

Despite its apparent straightforwardness, this three steps approach (with either Item 3 or Item $3'$) is difficult to implement because of Item 1. Indeed, let us describe more precisely what it implies. Kleene’s normal form theorem involves the T primitive recursive predicate which decides whether a given (encoding of a) computation corresponds to a given (encoding of a) program code or not. For this, you need a small-step operational semantics (a model of computation), say for instance Minsky (or counter) machines, and a compiler from recursive functions code to Minsky machines. You need of course a correctness proof for that compiler. Since the T predicate operates on natural numbers $\mathcal {N}$, all these data-structures should be encoded in $\mathcal {N}$ which complicates proofs further. Then the T predicate should answer the following question: does this given encoding of a sequence of states correspond to the execution of that given encoding of a Minsky machine. Most importantly, the T predicate should be proved primitive recursive and correct w.r.t. this specification. Programming using primitive recursive schemes is really cumbersome and virtually nobody does this.

Compared to the above three steps approach, the trick which is used in this paper is to merge Items 1 and 2. Instead of showing that recursive functions are minimizations of primitive recursive functions, it is sufficient to show that recursive functions are minimizations of Coq definable predicates. From this point of view, it is possible to completely avoid the encoding/decoding phases from/to $\mathcal {N}$ but more importantly, we do not need a small-step semantics any more; we can replace it with a decidable big-step semantics: this avoids the implementation of a model of computation and thus, the proof of correctness of a compiler.

Our mechanization proceeds in the following steps. We define an inductive predicate denoted and called cost aware big-step semantics. It reads as: the recursive algorithm f terminates on input $\varvec{v}$ and outputs x at cost $\alpha$. This relation is functional/deterministic in both $\alpha$ and x. We show the equivalence $\llbracket {f}\rrbracket \,\varvec{v}\,x\,\Longleftrightarrow \,\exists \alpha ,$ . We establish the central result of decidability of cost aware big-step semantics when $\alpha$ is fixed: for any f, v and $\alpha$, either x together with a proof of can be computed (i.e. ), or (an informative “or”) a proof that no such x exists can be computed (i.e. $\lnot \exists x,$ ). These results are combined in the following way: from a proof of definedness ($\exists x,\llbracket {f}\rrbracket \,\varvec{v}\,x$), we deduce $\exists x\exists \alpha ,$ . Equivalently we get $\exists \alpha ,{\mathtt {inhabited}}$ . By unbounded minimization of inhabited decidable predicates (see Sect. 3), we reify the proposition $\exists \alpha ,{\mathtt {inhabited}}$ into the predicate . Then we extract $\alpha$, x and a proof that , hence $\llbracket {f}\rrbracket \;\varvec{v}\;x$, showing that the computed value x is the output value of f on input $\varvec{v}$.

3 Reifying $\exists P$ into $\varSigma P$ for $P\,{:}\,\mathcal {N}\mathbin {\rightarrow }\{ {\mathtt {Prop}}, {\mathtt {Type}}\}$

In this section, we describe a way to reify non-informative inhabited decidable predicates of type $P\,{:}\,\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$. So we show how to constructively build a value $n\,{:}\,\mathcal {N}$ and a proof term $t\,{:}\,P\,n$. We use an unbounded (but still well-founded) minimization algorithm whose termination is guaranteed by a proof of inhabitation $\exists n,P\,n$. The mechanization occurs in the file nat_minimizer.v which is nearly self-contained. In a way, this shows that Coq has unbounded minimization of inhabited and decidable predicates, whereas the theory of recursive functions has unbounded minimization of partial recursive functions. In Sect. 3.3, we also reify informative decidable predicates $P\,{:}\,\mathcal {N}\mathbin {\rightarrow }{\mathtt {Type}}$ that are inhabited, i.e. verifying $\exists n,{\mathtt {inhabited}}\,(P~n)$.

3.1 Existential Quantification in Coq

Let us recall the usual interpretation of the existential quantifiers that are available in Coq. In Type Theory, they are called $\varSigma$-types over a index type X:

• for $P\,{:}\,X\mathbin {\rightarrow }{\mathtt {Prop}}$, the expression $\exists x\,{:}\,X, P\;x$ (or ${\mathtt {ex}}\,P$) is of type ${\mathtt {Prop}}$ and a term of that type is only a proof that there exists $x\,{:}\,X$ which satisfies $P\;x$. The witness x need not be effective. It can be obtained by non-constructive means. For instance, the proof may use axioms in ${\mathtt {Prop}}$ such as the excluded middle (typically). We say that the predicate $\exists x\,{:}\,X, P\;x$ is non-informative;

• for $P\,{:}\,X\mathbin {\rightarrow }{\mathtt {Prop}}$, the expression $\{ x\,{:}\,X \mid P\;x \}$ (or ${\mathtt {sig}}\,P$) is of type ${\mathtt {Set}}/{\mathtt {Type}}$ and a proof term for it is an (effective) term x together with a proof of $P\;x$ (x must be described by purely constructive methods). We say that the predicate $\{ x\,{:}\,X \mid P\;x \}$ is informative;

• for $P\,{:}\,X\mathbin {\rightarrow }{\mathtt {Type}}$, the expression $\{ x\,{:}\,X \,{ \& }\,P\;x \}$ (or ${\mathtt {sigT}}\,P$) is of type ${\mathtt {Type}}$. It carries both an effective witness x such that $P\;x$ is inhabited and an effective inhabitant of $P\,x$. The predicate $\{ x\,{:}\,X \,{ \& }\,P\;x \}$ is fully informative.

When the computational content of terms is extracted, the sub-terms of type ${\mathtt {Prop}}$ are pruned and their code does not impact the extracted terms: this property is called proof irrelevance. It implies that adding axioms in ${\mathtt {Prop}}$ will only allow to show more (termination) properties but it will not change the behaviour of terms. However, proof irrelevance is not preserved by adding axioms in ${\mathtt {Type}}$.

The Constructive Indefinite Description axiom as stated in Coq standard library module ${\mathtt {ChoiceFacts}}$ can reify any non-informative predicate $\exists P$:

$$\begin{aligned} \forall (X\,{:}\,{\mathtt {Type}}) (P\,{:}\,X\mathbin {\rightarrow }{\mathtt {Prop}}), (\exists x\,{:}\,X, P~x) \mathbin {\rightarrow }\{ x\,{:}\,X \mid P~x \} \end{aligned}$$

(CID)

It provides an (axiomatic) transformation of $\exists P$ (i.e. $\exists x, P\;x$ in Coq) into $\varSigma P$ (i.e. $\{ x \mid P\;x \}$ in Coq). The type $\forall X\,{:}\,{\mathtt {Type}}, {\mathtt {inhabited}}\; X \mathbin {\rightarrow }X$ provides an equivalent definition of (CID) where ${\mathtt {inhabited}}\,{:}\,{\mathtt {Type}}\mathbin {\rightarrow }{\mathtt {Prop}}$ is the “hidding predicate” of the ${\mathtt {Logic}}$ module; see file cid.v and Sect. 3.3.

Assuming the axiom (CID) creates an “artificial” bridge between two separate worlds.³ Some would even claim that such an axiom is at odds with the design philosophy of Coq: the default bridges that exist between the non-informative sort ${\mathtt {Prop}}$ and the informative sorts ${\mathtt {Set}}$/${\mathtt {Type}}$ were carefully introduced by Coq designers to be “constructively” safe; in particular, to ensure that extraction is proof irrelevant. Assuming (CID) would not be inconsistent with extraction but it would leave a hole in the extracted terms that make use of it. Moreover, assuming (CID), one can easily derive a proof of $\forall A\,B\,{:}\,{\mathtt {Prop}}, A\,{\vee }\,B\mathbin {\rightarrow }\{A\}+\{B\}$ and thus, a statement like $\forall x,\{P\,x\}+\{\lnot P\,x\}$ cannot be interpreted as “P is decidable” anymore. This is well explained in [3] together with the relations between (CID) and Hilbert’s epsilon operator. You will also find a summary of the incompatibilities between (CID) and other features or axioms in Coq.

3.2 The Case of Predicates of Type $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$

We describe a way to implement an instance of (CID) constructively but of course, that proof requires additional assumptions: we require that P is a decidable predicate that ranges over $\mathcal {N}$ instead of an arbitrary type X. We do not extract the missing information x but instead, we generate it using a well-founded algorithm that first transforms the non-informative inhabitation predicate $\exists x\,{:}\,\mathcal {N}, P\,x$ into a termination certificate for a well-founded minimization algorithm that sequentially enumerates natural numbers in ascending order.

Recall the definition of the non-informative accessibility predicate from the ${\mathtt {Wf}}$ module of the Coq standard library:

We write ${\mathtt {Acc}}~R$ instead of ${\mathtt {Acc}}~X~R$ because the parameter X is declared implicit.

We assume a predicate $P \,{:}\,\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ and we suppose that P is decidable (in Coq) with a decision term $H_P$. We define a binary relation $R\,{:}\,\mathcal {N}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ and we show the following results:

which all have straightforward proofs except for ${\mathtt {Acc\_P}}$. That last one is done by induction on the accessibility predicate ${\mathtt {Acc}}~R~n$. The proof term ${\mathtt {Acc\_P}}$ uses the decision term $H_P$ to choose between stopping and moving on to the successor: it stops when $H_P~n$ returns “true,” i.e. ${\mathtt {left}}~T$ with $T\,{:}\,P~n$; it loops on $1+n$ when $H_P~n$ returns “false,” i.e. ${\mathtt {right}}~F$ with $F\,{:}\,\lnot {P~n}$. We analyse the term:

The recursion cannot be based on the argument n because it would not be structurally well-founded in that case and the Coq type-checker would reject it. The recursion is based on the ${\mathtt {Acc}}~R~n$ predicate. The definition is split in two parts to make it more readable; ${\mathtt {Acc\_inv}}$ is from the module ${\mathtt {Wf}}$ of the standard library. The term ${\mathtt {Acc\_P}}$ is a typical example of fixpoint by induction over an ad hoc predicate (see [2] or the Coq’Art [1] p. 428). The ${\mathtt {Fix\_F}}$ fixpoint operator of the ${\mathtt {Wf}}$ module of the Coq standard library is defined this way as well. The cover-induction principle as defined in [4] uses a similar idea.

As a consequence, we can reify decidable and inhabited predicates over $\mathcal {N}$:

The proof is now simple: using ${\mathtt {P\_Acc\_R}}$ and ${\mathtt {Acc\_R\_zero}}$, from $\exists n,P\,n$ we deduce ${\mathtt {Acc}}~R\,~0$, and thus $\{ x\,{:}\,\mathcal {N}\mid P~x \}$ using ${\mathtt {Acc\_P}}$.

Considering this somewhat unexpected result, maybe some further clarifications about the proof of ${\mathtt {nat\_reify}}$ are mandatory at this stage. The witness n which is contained in the hypothesis $\exists n,P\;n$ of sort ${\mathtt {Prop}}$ is not informative and thus cannot be extracted to build a term of sort ${\mathtt {Type}}$. As this remarks seems contradictory with what we show, we insist on the fact that we do not extract the witness n contained in the hypothesis by inspection of its term. Instead, we compute the minimum value m which satisfies $P\,m$ by testing all cases in sequence: $P\,0\;?$, $P\,1\;?$, ... until we reach the first value m which satisfies $P\,m$ (the decidability of P is required for that). To ensure that such a computation is well-founded, we use the non-informative witness n contained in $\exists n,P\,n$ as a bound on the search space; but a bound in sort ${\mathtt {Prop}}$: we encode n into the accessibility predicate $A_n\,{:}\,{\mathtt {Acc}}~R~0$ which is then used as a certificate for the well-foundedness of the computation of ${\mathtt {Acc\_P}}~0~A_n$.

3.3 Reification of Predicates of Type $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Type}}$

We now generalize the previous result ${\mathtt {nat\_reify}}$ to predicates in $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Type}}$ instead of just $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$. But we first need to introduce two predicates:

where ${\mathtt {inhabited}}$ is from the standard library (module ${\mathtt {Logic}}$) and ${\mathtt {decidable\_t}}$ is an informative version of the ${\mathtt {decidable}}$ predicate of the ${\mathtt {Decidable}}$ module of the standard library. Their intuitive meaning is the following:

• ${\mathtt {inhabited}}~P$ hides the information of the witness of P. Whereas a term of type P is a witness that P is inhabited, a term of type ${\mathtt {inhabited}}~P$ hides the witness by the use of the non-informative constructor ${\mathtt {inhabits}}$;

• ${\mathtt {decidable\_t}}~P$ means that either a term of type P is given or a proof that P is void is given. The predicate is informative and contains a Boolean choice (represented by the $+$) which tells whether P is inhabited or not. But it may also contain an effective witness that P is inhabited.

We can now lift the theorem ${\mathtt {nat\_reify}}$ that operates on $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ to informative predicates of type $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Type}}$ in the following way:

The proof is only a slight variation from the $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ case. Notice that the result type $\{ n \,{:}\,\mathcal {N}\,{ \& }\,P~n \bigr \}$ contains the reified value n for which $P\,n$ is inhabited, but it also contains the effective witness that $P\,n$ is not void. On the contrary, in the hypothesis $\exists n,{\mathtt {inhabited}}\,(P\,n)$ neither n nor the witness that $P\,n$ is inhabited have to be provided by effective means.

4 Dependent Types for Recursive Algorithms

So far, we have only encountered datatypes which originate in the Coq standard library, and that are imported by default when loading Coq, most notably $\mathcal {N}$ which is a least solution of the fixpoint equation $\mathcal {N}\equiv \{{\mathtt {0}}\}+\{{\mathtt {S}}~n\mid n\,{:}\,\mathcal {N}\}$. We will need the type of vectors ${\mathtt {VectorDef.t}}$ and the type of positions ${\mathtt {Fin.t}}$ that also belong to the standard library module ${\mathtt {Vector}}$. However, the standard library only contains a small fraction of the results that we use for these datatypes. Moreover, the implementation of some functions of the ${\mathtt {Vector}}$ module is incompatible with how we intend to use them. Typically, the definition of ${\mathtt {VectorDef.nth}}$ which selects a component of a vector by its position does not type-check in our succinct definition of the upcoming ${\mathtt {recalg\_rect}}$ recursor: the definition of ${\mathtt {VectorDef.nth}}$ makes Coq unable to certify the structural decrease of recursive sub-calls which is mandatory for ${\mathtt {Fixpoint}}$ definitions. As a consequence, we use our own vectors and positions libraries. This represents little overhead compared to extending the standard libraries in the ${\mathtt {Vector}}$ module.

We define three types that depend on a parameter $k\,{:}\,\mathcal {N}$ representing an arity. First the type of positions

$$\begin{aligned} \mathop {{\mathtt {pos}}}0 \equiv \emptyset \qquad \mathop {{\mathtt {pos}}}(1+k)\equiv \{ {\mathtt {fst}}\}+\{ {{\mathtt {nxt}}\,{p}}\mid p\,{:}\,\mathop {{\mathtt {pos}}}k \} \end{aligned}$$

which is isomorphic to $\mathop {{\mathtt {pos}}}k\equiv \{i\,{:}\,\mathcal {N}\mid i<k\}$ but avoids carrying the proof term $i<k$. The library pos.v contains the inductive definitions of the type $\mathop {{\mathtt {pos}}}k$ and the tools to manipulate positions smoothly: an inversion tactic ${\mathtt {pos\_inv}}$, maps ${\mathtt {pos2nat}}\,{:}\,\mathop {{\mathtt {pos}}}k\mathbin {\rightarrow }\mathcal {N}$ and ${\mathtt {nat2pos}}\,{:}\,\forall i, i < k \mathbin {\rightarrow }\mathop {{\mathtt {pos}}}k$, etc. To shorten the notations in this paper, ${\overline{p}}$ denotes ${\mathtt {pos2nat}}~p$, the natural number below k which corresponds to p.

Positions of $\mathop {{\mathtt {pos}}}k$ mainly serve as coordinates for accessing the components of vectors of arity k

$$\begin{aligned} X^{0} \equiv \{ {\mathtt {vec\_nil}} \} \qquad X^{1+k} \equiv X\times X^{k} \end{aligned}$$

where $X^{k}$ is a compact notation for ${\mathtt {vec}}~X~k$. The type is polymorphic in X and dependent on $k\,{:}\,\mathcal {N}$. We will write terms of type $X^{k}$ in a bold font like with $\varvec{v}$ or $\varvec{w}$ to remind the reader that these are vectors. Given a position $p\,{:}\,\mathop {{\mathtt {pos}}}k$ and a vector $\varvec{v}\,{:}\,X^{k}$, we write $\varvec{v}_p\,{:}\,X$ for the p-th component of $\varvec{v}$, a short-cut for ${\mathtt {vec\_pos}}~\varvec{v}~p$. ${\mathtt {vec\_pos}}$ is obtained from the “correspondence” $X^{k} \equiv \mathop {{\mathtt {pos}}}k \mathbin {\rightarrow }X$. Notice however that the type $X^{k}$ enjoys an extensional equality (i.e. $\varvec{v}=\varvec{w}$ whenever $\varvec{v}_p=\varvec{w}_p$ holds for any $p\,{:}\,\mathop {{\mathtt {pos}}}k$) whereas the function type $\mathop {{\mathtt {pos}}}k \mathbin {\rightarrow }X$ does not. The file vec.v contains the inductive definition of the type of vectors together with the tools to smoothly manipulate vectors and their components where coordinates can either be positions of type $\mathop {{\mathtt {pos}}}k$ or natural number $i\,{:}\,\mathcal {N}$ satisfying $i<k$. The constructors are ${\mathtt {vec\_nil}}\,{:}\,X^{0}$ and ${\mathtt {vec\_cons}}\,{:}\,X\mathbin {\rightarrow }X^{k}\mathbin {\rightarrow }X^{1+k}$ and ${\mathtt {vec\_cons}}~x~\varvec{v}$ is denoted $x{\#}{\varvec{v}}$ here. The converse operations are ${\mathtt {vec\_head}}\,{:}\,X^{1+k}\mathbin {\rightarrow }X$ and ${\mathtt {vec\_tail}}\,{:}\,X^{1+k}\mathbin {\rightarrow }X^{k}$.

Fig. 1.

The type $\mathcal {A}_{k}$ of recursive algorithms of arity k.

With positions and (polymorphic) vectors, we can now introduce the inductive type of recursive algorithms of arity k denoted by $\mathcal {A}_{k}$ which is defined by the rules of Fig. 1 and implemented in the file recalg.v. The notation $\mathcal {A}_{k}$ is a short-cut for ${\mathtt {recalg}}~k$. Notice that $\mathcal {A}_{k}$ is a dependent type (of sort ${\mathtt {Set}}$). It is the least type which contains constants of arity 0, zero and succ of arity 1, projections at every arity k for each possible coordinate, and which is closed under the composition, primitive recursion and unbounded minimization schemes. $\mathcal {A}_{k}$ itself does not carry the semantics of those recursive algorithms: it corresponds to the source code. We will give a meaning/semantics to those recursive algorithms in Sect. 5 so that they correspond to the usual notion of recursive functions.

To be able to compute with or prove properties of terms of type $\mathcal {A}_{k}$, we implement a general fully dependent recursion scheme ${\mathtt {recalg\_rect}}$ described in the file recalg.v. This principle is not automatically generated by Coq because of the nested induction between the types $\mathcal {A}_{k}$ and ${\mathtt {vec}}~\_~k$ which occurs in the constructor $\mathop {\mathop {{\mathtt {comp}}}{f}}{\varvec{g}}$. The definition of ${\mathtt {recalg\_rect}}$ looks simple but it only works well because ${\mathtt {vec\_pos}}$ was carefully designed to allow the Coq type-checker to detect nested recursive calls as structurally simpler: using the “equivalent” ${\mathtt {VectorDef.nth}}$ instead of ${\mathtt {vec\_pos}}$ prohibits successful type-checking. We also show the injectivity of the constructors of the type $\mathcal {A}_{k}$. Some require the use of the ${\mathtt {Eqdep\_dec}}$ module of the standard library because of the dependently typed context. For example, the statement of the injectivity of the constructor $\mathop {\mathop {{\mathtt {comp}}}{f}}{\varvec{g}}$ involves type castings ${\mathtt {eq\_rect}}$ (or heterogenous equality):

5 A Decidable Semantics for Recursive Algorithms

In this section, we define three equivalent semantics for recursive algorithms. First the standard relational semantics defined by recursion on $f\,{:}\,\mathcal {A}_{k}$, then an equivalent big-step semantics defined by a set of inductive rules. Those two semantics cannot be decided. Then we define a refinement of big-step semantics by annotating it with a cost. By constraining the cost, we obtain a decidable semantics for recursive algorithms $\mathcal {A}_{k}$.

5.1 Relational and Big-Step Semantics

We define relational semantics $\llbracket {f\,{:}\,\mathcal {A}_{k}}\rrbracket \,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ of recursive algorithms by structural recursion on $f\,{:}\,\mathcal {A}_{k}$ so as to satisfy the fixpoint equations of Fig. 2 where $\llbracket {f}\rrbracket$ is a notation for ${\mathtt {ra\_rel}}\,f$; the fixpoint equations ${\mathtt {ra\_rel\_fix\_{*}}}$ are proved in the file ra_rel.v. Without preparation, such a definition could be quite technical because of the nested recursion between the type $\mathcal {A}_{k}$ and the type ${\mathtt {vec}}~{\mathcal {A}_{i}}~k$ of the parameter $\varvec{g}$ in the constructor $\mathop {\mathop {{\mathtt {comp}}}{f}}{\varvec{g}}$. Using our general recursion principle ${\mathtt {recalg\_rect}}$, the code is straightforward; but see the remark about ${\mathtt {recalg\_rect}}$ in Sect. 4. We explicitly mention the type $p\,{:}\,\mathop {{\mathtt {pos}}}x$ in the definition of $\llbracket {\mathop {{\mathtt {min}}}f}\rrbracket$ because it is the only type which does not depend on the type of f: the dependent parameter x is the result of the computation.

Fig. 2.

Relational semantics ${\mathtt {ra\_rel}}$ for recursive algorithms of $\mathcal {A}_{k}$.

The big-step semantics for recursive algorithms in $\mathcal {A}_{k}$ is an inductive relation of type ${\mathtt {ra\_bs}}\,{:}\,\forall k, \mathcal {A}_{k}\mathbin {\rightarrow }\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ and we denote $[{f};{\varvec{v}}]\,{\rightsquigarrow }\,{x}$ for $({\mathtt {ra\_bs}}~k~f~\varvec{v}~x)$; the parameter k is implicit in the notation. $[{f};{\varvec{v}}]\,{\rightsquigarrow }\,{x}$ intuitively means that the computation of f starting from input $\varvec{v}$ yields the result x. We define big-step semantics in file ra_bs.v by the inductive rules of Fig. 3. We point out that the rule corresponding to $[{\mathop {{\mathtt {min}}}f};{\varvec{v}}]\,{\rightsquigarrow }\,{x}$ is of unbounded arity but still finitary because $\mathop {{\mathtt {pos}}}x$ is a finite type. These rules are similar to those used to define the semantics of Partial Recursive Functions in [13] except that thanks to our dependent typing, we do not need to specify well-formedness conditions. In ra_sem_eq.v, we show that big-step semantics is equivalent to relational semantics:

However big-step semantics has the advantage of being defined by a set of inductive rules instead of being defined by recursion on $f\,{:}\,\mathcal {A}_{k}$.

Relational and big-step semantics are not recursive/computable relations: this is an instance of the Halting problem. As such, these relations cannot be implemented by a Coq evaluation function ${\mathtt {ra\_rel\_eval}}\,{:}\,\mathcal {A}_{k}\mathbin {\rightarrow }\mathcal {N}^{k}\mathbin {\rightarrow }{\mathtt {option}}~\mathcal {N}$ satisfying ${\mathtt {ra\_rel\_eval}}~f~\varvec{v} = {\mathtt {Some}}~x\,\Longleftrightarrow \,\llbracket {f}\rrbracket ~\varvec{v}~x$ for any f, $\varvec{v}$ and x. Indeed, when it is axiom free, Coq has normalisation which implies that the functions that can be defined in it are total recursive at the meta-theoretical level. Nevertheless big-step semantics as presented in Fig. 3 is an intermediate step towards a decidable semantics for $\mathcal {A}_{k}$.

Fig. 3.

Big-step semantics ${\mathtt {ra\_bs}}$ for recursive algorithms of $\mathcal {A}_{k}$.

Fig. 4.

Cost aware big-step semantic ${\mathtt {ra\_ca}}$ for recursive algorithms of $\mathcal {A}_{k}$.

5.2 Cost Aware Big-Step Semantics

The cost aware big-step semantics for recursive algorithms in $\mathcal {A}_{k}$ is defined as an inductive predicate of type ${\mathtt {ra\_ca}}\,{:}\,\forall k, \mathcal {A}_{k} \mathbin {\rightarrow }\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$. We denote $({\mathtt {ra\_ca}}~k~f~\varvec{v}~\alpha ~x)$ by where the argument k is implicit in the notation. intuitively means that the computation of f on input $\varvec{v}$ yields the result x and costs $\alpha$. We define the predicate ${\mathtt {ra\_ca}}$ in file ra_ca.v by the rules of Fig. 4. It is interesting to compare these rules with those of conventional big-step semantics ${\mathtt {ra\_bs}}$ of Fig. 3. The very simple but nonetheless powerful idea to get decidability is to decorate big-step semantics with a cost and to constrain computations by a cost that must be exactly matched. This is how we realize the principle of our proof that Coq contains total recursive functions: we avoid a small-step semantics (Kleene’s T predicate) and replace it with a big-step semantics for recursive algorithm that is nevertheless decidable.

We show the equivalence of relational and cost aware big-step semantics

in file ra_sem_eq.v. The proof is circular in style: ${\mathtt {ra\_ca}}$ implies ${\mathtt {ra\_bs}}$ implies ${\mathtt {ra\_rel}}$ implies $\exists {\mathtt {ra\_ca}}$ and all these three implications are proved by induction on the obvious inductive parameter. Do not feel puzzled by a statement of equivalence between a decidable and an undecidable semantics, because it is the quantifier $\exists \alpha$ in ${\mathtt {ra\_ca\_correct}}$ which brings undecidability.

Inversion lemmas named ${\mathtt {ra\_ca\_{*}\_inv}}$ are essential tools to prove the high-level properties of Sect. 5.3. They allow case analysis on the last step of an inductive term depending on the shape of the conclusion. Here is the inversion lemma of one rule:

Such results could be difficult to establish if improperly prepared. In our opinion, the easiest way to prove it is to implement a global inversion lemma that encompasses the whole set of rules of Fig. 4. Then a lemma like ${\mathtt {ra\_ca\_rec\_S\_inv}}$ can be proved by applying the global inversion lemma and discriminate between incompatible constructors of type $\mathcal {A}_{k}$ (in most cases) or use injectivity of thoses constructors (in one case). The global inversion lemma is quite complicated to write because of dependent types. It would fill nearly half of this page (see lemma ${\mathtt {ra\_ca\_inv}}$ in file ra_ca.v). However it is actually trivial to prove, a “reversed” situation which is rare enough to be noticed.

5.3 Properties of Cost Aware Big-Step Semantics

The annotation of cost in the rules of Fig. 4 satisfies the following paradigm: the cost of a compound computation is greater than the sum of the costs of its sub-computations. Hence, we can derive that no computation is free of charge:

The proof is by immediate case analysis on . The cost and results given by cost aware big-step semantics are unique (provided they exist)

The proof is by induction on together with inversion lemmas ${\mathtt {ra\_ca\_{*}\_inv}}$ to decompose . Inversion lemmas are the central ingredient of this proof.

Now the key result: cost aware big-step semantics is decidable (in sort ${\mathtt {Type}}$, see Sect. 3.3) when the cost is fixed

Its proof is the most complicated of our whole development. It proceeds by induction on $f\,{:}\,\mathcal {A}_{k}$ and uses inversion lemmas ${\mathtt {ra\_ca\_{*}\_inv}}$, functionality ${\mathtt {ra\_ca\_fun}}$ as well as a small decidability library to lift decidability arguments over (finitely) quantified statements. The central constituents of that library are:

Some comments about the intuitive meaning of such results could be useful. Recall that decidability has to be understood over ${\mathtt {Type}}$ (as opposed to ${\mathtt {Prop}}$):

• ${\mathtt {decidable\_t\_bounded}}$ states that whenever $P\,n$ is decidable for any n, then given a bound m, it is decidable whether there exists $i<m$ such that $P\,i$ holds. Hence bounded existential quantification inherits decidability;

• ${\mathtt {vec\_sum\_decide\_t}}$ states that if $\varvec{P}$ is a $\mathop {{\mathtt {pos}}}n\times \mathcal {N}$ indexed family of decidable predicates, then it is decidable whether there exists vector $\varvec{v}\,{:}\,\mathcal {N}^{n}$ (of length n) which satisfies $\varvec{P}_{p}~\varvec{v}_{p}$ for each of its components (indexed by $p\,{:}\,\mathop {{\mathtt {pos}}}n$), and such that the sum of the components of $\varvec{v}$ is a fixed value m. This express the decidability of some kind of universal quantification bounded by the length of a vector;

• ${\mathtt {vec\_sum\_unbounded\_decide\_t}}$ states that if P is a $\mathcal {N}\times \mathcal {N}$ indexed family of decidable predicates such that $P\,\_\,0$ is never satisfied, then it is decidable whether there exists a vector $\varvec{q}$ of arbitrary length which satisfies P at every component and such that the sum of those components is a fixed value m. This is a variant of ${\mathtt {vec\_sum\_decide\_t}}$ but for unbounded vector length, only the sum of the components acts as a bound.

Once ${\mathtt {ra\_ca\_decidable\_t}}$ is established, we combine it with ${\mathtt {ra\_ca\_fun}}$ to easily define a bounded computation function for recursive algorithms, as is done for instance at the end of file ra_ca_props.v:

Notice that the function ${\mathtt {ra\_ca\_eval}}$ could be proved primitive recursive with proper encoding of $\mathcal {A}_{k}$ into $\mathcal {N}$ but the whole point of this work is to avoid having to program with primitive recursive schemes.

6 The Totality of Coq

In this section, we conclude our proof that Coq contains all the recursive functions for which totality can be established in Coq. We assume an arity $k\,{:}\,\mathcal {N}$ and a recursive algorithm $f\,{:}\,\mathcal {A}_{k}$ which is supposed to be total:

Mimicking Coq sectioning mechanism, these assumptions hold for the rest of the current section. We first show that given an input vector $\varvec{v}\,{:}\,\mathcal {N}^{k}$, both a cost $\alpha \,{:}\,\mathcal {N}$ and a result $x\,{:}\,\mathcal {N}$ can be computed constructively:

The proof uses unbounded minimization as implemented in ${\mathtt {nat\_reify\_t}}$ to find a cost $\alpha$ such that is an inhabited type. This can be decided for each possible cost thanks to ${\mathtt {ra\_ca\_decidable\_t}}$. Recall that ${\mathtt {nat\_reify\_t}}$ tries 0, then 1, then 2, etc. until it finds the one which is guaranteed to exist. The warranty is provided by a combination of $H_f$ and ${\mathtt {ra\_ca\_correct}}$.

To obtain the predicate $t\,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}$ that realizes $\llbracket {f}\rrbracket$, we simply permute x and $\alpha$ in ${\mathtt {coq\_f}}~\varvec{v}$. We define $t\,{\mathtt {:=}}\,\varvec{v}\,{\mapsto }\,{\mathtt {proj1\_sig}}({\mathtt {projT2}}({\mathtt {coq\_f}}~\varvec{v}))$. Using ${\mathtt {projT1}}({\mathtt {coq\_f}}~\varvec{v})$, ${\mathtt {proj2\_sig}}({\mathtt {projT2}}({\mathtt {coq\_f}}~\varvec{v}))$ and ${\mathtt {ra\_ca\_correct}}$, it is trivial to show that $t~\varvec{v}$ satisfies $\llbracket {f}\rrbracket ~\varvec{v}~(t~\varvec{v})$. Hence, closing the section and discharging the local assumptions, we deduce the totality theorem.

7 Discussion: Other Approaches, Church Thesis

Comparing our method with the approach based on Kleene’s normal form theorem (Sect. 2), we remark that the introduction of small-step semantics would only be used to measure the length (or cost) of computations. Since there is at most one computation from a given input in deterministic models of computation, any computation can be recovered from its number of steps by primitive recursive means. Hence the idea of short-cutting small-step semantics by a cost.

It is not surprising that the Kleene’s normal form approach was only suggested in [2]. Mechanizing a Turing complete model of computation is bound to be a lengthy development. Mainly because translating between elementary models of computation resembles writing programs in assembly language that you moreover have to specify and prove correct. And unsurprisingly, such developments are relatively rare and recent, with the notable exception of [13] which formalizes computability notions in Coq. $\mu$-recursive functions are not dependently typed in [13] (so there is a well-formedness predicate) and they are not compiled into a model of execution. In [12] however, the same author presents a compiler from $\mu$-recursive functions to Unlimited Register Machines, proved correct in HOL. Turing machines, Abacus machines and $\mu$-recursive functions are implemented in [11] with the aim of been able to characterize decidability in HOL. The development in [8] approaches computability in HOL4 through $\lambda$-calculus also with the aim at the mechanization of computability arguments. We recently published online a constructive implementation in (axiom-free) Coq [7] of an significant portion of Krivine’s textbook [6] on $\lambda$-calculus, including a translation from $\mu$-recursive functions to $\lambda$-terms with dependent types in Coq. Actually, this gave us a first mechanized proof that Coq contained any total recursive function by using leftmost $\beta$-reduction strategy to compute normal forms. But it requires the introduction of intersection type systems, a development of more than 25 000 lines of code.

Now, what about a characterization of the functions of type $\mathcal {N}\mathbin {\rightarrow }\mathcal {N}$ definable in Coq? Or else, is such a converse statement of (CiT)

$$\begin{aligned} \forall (k\,{:}\,\mathcal {N})~(g\,{:}\,\mathcal {N}^{k}\mathbin {\rightarrow }\mathcal {N}), \exists f\,{:}\,\mathcal {A}_{k}, \forall \varvec{v}\,{:}\,\mathcal {N}^{k}\!,\, \llbracket {f}\rrbracket ~\varvec{v}~(g\;\varvec{v}) \end{aligned}$$

(ChT)

provable in Coq? It is not too difficult to see that (ChT) does not hold in a model of Coq where function types contain the full set of set theoretic functions like in [10], because it contains non-computable functions. However, it is for us an open question whether a statement like (ChT) could be satisfied in a model of Coq, for instance in an effective model.

In such a case, the statement (ChT) would be independent of (axiom free) Coq: (ChT) would be both unprovable and unrefutable in Coq. We think (ChT) very much expresses an internal form of Church thesis in Coq: the functions which are typable in Coq are exactly the total recursive functions. The problem which such a statement is that the notion of totality is not independent from the logical framework in which such a totality is expressed and some frameworks are more expressive that others, e.g., Set theory defines more total recursive functions that Peano arithmetic. It is not clear how (ChT) could be used to simplify undecidability proofs in Coq.

8 Reifying Undecidable Predicates

In Sect. 3, we did explain how to reify the non-informative predicate $(\exists n, P~n)$ into the informative predicate $\{ n\mid P~n\}$, for P of type $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$. This occurred under an important restriction: P is assumed Coq-decidable there. The Coq term ${\mathtt {nat\_reify}}$ that implements this transformation is nevertheless used in Sect. 6 to reify the undecidable “computes into” predicate ${\mathtt {ra\_bs}}$. This predicate is first represented as an existential quantification of the decidable precidate ${\mathtt {ra\_ca}}$, which is basically a bounded version of ${\mathtt {ra\_bs}}$. Then ${\mathtt {nat\_reify}}$ is used to compute the bound by minimization. Without entering in the full details, we introduce some of the developments that can be found in the file applications.v.

We describe how to reify other kinds of undecidable predicates. For instance, we can reify undecidable predicates that can be bounded in some broad sense. Consider a predicate $P\,{:}\,X\mathbin {\rightarrow }{\mathtt {Prop}}$ for which we assume the following: P is equivalent to $\bigcup _n (Q\;n)$ for some $Q\,{:}\,\mathcal {N}\mathbin {\rightarrow }X\mathbin {\rightarrow }{\mathtt {Prop}}$ such that Q n is (informatively) finite for any $n\,{:}\,\mathcal {N}$. Then, the predicate ${\exists }P$ can be reified into $\varSigma P$:

The idea of the proof is simply that the first parameter of Q is a weight of type $\mathcal {N}$ and that for a given weight n, there are only finitely many elements x that satisfy $Q\,n\,x$ (hence $P\,x$). The weight n such that $\exists x,\,Q\,n\,x$ is reified using ${\mathtt {nat\_reify}}$, then the value x is computed as the first element of the list given by $H_Q~n$. The hypothesis $\exists x, P\,x$ ensures that the list given by $H_Q~n$ is not empty.

Among its direct applications, such a weighted reification scheme can be used to reify provability predicates for arbitrary logics, at least those where formulæ and proofs can be encoded as natural numbers. This very low restriction allows to cover a very wide range of logics, with the notable exception of infinitary logics (where either formulæ are infinite or some rules have an infinite number of premisses). Hence, one can compute a proof of a statement provided such a proof exists. Another application is the reification of the normalizable predicate for any reduction (i.e. binary) relation which is finitary (i.e. with finite direct images). This applies in particular to $\beta$-reduction in $\lambda$-calculus.

To conclude, we implement a judicious remark of one of the reviewers. He points out that we can derive a proof of Markov’s principle for recursively enumerable predicates over $\mathcal {N}^{k}$ (instead of just decidable ones). These are predicates of the form $\varvec{v}\,{\mapsto }\,\llbracket {f}\rrbracket ~\varvec{v}~0$ for some $\mu$-recursive f function of arity k.

Hence if a recursively enumerable predicate can be proved inhabited, possibly using 1-consistent axioms in sort ${\mathtt {Prop}}$ such as e.g. excluded middle, then a witness of that inhabitation can be computed.

9 The Structure of the Coq Source Code

The implementation involves around 4 500 lines of Coq code. It has been tested and should compile under Coq 8.5pl3 and Coq 8.6. It is available under a Free Software license at https://github.com/DmxLarchey/Coq-is-total.

More than half of the code belongs to the utils.v utilities library, mostly in files pos.v, vec.v and tree.v. These could be shrunk further because they contain some code which is not necessary to fulfil the central goal of the paper. The files directly relevant to this development are:

• utils.v The library of utilities that regroups notations.v, tac_utils.v, list_utils.v, pos.v, nat_utils.v, vec.v, finite.v and tree.v;

• nat_minimizer.v The reification of $\exists P$ to $\varSigma P$ by unbounded minimization of decidable predicates of types $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Prop}}$ and $\mathcal {N}\mathbin {\rightarrow }{\mathtt {Type}}$, see Sect. 3;

• recalg.v The dependently typed definition of recursive algorithms with a general recursion principle and the injectivity of type constructors, see Sect. 4;

• a_{rel,bs,ca}.v The definitions of relational, big-step and cost aware big-step semantics, with inversion lemmas, see Sects. 5.1 and 5.2;

• ra_sem_eq.v The proof of equivalence between the three previous semantics, see Sects. 5.1 and 5.2;

• ra_ca_props.v High-level results about cost aware big-step semantics, mainly its functionality and its decidability, see Sect. 5.3;

• decidable_t.v The decidability library to lift decision arguments to finitely quantified statements, see Sect. 5.3;

• coq_is_total.v The file that implements Sect. 6, which shows that any provably total recursive function can be represented by a Coq term;

• applications.v The file that implements Sect. 8, reification of (undecidable) weighted predicates, provability predicates, normalizability predicates and recursively enumerable predicates.