What's the difference between term rewriting and pattern matching?

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

(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.