[Agda] Modelling term-rewriting systems in Agda

[Sergei Meshveliani]

On Tue, 2013-10-22 at 14:15 +0400, Sergei Meshveliani wrote:
> On Mon, 2013-10-21 at 16:42 -0400, Jacques Carette wrote:
> > Hello all,
> >      Does anyone have an example of modelling a term rewriting system, 
> > where you also prove properties like confluence (using critical pairs)?  
> > I am about to do this, and I would much rather use "best practices" 
> > rather than muddle my way through via re-inventing squarish wheels.
> > 
> > Jacques


I am not sure that I understand the goal:

> where you also prove properties like confluence (using critical 
> pairs)?

Forming critical pairs and reducing them is a way to prove confluence
(under some conditions). If they all reduce to trivial, then the
equation set is confluent (under some conditions). This procedure is a
part of the completion procedure. In this sense one can say that
confluence is proved as a part of completion algorithm. My completion
program also gives the  _reduction trace_ for each critical pair. 
This traces _can be considered_ and a proof for confluence.  
For example, one can think of converting these traces to Agda proofs
for equations for critical pairs.

But this confluence proof is also based on the _theorem of completion_: 
            
    Critical pairs are reduced to trivial   iff
    the equation system is confluent (under some conditions).

If you mean a formal _proof certificate for this theorem_,
then this is different, probably, a more complicated subject.

------
Sergei


> I have the  Dumatel  library for this, written in  Haskell.
> 
> It has  critical pairs, unfailing completion, modulo AC also,
> and other useful things, in a very general setting.
> This is for  _many-sorted term rewriting_.
> (It also has inductive prover function).
> 
> The last version project is interrupted, is not workable
> (it has polymorphic sorts evaluated dynamically, and I have met
> technical difficulties).
> 
> But if you ask, I can send you an older version, which has working 
> (AC) completion.
> I have an hope that  Dumatel  can be modified and used as a library
> prover helping to write proofs in Agda programs.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>