Subject: categories: Question on rewriting and program specification

From: "Ronald Brown" <[email-masked]>
Date: Sat, 12 Nov 2005 11:48:53 -0000

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

---

From: Jacques Carette <[email-masked]>
Date: Sat, 12 Nov 2005 22:23:13 -0500

There is one part of your questions that I can comment on:

>where most users give simple inputs?
Consider a Computer Algebra System (ie like Maple or Mathematica).
Almost everything interesting it does in the area of Analysis is
formally undecidable.  This is because zero-equivalence for any
interesting subset of the (constructive) reals is undecidable, and
almost all CAS algorithms to do analysis (integration, solving
equations, limits, simplification, etc) requires many zero-equivalence
tests, amongst many undecidable problems.

Nevertheless, these systems are very powerful, and frequently return
interesting answers to even fairly complex user input.  This is because
most users give ``structured'' input, for which semi-decision procedures
seem to be quite adequate.  Of course, if you happen to know exactly
which semi-decision procedures are being used, you can fool them and get
the system to either go into an infinite loop or give a wrong answer.
But that requires a huge amount of knowledge to do so.  The average user
would be unable to manufacture such examples.

It is very important to note that the distinction is between
``structured'' input and ``generic'' input, rather than between simple
and complex.  In other words, what seems to matter most is the
Kolmogorov Complexity (or in the specification case, the logical
succinctness) of an input.  [See
http://www.cas.mcmaster.ca/~carette/publications/simplification.pdf for
one approach to this].

There are similar examples in the automated theorem proving world, where
in particular PVS and IMPS can frequently prove theorems which are not a
priori known to be in a decidable subclass.  Here again, a combination
of semi-decision procedures driven by intelligent heuristics seems to be
highly effective.

Jacques