Manifest Termination

International audienceIn formal systems combining dependent types and inductive types, such as the Coq proof assistant [8], non-terminating programs are frowned upon. They can indeed be made to return impossible results, thus endangering the consistency of the system [7], although the transient usage of a non-terminating Y combinator, typically for searching witnesses, is safe [4]. To avoid this issue, the definition of a recursive function is allowed only if one of its arguments is of an inductive type and any recursive call is performed on a syntactically smaller argument. If there is no such argument, the user has to artificially add one, e.g., an accessibility property. Freemonads can still be used to address general recursion [6] and elegant methods make possible to extract partial functions from sophisticated recursive schemes [2, 5]. The latter yet rely on an inductive characterization of the domain of a function, and of its computational graph, which in turn might require a substantial effort of specification and proof. This leads to a rather frustrating situation when computations are involved. Indeed, the user first has to formally prove that the function will terminate, then the computation can be performed, and finally a result is obtained (assuming the user waited long enough). But since the computation did terminate, what was the point of proving that it would terminate? This abstract investigates how users of proof assistants based on variants of the Calculus ofInductive Constructions could benefit from manifestly terminating computations. A companion file showcasing the approach in the Coq proof assistant is available online [1]