▼Rewrite: The Term Rewriting Tools
►1 Motivation
On this page:
1.1 Short examples
  ← prev  up  next → 

1 Motivation

The thorougly developed rewriting theory has many applications in different fields of computer science [Baader99, Bezem03]. It could be a handy tool in everyday programming practice, making program units shorter and more expressive. The REFAL [Turchin89, Surhone10] and Wolfram’s Mathematica core language [Wolfram] give excellent examples of scalability, power and expressiveness provided by rewriting.

The aim of developing this library is to mimic Mathematica’s rewriting tools in Scheme. The library provides four forms: replace, replace-all, replace-repeated and replace-all-repeated named almost in the same way as rewriting functions in Mathematica. In spite of this naming convention, we use word “rewriting” for “replacement”, “substitution” or “transformation” in this manual, since “rewriting” has precise mathematical meaning.

1.1 Short examples

Rewriting is a function:
> (/. 'a --> 'b)

#<procedure:replace-all>

It replaces all occurences of 'a to 'b in a nested list structure:
> ((/. 'a --> 'b) '(1 a ((a b c) a)))

'(1 b ((b b c) b))

This rewriting describes cyclic swapping of symbols:

> ((/. 'a --> 'b 'b --> 'c 'c --> 'a) '(1 a ((a b c) a)))

'(1 b ((b c a) b))

Rewriting rules used as lambda-functions:

> ((/. x --> (* x x)) 4)

16

> ((/. x y --> (* y x)) 4 5)

20

> ((/. x (cons y z) --> (values (* x y) z)) 4 '(1 2 3))

4

'(2 3)

Rewriting is done at any level of a list structure:
> ((/. (? number? x) --> (* x x)) '(1 (2 3) 4))

'(1 (4 9) 16)

Rewriting rules accept any pattern recognized by match form:
> ((/. (list _ (and x (app length 2)) (or 1 2)) --> x) `(a (1 4) 2))

'(1 4)

Repetitive rewriting could be used to find a fixed point of a function. This finds a square root of √2 using Newton’s method:

> ((//. x  --> (/ (+ x (/ 2 x)) 2)) 1.0)

1.414213562373095

Simple implementation of symbolic η- and β-reduction rules for λ-calculus:

We need eval here because neither rewriting rules nor replace form (/.) are first class objects (same as match and it’s patterns).

> (define reduce
    (//. ; η-reduction
         `(λ. ,x (,f ,x)) --> f
         ; β-reduction
         `((λ. ,x ,B) ,A) --> (eval `((/. ',x --> ',A) ',B))))

These rules read: “The λ-term λ.x (f x) could be rewritten as f ”. “Application of a λ-term ((λ . x B) A) is done by rewriting each occasion of a formal argument x by A in the function’s body B”. Now we are able to make symbolic reduction of λ-terms:
> (reduce '((λ. x (f x x)) a))

'(f a a)

> (reduce '((λ. f (λ. x (f (f x)))) (λ. f (λ. y (f (f y))))))

'(λ. x (λ. y (x (x (x (x y))))))

> (define ω '(λ. f (λ. x ((f f) x))))
> (reduce `(,ω (λ. x x)))

'(λ. x x)

> (reduce `((λ. x y) (,ω ,ω)))

'y

To be precise, it is not really lazy. If the whole expression were not a β-redex, rewriting would proceed with it’s parts and finally fall into (ω ω) infinite loop.

The last example shows that we have implemented a sort of lazy evaluation. This is a reflection of the rewriting strategy: first try to rewrite the whole expression and then it’s parts.

More examples could be found in the "examples/" folder within the package distribution. Examples include:

  • "examples.rkt" – more basic examples.

  • "automata.rkt" – finite automata defined with rewriting.

  • "infix.rkt" – transformation of algebraic expressions given in infix notation, to prefix notation with parenthesis and reverse polish notation.

  • "peano.rkt" – definition of Peano axioms.

  • "logics.rkt" – simple tautology prover.

  • "turing.rkt" – a Turing machine interpreter.

  ← prev  up  next →