As there was no response at Lambda the Ultimate I try it here again: term rewriting systems are used for instance in automated theorem proving a symbolic calculation, and of course to define formal grammars. There are some programming languages based in term rewriting, but as far as I understand the concept is more known as pattern matching. Pattern matching is used a lot in functional languages. Barry Jay has created a whole theory called pattern calculus, but he only mentions term rewriting in brief. I have the feeling that they all refer to the same basic idea, so can you use term rewriting and pattern matching synonymously?
3 Answers
One way of looking at these two concepts is to say that pattern matching is a feature of programming languages for combining discrimination on constructors and destructing terms (while at the same time selecting and locally naming term fragments) safely, compactly and efficiently. Research on pattern matching typically focusses on implementation efficiency, e.g. on how to minimise the number of comparisons the matching mechanism has to do.
In contrast, term rewriting is a general model of computation that investigates a wide range of (potentially non-deterministic) methods of replacing subterms of syntactic expressions (more precisely an element of a term-algebra over some set of variables) with other terms. Research on term rewriting systems is usually about abstract properties of rewriting systems such as confluence, determinism and termination, and more specifically about how such properties are or are not preserved by algebraic operations on rewrite systems, i.e. to what extent these properties are compositional.
Clearly there are conceptual overlaps between both, and the distinction is to a degree traditional, rather than technical. A technical difference is that term rewriting happens under arbitrary contexts (i.e. a rule $(l, r)$ induces rewrites $C[l\sigma] \rightarrow C[r\sigma]$ for arbitrary contexts $C[.]$ and substitutions $\sigma$), while pattern matching in modern languages like Haskell, OCaml or Scala provides only for rewriting 'at the top' of a term. This restriction is also, I think, imposed in Jay's pattern calculus. Let me explain what I mean by this restriction. With pattern matching in the OCaml, Haskell, Scala sense, you cannot say something like
match M with
| C[ x :: _ ] -> printf "%i ...\n" x
| C[ [] ] -> printf "[]"
What is C[.]
here? It's supposed to be a
variable that ranges over one-holed contexts. But languages like
OCaml, Haskell or Scala don't give programmers variables that
range over arbitrary (one-holed) contexts, only variables that range
over values. In other words, in such languages you cannot pattern
match at an arbitrary position in a term. You always have to specify
the path from the root of the pattern to the parts that you are
interested in. I guess the key reason for imposing this restriction
is that otherwise pattern matching would be non-deterministic, because
a term might match a pattern in more than one way. For example the
term (true, [9,7,4], "hello", 7)
matches the
pattern C[7]
in two ways, assuming C[.]
ranged over such contexts.
I don't think it's correct to call them synonyms; there is some overlap in terms of research and implementation. I'm not familiar at all with Jay's work, and I'm only somewhat familiar with term rewriting systems, so I may be missing something too.
Pattern matching in general deals with the following problem: you have some structure (a tree or a list or a multiset) and you want to check whether the structure matches a pattern (or one of a number of patterns). This question is certainly relevant to term rewriting, because in term rewriting systems the fact that a term matches a pattern means that the term can be rewritten to a different term, but it's not synonymous term rewriting. (There may be a formulation of pattern matching as rewriting: "Given a term, can you rewrite it to match pattern?" but I've never seen this.)
Pattern matching in a functional programming language has a logical interpretation in terms of focusing (see Krishnaswami's "Focusing on Pattern Matching", for example). Term rewriting systems, on the other hand, often do matching modulo some equational properties, which isn't present in most functional programming languages (you can't match against a multiset in ML or Haskell). There's no fundamental reason why matching modulo equational properties shouldn't be present in functional languages, however.
-
1$\begingroup$ Thanks for your answer. I agree that pattern matching in general is not synonymous with term rewriting but it is more basical. But if someone says that a systems with computational power is based on pattern matching, I cannot see the difference to a term rewriting system with computational power. Can you further exemplify the difference between "has a logical interpretation" and "some equational properties"? $\endgroup$– JakobApr 26, 2011 at 17:45
-
$\begingroup$ "I cannot see the difference to a term rewriting system with computational power" - I'm not sure what this means. As Martin says, term rewriting is a general model of computation, and pattern matching is a feature, not a model of computation. $\endgroup$ Apr 27, 2011 at 12:25
-
$\begingroup$ Can you further exemplify the difference between "has a logical interpretation" and "some equational properties"? - There's not any sort of shallow difference - they're just different properties, apples and oranges. I think that any actual connection between these two might turn out to be a pretty deep research question! Pun with deep inference - see alessio.guglielmi.name/res/cos - probably intended. $\endgroup$ Apr 27, 2011 at 12:27
(I'd rather write this as a comment, but I can't at present.)
Correct me if I'm wrong, but as far as I understand, one more difference between pattern matching and term rewriting, apart from what Martin Berger said in his excellent answer, is that pattern matching rules come with a fixed order (in implementations like Haskell's), whereas with term rewriting rules this is not necessarily the case. This feature, as one would expect, can make a lot of difference when considering the behavior (in particular, termination) of the rules (see "A Gentle Introduction to Haskell, Version 98", section 4.2, for example, or just the factorial example at "Learn you a Haskell").
People more knowledgeable in rewriting theory would have more to say on that (for example, how does typing fit such a comparison exactly?), but, it seems to me fair to agree with Martin Berger, in that term rewriting can be seen to encompass pattern matching (at least as this is implemented in languages like Haskell), to the extent that both can be (rather dryly) viewed as devices which merely employ term-relating rules.