The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Maybe the time is ripe to switch to a more semantical notion of 
termination and guardedness.  The syntactic guard condition gets you 
somewhere, but then needs a lot of extensions and patching to work 
satisfactory in practice.  Formal verification of it becomes too 
difficult, and only intuitive justification is prone to errors.

Let's rather invest our energy in integration type-based termination 
into our tools, as, e.g., done in this project:

  Coq^
  http://qatar.cmu.edu/~sacchini/coq.html

This might be a huge initial investment, but I believe it will pay off 
in the long run.

Andreas

On 13.12.2013 12:05, Christine Paulin wrote:
> There are indeed examples where this is needed
> for instance to have (pred n) < n when (n<>0) or any other destructor
> function
> in particular the definition of the fixpoint combinator on well-founded
> relations relies on that.
>
> However there is a simple restriction to the match rule that should
> solve the problem :
>      checking the order is done with respect to an inductive definition
> Ind (the type of the recusive variable in the fixpoint)
>      the return type of the match (the one gouverning the type of eache
> branch) should produce something in this inductive definition (so be of
> the form (x1:A1)...(xn:An)Ind)
> This added condiction should be enough to establish an invariant that
> will guarantee the safety of the condition.
>
>      when doing an elimination on the proof of X=Y to change an object
> of type X into an object of type Y the predicate is fun (p:Prop => p)
> which does not meet the condition. Other useful match constructions that
> I know should pass the test.
> Christine
>
>
>
>
>
> On 12/13/2013 11:04 AM, Viktor Vafeiadis wrote:
> > On 13 Dec 2013, at 08:21, Christine Paulin wrote:
> >
> > > The principle is the recursive call in the definition of f x should
> > > be of the form
> > >      f t
> > > with t a strict recursive subterm of x
> > >
> > > there is a rule to accept a term t of the form (match u with t1 .. tn
> > > end)
> > > whenever all ti are recursive subterms of x
> > >      in particular when u has type False (match u with end) is accepted
> > [...]
> > > So some check needs to be added. A simple idea would be that a
> > > recursive subterm could never be an abstraction, or to add some finer
> > > analysis in which context u should be typable.
> > An even simpler fix would be to just drop the rule that accepts (match
> > u with t1 .. tn end) as a subterm.
> >
> > I wonder whether there are any actual proofs that rely on recursive
> > definitions of such form.
> >
> >
> > Viktor


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/