# [Agda] Modelling term-rewriting systems in Agda

Sergei Meshveliani mechvel at botik.ru
Tue Oct 22 14:50:05 CEST 2013

```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
>

```