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

[Xavier Urbain]

On 29 June 2010 11:26, Frederic Blanqui <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
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.lri.fr/pipermail/termtools/attachments/20100629/f46534ac/attachment.htm