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