View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Term Rewriting

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

PhD thesis. Has a few good things in it.

Rewriting Logic as a Logical and Semantic Framework

.