MENTAL
 Main Menu
 Applications
 Computer Science
 Rewriting Systems

Rewriting Systems
 REWRITING
SYSTEMS

"Rewriting rules are a simple and natural way to describe any kind of non-numerical process" (J.A. Gognen).

"But only this is to be called 'interpretation': substituting one expression of the rule for another" (Wittgenstein. Philosophical Investigations).


Definición

A Rewrite System consists of:
  1. A set of rules (called rewrite rules"), whose general form is:

      expression1 → expression2 if condition
      (the condition is optional)

    Abbreviated, "p → q if c", being p and q expressions in general. It can be read as "p is rewritten as q" or "p is replaced by < i>q" or "p reduces to q", all under the condition c.

    The arrow indicates "substitution". If the condition does not exist, you have what is usually called a "direct equation", but is better termed "pure substitution" or "unconditional substitution".

  2. An algorithm or control program that performs two tasks. First, the analysis of each rule to determine if it is applicable. Second, when a rule is applicable, it performs the process of substituting in the expression the left-hand side of the rule for the right-hand side.

  3. A context. The context of a Rewrite System is the environment on which substitutions are to be performed. It can be numbers, functions, algebraic expressions, etc.

Reduction

The process of replacing an expression appearing on the left-hand side of a rewrite rule with its corresponding right-hand side is called reduction. So the evaluation of an expression involves a sequence of reductions.

If a is derived directly from b (a reduces to b in one step), it is written a ⇒ b. If a is derived from b through several steps, it is symbolized by a ⇒* b.

From an initial expression a1, applying the rules, we obtain a sequence of reductions: Each discrete step, from ai to aii+1 is a reduction. The last term, which cannot be further reduced is said to be in "normal form" and the expression is "residual".

The term "reduction", however, is misleading, since it may happen that ai+1 is larger than ai. It is more general to use the term "transformation" or "rewrite".


Examples
  1. In the context of powers of type xn, we have the following three rules:

    • xn → 1 if n=0
    • xn → xn/2 × xn/2 if n is even
    • xn → x × xn−1 in all other cases

    Example:

    x5 ⇒ x × x4 ⇒ x× (x2 × x2) ⇒ x × ((x × x) × (x × x))

    Rules 3, 2 and 2 have been applied successively.

  2. The best known example of Rewrite System is the lambda calculus. The context is that of lambda functions, along with their arguments. The general rule is to replace the parameters (identified by the prefix "λ" with the arguments. For example:

    • (λx . 3x+y)4 ⇒ 12+y (replace x with 4 in the function λx.3x+y)

    • (λxyz . x+y+z)(a, b, c) ⇒ a+b +c (parallel substitution of x,y,z by a,b,c;)

    • (λx. λy. λz. x+y+z)abc ⇒ (λy. λz. a+y+z)bc ⇒ (λz. a+b+z)c ⇒ a+b+c
      (successive substitutions, in series)

  3. The system defined by direct substitutions

      Sxyz = xz(yz)
      Kxy = x

    allow to represent all computable functions and is the basis of the Functional Combinators [see Addendum].

Properties

The two most important properties of a Rewrite System are:
  1. Confluence (or Church-Rosser property).
    If there is more than one rule that can be applied at each point in the process, the order or criteria for selection of the rule to be applied by the control program must be considered.


    A set of rules in which the order of application of those rules is indifferent is said to be Church-Rosser. This means that if there are two reductions from the same term p to two different terms, q1 and q2;, we can find two other reductions from these terms to the same term r. Uniqueness implies that the order of application of the rules is indifferent.

  2. Normalization.
    The process of applying the rewrite rules may or may not reach an end. If an end is actually reached (i.e., an infinite sequence of reductions does not occur), the rule set is said to be of finite termination. And all expressions can reach normal form.
A Rewrite System that has these two properties (confluence and normalization) is called "complete".


Concrete and Abstract Rewriting Systems

Concrete Rewrite Systems are those that have an a priori defined semantics. In abstract Rewriting Systems the semantics is free, that is, they admit many interpretations, called "models", as in the case of formal axiomatic systems.

Many problems or domains, apparently different, appear with an analogous formal structure contemplated from the paradigm of Rewriting Systems. In fact, there are so-called "Abstract Reduction Systems" (Abstract Reduction Systems, ARS), since many aspects of rewriting can be studied independently of the nature or semantics of the objects.


Specification in MENTAL

General form of a rule and evaluation process

In MENTAL, a rewrite rule is encoded by a generic expression, parameterized or not: Since the rules are generic expressions, they are automatically applied at all times by the MENTAL interpreter, so there is no need for a specific control program. A given expression is self-evaluated if no rule can be applied, or is evaluated to another expression as a consequence of the automatic evaluation process.


The possibilities of MENTAL as a Rewriting System

MENTAL provides a complete computational model, a generic and flexible framework for defining rewriting systems. Here are some of its possibilities in this regard:
Examples
  1. Example 1 above would be coded like this:

    ⟨( (x^n = 1) ← n=0 )⟩

    ⟨( (x^n = (x^(n÷2) * x^(n÷2))) ) ← (n = (n÷2)*2) )⟩

    ⟨( (x^n = (x * x^(n−1))) )← n≠0 ← (n ≠ n÷2)*2) )⟩

    X^5 // ev. (x * x^4) ev. (x * x^2 * x^2) ev. (x*x*x*x*x*x*x)

    The 3 rules could actually be coded as one, with the hierarchical conditions.

  2. A function-based example:

    ⟨( (f(x y) = (g(x+y) g(x*y))) )⟩ // no condition
    ⟨( (g(x) = 24) ← x>10 )⟩
    ⟨( (g(x) = 12) ← x≤10 )⟩

    f(3 4) // ev. (g(7) g(12)) ev. (12 24)
    f(1 1) // ev. (g(2) g(1)) ev. (12 12)

Addenda

Origin

Rewrite Systems historically emerged from lambda calculus and combinatorial logic. They are playing an important role as a theoretical model of computation, mainly in the area of functional languages. Their main attractions are their generic character and their simplicity.

Rewrite Systems constitute a totally generic programming formalism that serves to specify any computable function, as Bergstra and Tucker [1985] have shown. But by relying on only two conceptual primitives (substitution and condition), it prevents it from becoming a universal language.

According to Gognen [1984], "rewriting rules constitute a simple and natural way of describing any kind of non-numerical process."


Relationships to other domains and applications Other applications of Rewrite Systems include: algebraic specification, recursion theory, automatic theorem proving, program transformation, program verification, machine translation, compilers, natural language processing, automata theory, signal processing, evolutionary systems, etc.


Language OBJ

OBJ [Gognen, 1979] is a very high-level language that is based on rewriting rules, which are called "logical equations" and the corresponding logical system is called "equational logic".

In OBJ the syntactic form of a rewrite rule is. An interesting feature of OBJ is its flexible syntax in which it is possible to define prefix, postfix, infix and mixfix operations. Mixfix operations are the most general. The term "mixfix" is due to P. Mosses (the word "distfix" is also used, where "dist" indicates distributed) and refers to the possibility of specifying operands mixed with symbols or other words. For example, IF_THEN_ELSE_FI is the mixfix statement corresponding to "conditional", where underscores correspond to operands.


Functional combinators

Functional combiners have their origin in two main ideas: The idea of eliminating variables in functions has its origin in the ideas of Moses Schönfinkel, who in the 1920s developed the so-called "functional calculus".

Curry developed the same idea, independently, under the name "combinatorial logic" [Curry, 1958, 1971].

For example, if we have the functions and we define the function then F can be expressed as The associativity is assumed on the right-hand side, i.e, If we define a new function where the arguments can represent functions, it follows that Therefore, F = QAM is a new function that can be defined from the functions Q, A and M, disappearing the variables in its definition and being expressed only by other functions.

Schönfinkel discovered that it was sufficient to introduce two primitive combinatorial forms (combinators) to express any function, without the need for variables: The first can be considered the distribution of z over x and y.

The second is the reduction or elimination of the second argument or the projection onto the first argument.

For example, the identity function Ix = x is a derivative function, since it can be expressed by the two primitives: I = SKK

In effect,
Bibliography