Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I've done a bit of googleing and have come up a bit short.
I am wondering what are the main reasons for computing scientists, programmers, to study term rewriting, and/or term graph rewriting.
As far as I can tell, it just helps for basic reasoning about functional programs and (imperative) program control. Apparently, it is a topic of great interest to logicians and those who study constructive abstract algebras.
Any help would be most appreciated!
I am not sure that this will bring you more than you already know. But then, I may fail to understand the reasons that make you wonder about term rewriting. It does help.
As you may know, grammars are string rewriting systems. At the top of the Chomsky hierarchy, you have type 0 grammars, which define recursively enumerable (RE) anguages, and have the computational power of Turing machines.
So that tells you that rewriting systems in general have a lot do do with expressing algorithms.
The problem with strings in general is that there is no obvious way to attach semantics to them. It is a kind of amorphous rewriting.
What people are usually interested in is expressing algorithms in specific domains that have structure and properties. Such domains are often defined from elementary (atomic) entities, and closed by various operations, possibly quotiented by equivalence relations, and so on. These are often called algebras.
These domains are often abstract. But computations on their elements can be expressed only on concrete representations. Terms are natural represntation of these elements since they express how elements can be obtained for other elements by application of operations, recursively downto atomic elements (though general properties need not always go all the way down). Terms are a kind of tree structure syntax that can be manipulated to express algorithms (as for string). But the operator operand structure of terms also allows associating to them semantics in some abstract domain by means of homomorphisms.
Rather than take the very formal view of wikipedia and many texts on this topic, just consider programs. It is usually recognized that a convenient syntactic representation of programs is what is called Abstract Syntax Tree (AST). But an AST is just a term to represent a program object. Denotational semantics is a way of defining abstract domains and associate values from these domains to AST (or AST subtrees) by mean of homomorphisms. Programs in AST form can be transformed or optimized by applying rewriting rules (I am not asserting that all optimizations can or should be done that way).
Transformation of algebraic expressions for various purposes can be expressed by term rewriting. For example, the simplification of some expressions. Various types of computations can also be naturally expressed as term rewriting, such as the computation of derivatives. Term rewriting is also used sometimes to define canonical forms in algebras, when the same semantic entity can have several syntactic representations.
I do suggest that you look at the wikipedia article on this topic.
My thought is, it's because Term Rewriting is something extremely fundamental, and that lets you describe things in an extremely low-level way, independent of any hardware.
Term-rewriting can describe grammars, but it also gives you the mechanics to described logical systems, like first order logic, etc. Proving and deductions can be written as term-writings. Then, the substitution of term-rewriting is really the only operation you have. The simplicity here is valuable because you're describing logic, so you can't use the full complexity of logic to describe your system (since that's the system you're trying to describe).
This then gives you the mechanics you need to talk about the lambda calculus as a logical/axiomatic system, which gives you an extremely formal, fundamental version of computation.
Turing Machines are useful, but their underlying definitions require you to have a concept of sets, functions, etc. There's a lot more math that's assumed to have been build.
Lambda calculus, on the other hand, is defined in terms of logic, so you can use it without much in the way of definitions for set theory, functions, etc.
Term rewriting, modeled by logic, isn't only applicable to functional programing. When you're doing formal verification of hardware or software, you're always going to do reasoning of some sort, and this reasoning can be modeled by term rewriting.
One very practical reason is that it leads to the construction of program transformation systems, tools that let one manipulate the code for programs as terms (abstract syntax trees) using surface-syntax rewrites.
One example of this my system, the DMS Software Reengineering Toolkit, which has been used for a wide variety of program analysis and massive transformation tasks. You can see how DMS expresses rewrites. These rewrites are applied by an associative-commutative term rewriting system that operates behind the scenes.
