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.
> (/. 'a --> 'b)
> ((/. '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)
> ((/. x y --> (* y x)) 4 5)
> ((/. x (cons y z) --> (values (* x y) z)) 4 '(1 2 3))
Repetitive rewriting could be used to find a fixed point of a function. This finds a square root of √2 using Newton’s method:
> (define reduce (//. ; η-reduction `(λ. ,x (,f ,x)) --> f ; β-reduction `((λ. ,x ,B) ,A) --> (eval `((/. ',x --> ',A) ',B))))
> (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) (,ω ,ω)))
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.
"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.