Commentary by cpressey on Term Rewriting works

Advanced Topics in Term Rewriting

.

Reflection in Rewriting Logic

Page 10 gives the rules of inference for rewriting logic.

The book seems otherwise not-very-interesting. It might become more interesting if I became more interested in reflection in this logic, but here it seems to be tied up with "strategies", which feels a little expedient and is thus a little off-putting.

Combinatory Reduction Systems

CRS'es are term rewriting systems that support name binding, like the lambda calculus does.

This paper is, honestly, not the smoothest reading, but, it is also covering very interesting subject matter, and, it does give a formal definition of CRS'es. When it gets to section 11 (the formal definition of a CRS) it gets a better because there is something concrete to latch on to.

The basic idea is that it's a term rewriting system with variable binding.

The upshot is that lambda calculus can be defined as a term rewriting system (with variable binding). Here is the rule for beta reduction:

@(λ([x]Z(x)),Z') → Z(Z')

I might choose different names, for clarity:

@(λ([x]Y(x)),Z) → Y(Z)

In a sense, CRS generalizes lambda calculus.

A rewrite rule in CRS consists of a pair of "Metaterms". Metaterms are terms which may contain metavariables (written in Caps). Ordinary terms may contain only ordinary variables, which are written in italics x and which are part of the object language.

The operator for abstraction: "if t is a metaterm and x a variable, then [x]t is a metaterm, obtained by abstraction."

Definability in lambda calculus is not their concern. They refer to a paper about a self-interpreter for lambda calculus with a normal form, for that.

I was once interested on whether natural deduction rules of inference could be written as CRS rewrite rules.

It should be noted that CRS is a theoretical tool. Implementing it for practical purposes does not seem particularly valuable. It is possible to build an ad hoc term rewriting system that handles name binding, simply using capture-avoiding substitution where appropriate, just as if you were implementing the lambda calculus. CRS really serves more as a theoretical basis to justify it.

What follows are somewhat older notes that I wrote out when trying to understand:

A CRS is a pair (A, R) where A is an alphabet and R is a set of rewrite rules.

The alphabet A consists of a set Var of variables (x_n with n >= 0, also written: x, y, z) a set MVar of metavariables (Z{k}n) with n >= 0, where k is the arity of Z{k}_n a set of function symbols, each with a fixed arity a binary operator for extraction, written []_ improper symbols "(", ")", and ","

"The arities k of the metavariables Z{k} can always be read off from the metaterm in which they occur - hence we will often suppress these superscripts. For example, in (\x.Z_0(x))Z_1, the Z_0 is unary and the Z_1 is 0-ary.".

Definition of a metaterm: a variable is a metaterm. if t is a metaterm and x is a variable, then [x]t is a metaterm. if F is an n-ary function symbol and t1, ... tn are metaterms, then F(t1, ..., tn) is a metaterm. if ti,..., tk (k>O) are metaterms, then Zi(t 1, . . . , tk) is a metaterm (in particular the Z,” are metaterms).

A meta-term is: a meta-variable, or c(mt1, mt2, ... mtn) where c is a function symbol and mt1, mt2, ... mtn are meta-terms.

A rewrite rule is a pair (Lhs, Rhs) of meta-terms.

A term is: a variable, or c(m1, t2, ... tn) where c is a function symbol and t1, t2, ... tn are terms.

Matching Power

A simple (mostly) exposition of the rho-calculus, a lambda calculus-like calculus for term rewriting systems, or for lambda calculus with matching.

The Rho Cube

.

A Constructive Semantics for Rewriting Logic

Michael N. Kaplan's PhD thesis, which, at 94 pages, is one of the shorter PhD theses I've seen. It has as a few good things in it, which I hurriedly wrote down, and which I will try to dump here.

• Equational logic -- rules of inference on p. 18
• Rewriting logic -- rules of inference on p. 30
• Constructive type theory -- it's coded in Coq

One interesting idea in it (that the author does not pursue): define Church-Rosser as a type, then write a proof that a given equational specification inhabits that type.

They emphasize how equational logic and rewriting logic are closely linked.

Somewhere around p. 19 they make the good point that it would be great to have computers automatically prove theorems using equational logic, which is a nice logic because it is sound and complete. But equational logic is hard to automate, as equations go both ways. So each equation is treated as a "oriented equation", that is, a rewrite rule. This remains sound, but is no longer complete.

My own take on this is that every rewriting logic implies an equational logic. Under the "oriented equation" approach, if A rewrites to B, then A and B are things we are considering equal (or equivalent).

Equational logic is sound ("all that is written is true") and complete ("all that is true can be written"). Removing Symmetry results in = becoming a directed rewrite operation; the resulting proof theory is still sound, but no longer complete.

However it is much more practical, as (I would say) the proof system that results is deterministic.

The author notes that formalizing equational logic in Coq often follows a quotienting approach: take a term algebra over the signature of the equational theory (so that you can work with pairs), and define a quotienting relation where two terms are considered equal if that pair is derivable in the equational theory.

To actually implement what they have in Coq, they define a term algebra, and a carrier term algebra, and define a quotienting relation between the two to get constructive proof terms. They discuss how the quotienting relation could be anything from "the most strict" (two proof terms are the same if they have the exact same syntactic form) to "the most permissive" (two proof terms are the same as long as they map the same inputs to the same outputs). Very reminiscent of discrete vs trivial topology, initial vs final algebra.

Some relevant references:

[12] V. Capretta. “Equational reasoning in type theory.” May 2000. [Online]. Avail- able: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.9448

[13] V. Capretta, “Universal algebra in type theory,” in Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs ’99, ser. Lecture Notes in Computer Science (LNCS), Y. Bertot, G. Dowek, A. Hirschowits, C. Paulin, and L. Th ́ery, Eds., vol. 1690. Springer, 1999, pp. 131–148.

[14] T. Ramsamujh, “Equational logic and abstract algebra,” in Proceedings: Thirty-fourth Annual Meeting of the Florida Section of the Mathematical Association of America, D. Kerr and B. Rush, Eds., April 2002. [Online]. Available: http://sections.maa.org/florida/proceedings/2001/default.htm

Rewriting Logic as a Logical and Semantic Framework

.