fs@rex.cs.tulane.edu (Frank Silbermann) (06/09/90)
(Based on <1556@sys.uea.ac.uk> jrk@sys.uea.ac.uk from Richard Kennaway) > One use of term-rewriting is in equational specification, > where rules like mult(inv(x),x)=id and f(f(x,y),z)=f(x,f(y,z)) > are perfectly reasonable and useful. > > An alternative motivation for use of equational systems is > their use as functional languages. Non-left-linear rules, > overlapping rules, and systems failing to distinguish > operator symbols from constructor symbols > are pathological cases of little interest, > to be excluded from the class of "nice" rewrite systems. Lacking "niceness" is an understatement. To view a rewriting system as a functional language, the system must recognize such programs as illegal. It may not be easy to find an adequate mechanism which maintains the language's expressiveness. > Those motivated by functional programming can be distinguished > by their tendency to write "->" instead of "=". :-) Perhaps admitting that the system's logic is no longer truly equational? >> I admit your program's operational behavior could be interpreted >> as the implementation of a few familiar functions, >> but do the _formal semantics_ interpret them as such? > I think of the equations as defining functions, > and that's how they behave. Looks like a duck, > quacks like a duck - it's a duck. I don't have to > encode the whole thing in lambda calculus > to put that intuition on a formal basis. The duck rule is OK for hackers, but not for theorists. If the intuition _is_ made explicit in the formal semantics, by whatever means, and if the programmer can rely on the system to ensure that his definitions are "nice," I am satisfied. >> (re: A functional language based on term-rewriting) >> You will need a set of constructs which is sufficiently expressive, >> and an evaluation procedure which is correct and complete, >> and which recognizes illegal programs. > I believe it's been done already. The Huet&Levy paper > gives theoretical underpinnings to Michael O'Donnell's > "Equational Logic as a Programming Language" (MIT, 1985). I am not an expert on O'Donnell's work, but my impression was that it presented a choice: -- either one could have a very expressive equational language whose implementation might not be practical, or a restricted but efficient language, whose usefulness was in doubt. O'Donnell chose to experiment with the latter to see what kinds of programs it _could_ handle. It worked well for specifying and implementing certain abstract data structions, e.g. stacks and queues. To relax the restrictions while maintaining efficiency and correctness was left to future research. Unless those problems have been solved, I'll still prefer the denotational approach. Frank Silbermann fs@rex.cs.tulane.edu