[Agda] Modelling term-rewriting systems in Agda
mechvel at botik.ru
Tue Oct 22 17:02:02 CEST 2013
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).
More information about the Agda