Question on rewriting and program specification
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
There is one part of your questions that I can comment on: Ronald Brown wrote:
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?
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
Jacques Carette wrote:
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.
I have a rather unfortunate experience with "average users" who get wrong answers from CAS's, namely our undergraduate math majors. In their first-year analysis course they learn how to compute limits. Invariably, they are given some limits which Mathematica gets wrong, e.g.: Limit[((1 + 4 x^2)^(1/4) - (1 + 5 x^2)^(1/5))/(a^(-x^2/2) - Cos[x]), x -> 0] The answer is 0, _except_ when the parameter a equals e, in which case the answer is 6. Yes, this is a nasty limit pulled out of a hat, but it is precisely the sort of thing we test our students on. It is rather disappointing that Mathematica falls into exactly the same sort of trap as the average student. Another example is the use of l'Hospital rule, which is used by every CAS. There is a side condition which is not checked by them, which makes them give wrong answers. (The side condition is very nasty to check, namely, whether the zero of a derivative is isolated.) The situation is even worse when engineers and physicsts use CAS. They trust them blindly (I suspect). One day they're going to build a nuclear power plant based on a faulty limit computed by Mathematica or Maple. Andrej Bauer
I should have been more precise when I spoke of "decision procedures" in the context of a CAS. There are many semi-decision procedures for non-parametric problems. For parametric problems, these procedures break down. The issue is almost always the same: a theorem is applied without properly checking side-conditions. Frequently, the issue is one of zero recognition in the presence of parameters, but there can be more complex situations, such as the one Andrej points out. CASes are typically very good at getting good answers at non-parametric problems, and my comments were aimed mostly at that class. Computer Algebra implementers (and I used to be one) are typically very afraid of combinatorial explosions, as a lot of computer algebra people are ``algorithms'' people. Their mathematics background was often such that they prefered a ``generic'' answer quickly than a thorough answer that was a) a mess, and b) slow to get. This is, in part, why I am now in academia, as I want to ``fix'' that. Andrej Bauer wrote:
I have a rather unfortunate experience with "average users" who get wrong answers from CAS's, namely our undergraduate math majors. In their first-year analysis course they learn how to compute limits. Invariably, they are given some limits which Mathematica gets wrong, e.g.:
Limit[((1 + 4 x^2)^(1/4) - (1 + 5 x^2)^(1/5))/(a^(-x^2/2) - Cos[x]), x -> 0]
The answer is 0, _except_ when the parameter a equals e, in which case the answer is 6. Yes, this is a nasty limit pulled out of a hat, but it is precisely the sort of thing we test our students on. It is rather disappointing that Mathematica falls into exactly the same sort of trap as the average student.
This is exactly the kind of parameter specialization problem where CAS designers have ``chosen'' to ignore and return a generic answer. This has been documented since at least 1991 in a nice paper in the Bulletin of the AMS.
Another example is the use of l'Hospital rule, which is used by every CAS. There is a side condition which is not checked by them, which makes them give wrong answers. (The side condition is very nasty to check, namely, whether the zero of a derivative is isolated.)
I don't know about Mathematica, but Maple does NOT use l'Hospital's rule. Almost all limits are computed using one-sided asymptotic series expansions, as l'Hospital's rule is just not very suitable to large-scale computations. If interested, I can provide various published references to the algorithms involved. Of course, one still needs to check that the leading term is non-zero. For the limit above, observe (in Maple):
assume(a::real, x::real); f := ((1 + 4*x^2)^(1/4) - (1 + 5*x^2)^(1/5))/(a^(-x^2/2) - cos(x)): normal(series(f, x=0,5));
1 2 4 - ---------- x~ + O(x~ ) ln(a~) - 1 which clearly indicates that a=exp(1) is a problem point. That the limit is computed anyways is an instance of choosing the ``generic'' answer [whatever that means].
The situation is even worse when engineers and physicsts use CAS. They trust them blindly (I suspect). One day they're going to build a nuclear power plant based on a faulty limit computed by Mathematica or Maple.
Engineers and physicists don't use CAS - they use Matlab. The errors you get there are both worse and better: worse because numerical algorithms are so much more prone to giving (silent) nonsense, and better because Matlab cannot phrase any problems which are parametric! In Ontario (where I teach to Engineers), an Engineer who used either a CAS or Matlab in a computation for their safety critical system and did not check the correctness of the result, would be fully liable for any ensuing problems on their design. Thus, theoretically, Professional Engineers are supposed to given full justifications for the answers of the tools they use. In practice, they trust the tools blindly a bit too often. Again in Ontario, I have some knowledge of the process used for safety-critical software in nuclear power plants [I even have some grant money associated to that]. Tools like Matlab or Maple would not be allowed to give ``final'' answers, in any step of the process. But this is getting just a bit off-topic for the categories mailing-list... Jacques
participants (3)
-
Andrej Bauer -
Jacques Carette -
Ronald Brown