[Agda] Modelling term-rewriting systems in Agda

[Sergei Meshveliani]

On Tue, 2013-10-22 at 10:33 -0400, Jacques Carette wrote:
> On 2013-10-22 10:24 AM, Sergei Meshveliani wrote:
> > Do you mean
> >    to formulate in Agda
> >    1) a notion of what is a set of _rewriting rules_
> >       (or `equations'),
> >    2) a notion of a rule (equation) set being confluent,
> >    and so on
> > ?
> 
> Yes.  And to be able to effectively work with these notions.  Just 
> encoding is easy enough.

I shall be surprised if anyone has done this.

On the other hand, there is known the Groebner basis method for
_polynomials_. It is an analogue of completion of term rewriting
(forming critical pairs etc.), kind of a special case, in which the 
completion algorithm is proved terminating.

And there are announced (and probably, done) works on formal proof
certificate for formulating the Groebner basis theorem and a proof for
its correctness (this is in Theorema by Bruno Buchberger, and also I
have seen a reference to a proof in the libraries related to Coq).

------
Sergei