[Agda] Modelling term-rewriting systems in Agda

[Peter Hancock]

On 21/10/2013 21:42, Jacques Carette wrote:
> Hello all, Does anyone have an example of modelling a term rewriting
> system, ...

I don't have a fully worked out example, but once thought about it.

If one restricts oneself to terms in a first-order single-sorted
discrete signature of finitary operators, then basic things seem
tractable.  There is a well-defined notion of a "position" within
an expression (at which a redex might occur).  There is also a
notion of replacing a subexpression "redex" at a particular position
with another expression "contractum".  (This can all be done
by general hocus-pocus exploiting Conor McBride's notion
of derivative for a finitary container.)

I have used this in an ad-hoc way for rewriting in specific arithmetic
and algebraic examples.  I did't notice any corners on my wheels.
For me the idea came from a gofer program by Mark Jones.

With the container being finitary, equality is decidable,
and matching against linear patterns seems to be computable.
Maybe a rewriting rule is given by a linear pattern to be matched
against an expression and a function building a new expression from the matching parts.
(But I haven't thought much about how to express that in a usable way.)

Expressing rewriting concepts well in Agda
should not be a problem providing one has a decent way of
expressing them well in real life.

Hank