Question on rewriting and program specification

["Ronald Brown" <ronnie@ll319dg.fsnet.co.uk>]

I would be grateful for advice and background on the following question or
issues, on which I do not know the computer science background.

I have read that rewriting for monoid presentations is relevant to program
specification.

Now at Bangor we have been involved with computing induced actions of
monoids (and categories)
(with Anne Heyworth), `Using rewriting systems to compute
left Kan extensions and induced actions of categories', J.
Symbolic Computation 29 (2000) 5-31.
where there is defined the notion of presentation for the data of a Kan
extension (= induced action).
--------------------------------------
Question: is it reasonable to say that rewriting for such a presentation is
relevant to program specification in which information is also given on the
input to the program?
-----------------------------------------
The intuitive idea is that a program may be very complex, even undecidable,
or inconsistent, but if the input is trivial, or simple, then the output may
be decidable, and simple. Perhaps there are commercial examples of this,
where most users give simple inputs?

Recall that  we get induced actions for monoids when given a morphism u:
M --> N of monoids, an action of M on X, and so get an action of N on a set
u_*(X). A presentation for this involves a presentation for N, and
generators A for M, and the values of these generators in terms of the
presentation of N. If these generators act trivially on X, and u(A)
generates N, then the induced action is on X again, with trivial action of
N.

A recent application of these ideas of induced actions of categories is for
computing double cosets (math.CO/0508391 with Neil Ghani, Anne Heyworth,
Chris Wensley, JSC to appear).


Ronnie Brown
www.bangor.ac.uk/r.brown
www.popmath.org.uk