The Coq mailing list

[Benjamin Werner <werner AT pauillac.inria.fr>]

      Hi Jean-Francois, hi everyone,

This is an old debate. This question appeared a while ago in the coice
between what Per Martin-Lof called extentional, resp. intentional,
type theories. The latter uses the conversion rule as we know it (with
variants of beta-conversion) in the first, the beta-conversion
side-condition is replaced by Leibniz equality.

It is easy to see that in an incoherent context one can prove A = A->A
and thus type any term in an extentional theory.

The situation is simillar here with the Acc-rec, even if not so
extreme.

In both cases however, strong normalization is broken and thus
(theoretical) decidability of type-checking.

More generaly, it appears that :

* computational terms (of sorts Set, Type) can depend upon
non-computational proofs through three constructs: False_rec, eq_rec
and Acc_rec (and their _rect counterparts).

* False_rec poses no problem, since there is no computation rule
associated to it.

* eq_rec could be handled using a trick Christine mentioned a while
ago, since only conversion of the two parts  of the equality is
involved, which is decidable.

* acc_rec is more tricky. I do not know of a totaly satisfactory
solution which would come in handy.


My main question is whether the reduction of acc_rec is actualy used
to a large extent, of if one will want to use it (for other means than
proving the corresponding equality lemmas).

Up to now, I was tending to think that what we be gained from this was
not worth breaking strong normalization (and also making
efficient/compiled reduction much more difficult).

I would be interested in any opinions on this topic.


Best wishes,



Benjamin


> OK, but what is the point to enforce normalisation in an inconsistent
> context? One of the main uses of normalisation is to ensure
> consistency.
> 
> Best,
>   JF
> 
> > If you add an inconsistent axiom such as
> > 
> > Axiom wf : (x:A)(accessible x).
> > 
> > and if you remove the head-constructor condition for the decreasing 
> > argument, then you can build terms that have no normal form:
> > (f a (wf a)) here.
> 
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>