How does term-rewriting based evaluation work?

Question

The Pure programming language is apparently based on term rewriting, instead of the lambda-calculus that traditionally underlies similar-looking languages.

...what qualitative, practical difference does this make? In fact, what is the difference in the way that it evaluates expressions?

The linked page provides a lot of examples of term rewriting being useful, but it doesn't actually describe what it does differently from function application, except that it has rather flexible pattern matching (and pattern matching as it appears in Haskell and ML is nice, but not fundamental to the evaluation strategy). Values are matched against the left side of a definition and substituted into the right side - isn't this just beta reduction?

The matching of patterns, and substitution into output expressions, superficially looks a bit like syntax-rules to me (or even the humble #define), but the main feature of that is obviously that it happens before rather than during evaluation, whereas Pure is fully dynamic and there is no obvious phase separation in its evaluation system (and in fact otherwise Lisp macro systems have always made a big noise about how they are not different from function application). Being able to manipulate symbolic expression values is cool'n'all, but also seems like an artifact of the dynamic type system rather than something core to the evaluation strategy (pretty sure you could overload operators in Scheme to work on symbolic values; in fact you can even do it in C++ with expression templates).

So what is the mechanical/operational difference between term rewriting (as used by Pure) and traditional function application, as the underlying model of evaluation, when substitution happens in both?

Avert

@GuyCoder among other things, to emphasise the engineering aspect of the question ("what is it actually doing?") because I wasn't - and still am not - confident in understanding the scientific ("what does this mean?") perspective. – Avert

Lambda is just a specific form of term-rewriting eval [(λx -> '(+ 1 x)) 5] = replace x by 5 in '(+ 1 x) , why not generalize it to implement effect systems, linear types, and awesome pattern matching. – Abstract

Answer 1

Term rewriting doesn't have to look anything like function application, but languages like Pure emphasise this style because a) beta-reduction is simple to define as a rewrite rule and b) functional programming is a well-understood paradigm.

A counter-example would be a blackboard or tuple-space paradigm, which term-rewriting is also well-suited for.

One practical difference between beta-reduction and full term-rewriting is that rewrite rules can operate on the definition of an expression, rather than just its value. This includes pattern-matching on reducible expressions:

-- Functional style
map f nil = nil
map f (cons x xs) = cons (f x) (map f xs)

-- Compose f and g before mapping, to prevent traversing xs twice
result = map (compose f g) xs

-- Term-rewriting style: spot double-maps before they're reduced
map f (map g xs) = map (compose f g) xs
map f nil = nil
map f (cons x xs) = cons (f x) (map f xs)

-- All double maps are now automatically fused
result = map f (map g xs)

Notice that we can do this with LISP macros (or C++ templates), since they are a term-rewriting system, but this style blurs LISP's crisp distinction between macros and functions.

CPP's #define isn't equivalent, since it's not safe or hygenic (sytactically-valid programs can become invalid after pre-processing).

We can also define ad-hoc clauses to existing functions as we need them, eg.

plus (times x y) (times x z) = times x (plus y z)

Another practical consideration is that rewrite rules must be confluent if we want deterministic results, ie. we get the same result regardless of which order we apply the rules in. No algorithm can check this for us (it's undecidable in general) and the search space is far too large for individual tests to tell us much. Instead we must convince ourselves that our system is confluent by some formal or informal proof; one way would be to follow systems which are already known to be confluent.

For example, beta-reduction is known to be confluent (via the Church-Rosser Theorem), so if we write all of our rules in the style of beta-reductions then we can be confident that our rules are confluent. Of course, that's exactly what functional programming languages do!

Caparison

Checking many examples isn't a valid approach to ensuring confluence, whether it's done manually or automatically. A proof needs to be derived from the rules themselves, either informally (eg. a comment like "this is confluent since function composition is associative") or formally (eg. with a model in a meta-logic, like Coq). – Caparison

This is a really cool answer. I'm left with a slightly refined question: without a phase separation, when does (a language like) Pure do the "useful work" of low-level operations like adding two numbers, if + always acts as a constructor that returns an inspectable value, and every function call is effectively a match+cons? Or is the concession to allow low-level concepts like integer math and loops and so on into the language basically just an ad-hoc thing that has nothing to do with the underlying theory? (I should probably try to understand it via one of the alternate paradigms first.) – Avert

It's not that "+" acts as a 'constructor', it's that all terms are just dumb symbols which don't "act" at all. All of the work is performed by the rewrite engine, which chooses which rule to apply next and performs the rewrite. Crucially, all control flow is global: "+" doesn't need to 'decide' whether to reduce it's arguments into a result or leave them 'inspectable' for other rules; all of that is governed by the rewrite engine itself. – Caparison

Term rewriting can be used in the REPL to write our programs for us, but then we can use term-rewriting to turn them into functional programs. – Abstract