[Agda] Modelling term-rewriting systems in Agda
hancock at spamcop.net
Tue Oct 22 20:48:36 CEST 2013
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.
More information about the Agda