[Agda] Modelling term-rewriting systems in Agda
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
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.
> 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.
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda