The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 19/12/2013 12:18, Ali Assaf wrote:

Out of curiosity, is there a specific reason why the Coq kernel does not use primitive recursion internally, as in [1]? From my point of view, this is because primitive recursors are sometimes cumbersome when it comes to writing simple recursive functions. One simple example is division by 2 on nat. In ML you write

let rec div2 n =
  match n with
  | (S (S k)) => S (div2 k)
  | _ => O

With primitive recursors, I can give two typical translations:
- one that relies a lot on the specific problem and do not generalize well: have an extra boolean that
  tells whether the input is even:

let rec div2 n =
  match n with
  | O => (O, true)
  | S k => let (k',b) = div2 k in
                if b then (k',false) else (S k', true)

- one that generalizes better by computing the result for the input and its successor (this is a drastic simplification of what is done in Gimenez' paper):

let rec div2 n =
  match n with
  | O => (O,O)
  | S k => let (dk,dn) = div2 k in (dn, S dk)

Both are neither very easy to read nor especially efficient.


That is, allow the user to write pattern matching and fixpoints as usual, but transform everything to only use primitive recursion. That ought to fix the problems of code complexity (simpler rules) and correctness (any error in the transformation is detected by the kernel).
The problem is that the result of the translation (especially the general one) is quite complex and hard to reason about.

The initial design of a match and a fixpoint with a syntactic criterion for termination was rather simple and well-understood. So it was almost as safe as the recursor, but with a lot of benefits for the users. Then, to allow more recursive calls, the criterion was relaxed and the precise justification has been lost little by little.

In contrast, the type-based approach to termination would have required much less extensions to provide the same features. But it has a higher initial cost (in terms of implementation) to get just the primitive recursor.

Bruno.