[Termtools] [Cime-club] problem with Coccinelle's RPO?

[Frederic Blanqui]

I see. Thank you for your explanations.

Xavier Urbain a écrit :
> 
> 
> On 29 June 2010 11:26, Frederic Blanqui <frederic.blanqui at inria.fr 
> <mailto:frederic.blanqui at inria.fr>> wrote:
> 
> 
> 
>     Pierre Courtieu a écrit :
> 
>         Hello to both of you. First thank you for using coccinelle!
> 
>         There is no problem with symbol equivalence in rpo definition of
>         coccinelle. Actually afs and symbol equivalence are just
>         instances of
>         well foundedness proofs by "inverse image" theorem. This works very
>         well in Cime certificates.
> 
>         If you want to apply an afs, you need to apply a function (doing
>         projection or removing arguments) to your terms before applying your
>         ordering. It is well known that you obtain a well founded
>         ordering if
>         the initial ordering was.
> 
>         If moreover you need to consider symbol f equivalent to g, then
>         it is
>         enough to modify the afs function in such a way that it replaces all
>         occurrence of f by g.
> 
> 
>     Does the CPF format allow this?
> 
> 
>     _______________________________________________
>     Cime-club mailing list
>     Cime-club at lists.gforge.inria.fr <mailto:Cime-club at lists.gforge.inria.fr>
>     http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/cime-club
> 
> 
> 
> Dear Frédéric,
> 
> Regarding termination proofs using RPO, the CPF format specifies the AFS 
> function and the precedence of symbols with their status (lex, mul). 
> When CiME generates a Coq/Coccinelle certificate from a CPF trace, it 
> builds a new AFS that takes into account equivalence of symbols. We can 
> then apply the RPO theorem as it is formalised in Coccinelle, thus 
> validating the original proof in the CPF file.
> 
> Generally speaking, the CPF format does not specify the way one should 
> use a given certification library, it aims to provide relevant proof 
> arguments. The certifier checks that those arguments are sufficient to 
> prove termination.
> 
> In our case, what we do is using a Coq function of type term -> term 
> that projects its argument into the "quotient type" obtained by 
> equalising all the symbols declared equal by the precedence (in fact we 
> do that during the AFS phase but both phases can be split). Then, the 
> ordering corresponding to an RPO with a precedence having an equality 
> part eq_prec is:
> fun t1 t2 => Rpo.rpo (eq_prec t1) (eq_prec t2).
> 
> Best regards,
> 
> The A3PAT team
> 
> 
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Cime-club mailing list
> Cime-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/cime-club