The Coq mailing list

[courtieu <pierre.courtieu AT gmail.com>]

Le Sun, 15 Jun 2008 13:48:20 +0200,
Matthieu Sozeau 
<sozeau AT lri.fr>
 a écrit :


> > If it is understood that this sort of function need a lot of care,  
> > we might as well decide arbitrarily that iota-reduction watches
> > the first argument everytime (it would be quite of an interesting  
> > accident that choosing another argument would be of any interest  
> > whatsoever). Anyway, the need to check that a particular argument
> > is constructed before unfolding the fixpoint is an artefact of  
> > structural recursion, therefore we shouldn't need any for non- 
> > structural recursion.
> 
> Of course, but the only means of informing the reduction machine of  
> some strategy is through that information (as of now) and I don't
> see any other way of getting as-reasonable-as-possible reductions
> with unchecked fixpoints. My proposal is geared towards functions
> that are actually structurally decreasing but where the syntactic
> criterion fails. { unchecked-struct } might be a better name?


Hi all,
maybe this the point. As far as I understand, the strategy based
on structural argument (unfolding fixpoint only when decreasing arg
has a head constructor) has the good property to terminate even if a non
terminating function is defined (in an inconsistent environment for
example). This is important because *typing* (more precisely
conversion) remains terminating (if I understand well) even if
the typing environment is inconsistent.

Do we want to lose this property (termination of typing even in
presence of inconsistent environments)?

Is there a way to keep this property without structural
argument strategy? Maybe experts can answer this question.

Pierre