The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

In LEGO the iota reductions of inductive types were implemented inside
the kernel using rewriting by the appropriate recursion equations.

There was syntax to turn any propositional equation into a computation
rule using this rewriting engine. This was obviously unsafe, but very
useful for experimentation.  Many things can go wrong with unsafe use
of this feature.  Matching the left hand side of an equation can be
problematic for many reasons.

LEGO had no coinductive types, and used only a normalizing reduction
strategy (the upsilon machine of Pierre Lescanne).

I encourage some unsafe features in Coq to support experimentation.
Coq can keep track of which lemmas and definitions depend
(hereditarily) on some unsafe feature, and always annotate output to
indicate this fact.

Best,
Randy
--
Benjamin Werner writes:
 > Hi,
 > 
 > Obviously, having unguarded fixpoints yields paradoxes.
 > 
 > It could also be worse, since with a fixpoint we can build
 > a type A such that   A is convertible to A->A.
 > 
 > We then can type any term. If we use this and have
 > a case analysis over (say) a type with n constructors and
 > apply it to an object of a type with n+1 constructors, we could
 > end up with a segmentation fault (for the compiled version
 > of reduction).
 > 
 > Whether this can really be done boils down to the fact whether
 > one can really use the fix-point to have the system "understand"
 > that A and A->A are convertible, without entering a loop first; as
 > hinted by Pierre below.
 > 
 > But I  would say this is not too important, if one agrees that the
 > "no-check" option is really unsafe and for experimentation.
 > Whether this option should be offered and documented in
 > the standard Coq is however a question I would not decide
 > alone.
 > 
 > 
 > Best,
 > 
 > Benjamin

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.