What's the difference between term rewriting and pattern matching? 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?
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 :: _ ]  -&gt; printf "%i ...\n" x
   | C[ [] ] -&gt; 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.