Re: Term rewriting
Abram Demski
My evaluation of the Maude language, which I've spent most of today studying.
http://en.wikipedia.org/wiki/Maude_system
I think Maude has a very nice idea behind it, namely, being able to
specify an algebra and then immediately perform computations using it.
This is very useful to me in particular, for trying out different
logics on the fly (since a logic is nothing but a set of expressions
with transformation rules).
Maude is capable of being a general programming language, but that's
probably not the best use for it. In some ways it is halfway between a
programming language and a theorem prover or proof assistant, because
(like formal code verification systems) it is suited to look for flaws
in systems-- one might specify a program in Maude and then tell Maude
to search for ways of getting to undesired states.
Maude does, however, have some clunkyness. For one thing, the syntax
is sometimes a bit unusual-- for example using /\ to represent and.
For another, the reflective capabilities have the feel of something
written by someone who didn't understand Lisp: the system comes
out-of-the-box with two different types of reflection, both of which
are implementations of it within itself. (To be honest, I don't see
why 2 are necessary.)
--Abram