The Coq mailing list

[Maria Joao Frade <mjf AT di.uminho.pt>]

Hello,

while trying to understand Coq's mechanism for
guarded recursive definitions, we came across
an example of non-terminating function which is
accepted by Coq.

First, we define a constant function goodzero,
which maps any natural n to O.

Fixpoint  goodzero [x:nat] : nat :=
       Cases x of
          _ => O
       end.

Coq accepts the definition (with a warning
that the function goodzero is non-recursively
defined).

Now, we modify the function by replacing O
with (([a:nat] O)  (badzero x)). The latter
beta-reduces in 1 step to zero, but contains
a recursive call on x.

Fixpoint badzero [x:nat] : nat :=
       Cases x of
          _ => (([a:nat] O)  (badzero x))
       end.

The function badzero is non-terminating.
We have:

      badzero 0
->  Cases 0 of  _ => (([a:nat] O)  (badzero x))
->  ([a:nat] O) (badzero O)

and thus we cannot normalize badzero O under
call-by-value evaluation:

(* Cbv is call-by-value *)
(* Compute is an alias for Cbv Beta Delta Iota  *)

Eval Compute in (badzero O).
(* !!!!!!!!!!!!!!!!!!!!!  Stack overflow  !!!!!!!!!!!!!!!!!!!! *)


We are not sure how new is this observation:
in his thesis [page 165], Bruno Barras suggests
that non-normalizable expressions may arise if,
as seems to be done in Coq, one checks the guard
condition on the normal form of expressions,
so for badzero,  one reduces (([a:nat] O)  (badzero x))
to O before checking that the guard condition is
--trivially-- verified for O.

However, we would like to know whether someone has
investigated modifications to the current verifications
made in Coq so as to avoid non-terminating functions?
We are interested  to hear about modifications on the
guard condition rather than on type systems a la Gimenez
ICALP'98 (actually, we came across this problem when
trying to prove that all inductive definitions accepted by Coq
are also accepted by a type system stemming from Gimenez
ICALP'98 article and we would like to know what is the most
powerful type system based on the guard predicate that is
strongly normalizing).

Thank you in advance,

     Maria Joao

--
----------------------------------------------------------------
Maria Joao Gomes Frade                email:  
mjf AT di.uminho.pt
Departamento de Informatica
Universidade do Minho
Campus de Gualtar                     TEL: +351 253 60 44 70
4710-057 Braga   (PORTUGAL)           FAX: +351 253 60 44 71
----------------------------------------------------------------