#lang scribble/manual

@(require
  scribble/eval
  planet/scribble
  (for-label racket "main.rkt"))

@(define replace-eval
   (let ([sandbox (make-base-eval)])
     (sandbox '(require "main.rkt"))
     sandbox))


@title[#:style '(toc)]{Rewrite: The Term Rewriting Tools}

@author{@elem["Sergey B. Samoilenko"]}

@defmodule["main.rkt"]{
 The package provides tools for programming via term rewriting technique. 
 Provided forms could be considered as a syntactic sugar for Racket's @racket[match] form,
 however they offer different semantics. The package introduces repetitive rewriting 
 in order to obtain the normal form of given expression, ability to transform any subpart
 in nested list structure and definition of formal functions which abstract general algebraic types.}

@local-table-of-contents[]

@section{Motivation}

The thorougly developed rewriting theory has many applications in different fields of
computer science @cite["Baader99"  "Bezem03"]. It could be a handy tool in everyday programming practice, making 
program units shorter and more expressive. The REFAL @cite["Turchin89" "Surhone10"] and Wolfram's Mathematica core 
language @cite["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: @racket[replace], @racket[replace-all], @racket[replace-repeated] and @racket[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. 

@subsection{Short examples}

Rewriting is a function:
@interaction[#:eval replace-eval
                    (/. 'a --> 'b)]

It replaces all occurences of @racket['a] to @racket['b] in a nested list structure:
@interaction[#:eval replace-eval
                    ((/. 'a --> 'b) '(1 a ((a b c) a)))]

This rewriting describes cyclic swapping of symbols:

@interaction[
             #:eval replace-eval
                    ((/. 'a --> 'b 'b --> 'c 'c --> 'a) '(1 a ((a b c) a)))]

Rewriting rules used as lambda-functions:

@interaction[
             #:eval replace-eval
                    ((/. x --> (* x x)) 4) ;unary
                    ((/. x y --> (* y x)) 4 5)
                    ((/. x (cons y z) --> (values (* x y) z)) 4 '(1 2 3))]

Rewriting is done at any level of a list structure:
@interaction[
             #:eval replace-eval
                    ((/. (? number? x) --> (* x x)) '(1 (2 3) 4))]

Rewriting rules accept any pattern recognized by @racket[match] form:
@interaction[
             #:eval replace-eval
                    ((/. (list _ (and x (app length 2)) (or 1 2)) --> x) `(a (1 4) 2))]


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

@interaction[
             #:eval replace-eval
                    ((//. x  --> (/ (+ x (/ 2 x)) 2)) 1.)]

Simple implementation of symbolic η- and β-reduction rules for λ-calculus:
@margin-note{We need @racket[eval] here because neither rewriting rules nor replace form (@racket[/.]) are 
                     first class objects (same as @racket[match] and it's patterns).}

@#reader scribble/comment-reader
   (interaction #:eval replace-eval
    (define reduce
      (//. ; η-reduction
           `(λ. ,x (,f ,x)) --> f
           ; β-reduction
           `((λ. ,x ,B) ,A) --> (eval `((/. ',x --> ',A) ',B))))
   )

These rules read: ``The λ-term @math{λ.x (f x)} could be rewritten as @math{f} ''. ``Application of a λ-term @math{((λ . x B) A)} is done by rewriting each occasion of a formal argument @math{x} by @math{A} in the function's body @math{B}''. Now we are able to make symbolic reduction of λ-terms:
@interaction[
             #:eval replace-eval              
                    (reduce '((λ. x (f x x)) a))
                    
                    (reduce '((λ. f (λ. x (f (f x)))) (λ. f (λ. y (f (f y))))))
                    
                    (define ω '(λ. f (λ. x ((f f) x))))
                    
                    (reduce `(,ω (λ. x x)))
                   
                    (reduce `((λ. x y) (,ω ,ω)))]
@margin-note{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 @math{(ω ω)} 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 @racket{examples/} folder within the package distribution.
Examples include:
@itemize{
         
         @item{@scheme{examples.rkt} -- more basic examples.}
          
          @item{@scheme{automata.rkt} -- finite automata defined with rewriting.}
          
          @item{@scheme{infix.rkt} -- transformation of algebraic expressions given in infix notation,
                 to prefix notation with parenthesis and reverse polish notation.}
          @item{@scheme{peano.rkt} -- definition of Peano axioms.}
          
          @item{@scheme{logics.rkt} -- simple tautology prover.}
          
          @item{@scheme{turing.rkt} -- a Turing machine interpreter.}
          
          }

@section{Replacement Forms}

@subsection{Singlefold Rewriting}

@defform/subs[#:literals (--> => ?)(replace rule-spec ...) 
([rule-spec (pat ... --> expr) 
(pat ... --> (=> id) expr) 
(pat ... --> (? guard) expr)])]{Transforms to a function which applies rules specified by @racket[rule-spec] in an attempt to transform the entire input expression. If no rules could be applied, input expression is left unchanged.

@racket[pat] --- any pattern suitable for the @racket[match] form. The sequence of patterns correspond to a sequence of arguments to which a rewriting function is applied.

@racket[expr] --- any expression. In contrast to @racket[match] the right-hand side part of the rule should contain only one expression. Use  @racket[begin] for sequencing.

@defexamples[#:eval replace-eval
                (define f 
                  (replace x --> (* x x) 
                           x y --> (* x y)))
                (f 4)
                (f 4 5)
                (f 4 5 6)]

If none of patterns match, the input arguments are returned as a list.

An optional @racket[(=> id)] between patterns and the @racket[expr] is bound to a failure procedure of zero arguments. It works in the same way as in the @racket[match] form.

An optional @racket[(? guard)] between patterns and the @racket[expr] is used to guard the rule. The @racket[_guard] is evaluated with bindings given by patterns. If @racket[guard] evaluates to @racket[#f] evaluation process escapes back to the pattern matching expression, and resumes the matching process as if the pattern had failed to match. Otherwards the rule is applied. 
}
@defform[(replace-all rule-spec ...)]{Transforms to a procedure which applies rules specified by @racket[rule-spec] in an attempt to transform each subpart of the input expression. If no rules could be applied, input expression is left unchanged.}
@defform[(/. rule-spec ...)]{An alias for the @racket[replace-all] form.}

@examples[#:eval replace-eval
                    ((/. 'a --> 'x) '(a b a d a))
                    ((/. 'a --> 'x) '(a (b (a) d) a))
                    ((/. 'a --> 'b 'b --> 'a) '(a (b (a) b) a))]

Only unary rules could be applied to subexpressions. 
At the same time multiary rules could be applied to a sequence of input arguments.
@examples[#:eval replace-eval
                (define g 
                  (/. (? number? x) --> (* x x) 
                      x y --> (* x y)))
                (g 4)
                (g '(4 5))
                (g 4 5)]

@defform[(define/. id rule-spec ...)]{Expands to @racket[(define id (/. rule-spec ...))].}

@subsection{Repetitive Rewriting}
Repetitive rewriting rules could be either @emph{regular} or @emph{terminal}.
Application of repetitive rewriting rules follows the algorithm:
@itemize{
         @item{Consequently try to apply given rules to the expression.}
          @item{If a pattern, corresponding to a @emph{regular} rule matches, make rewriting and apply rules to the result, starting from the beginning of the rule sequence.}
          @item{If a pattern, corresponding to a @emph{terminal} rule matches, make rewriting, stop the rewriting process and return the result.}
          @item{The rewriting process stops either if expression does not change after rewriting, or if the last applied rule was terminal.}}

@defform/subs[#:id replace-repeated #:literals (--> -->. => ?) (replace-repeated rule-spec ...) 
([rule-spec (pat ... ar expr) 
(pat ... ar (=> id) expr) 
(pat ... ar (? guard) expr)]
[ar --> -->.])]{Transforms to a function which applies rules, specified by @racket[rule-spec], repeatedly in an attempt to get the normal form of the entire input expression.

Arrows  @racket[-->] and  @racket[-->.] correspond to regular and terminal rewriting rules, respectively.
} 

@defform[(replace-all-repeated rule-spec ...)]{Transforms to a procedure which repeatedly performs rewriting in every part of the given expression until either result no longer changes, or terminal rule is applied. It performs one complete pass over the expression using @racket[replace-all], then carries out the next pass.
Each pass is done using preorder traversal of nested list structure.                                      }    

@defform[(//. rule-spec ...)]{An alias for @racket[replace-all-repeated] form.}   

@examples[#:eval replace-eval
                    ((//. 'a --> 'b 
                          'b --> 'c
                          'c --> 'd) '(a b c))]

Using a terminal rule
@interaction[#:eval replace-eval
                    ((//. 'a -->. 'b 
                          'b --> 'c
                          'c --> 'a) '(a b c))]
If rewriting proceeds with multiple values, these values could be accepted as arguments during repeating iterations.

Example. Calculation of GCD:
@interaction[#:eval replace-eval
((//. a 0 -->. a
      a b --> (values b (modulo a b))) 225 125)]

Let's compare three functions which iteratively calculate the @math{n}-th Fibonacci number. The first of them is defined in a regular recursive way, the second implements recursion via rewriting, and the third one uses repetitive rewriting.
@defs+int[#:eval replace-eval
                 [(define (fib1 n)
                    (case n
                      [(1) 0]
                      [(2) 1]
                      [else (let loop ([a 0] [b 1] [i n])
                              (if (= i 3) 
                                (+ a b)
                                (loop b (+ a b) (- i 1))))]))
                  
                  (define fib2
                    (replace
                     1 --> 0
                     2 --> 1
                     n --> (fib2 0 1 n)
                     a b 3 --> (+ a b)
                     a b i --> (fib2 b (+ a b) (- i 1))))
                  
                  (define fib3
                    (replace-repeated
                     1 -->. 0
                     2 -->. 1
                     n --> (values 0 1 n)
                     a b 3 -->. (+ a b)
                     a b i --> (values b (+ a b) (- i 1))))]
                 
                 (let ([n 100000])
                   (= (time (fib1 n)) (time (fib2 n)) (time (fib3 n))))]

@defform[(define//. id rule-spec ...)]{Expands to @racket[(define id (//. rule-spec ...))].}

@section{Formal Functions}

@subsection[#:tag "formal motivation"]{Motivation}

Pattern matching usually goes together with algebraic types. 
Racket's structures and lists could be used as constructors for algebraic data types, but they use have some drawbacks.

Suppose we wish to define a rewriting system for Peano axioms. We start with definition of types for numerals, successor, sum and product:
@defs+int[#:eval replace-eval
                 [(struct N (x) #:transparent)
                  (struct 1+ (x) #:transparent)
                  (struct Sum (x y) #:transparent)
                  (struct Prod (x y) #:transparent)]]
Next we define rewriting rules:
@def+int[#:eval replace-eval
                (define calculate
                  (replace-all-repeated 
                   (N 0) --> 0
                   (N n) --> (1+ (N (- n 1)))
                   
                   (Sum x 0) --> x
                   (Sum x (1+ y)) --> (1+ (Sum x y))
                   
                   (Prod _ 0) --> 0
                   (Prod x (1+ y)) --> (Sum x (Prod x y))))
                (calculate (Sum (N 2) (N 3)))]

However, this clear definition doesn't work, because the rewriting process can't get into the structures and change their parts. One solution is to add rules for penetrating into the structures:
@def+int[#:eval replace-eval
                (define calculate2
                  (replace-repeated 
                   (N 0) --> 0
                   (N n) --> (1+ (N (- n 1)))
                   
                   (Sum x 0) --> x
                   (Sum x (1+ y)) --> (1+ (Sum x y))
                   
                   (Prod _ 0) --> 0
                   (Prod x (1+ y)) --> (Sum x (Prod x y))
                   
                   (1+ x) --> (1+ (calculate2 x))
                   (Sum x y) --> (Sum (calculate2 x) (calculate2 y))
                   (Prod x y) --> (Prod (calculate2 x) (calculate2 y))))
                (calculate2 (Sum (N 2) (N 3)))
                (calculate2 (Prod (N 2) (N 3)))]
Now it works! But heavy and tautological lines which end up the rewriting system look cumbersome. They describe programming, not Peano axioms.

Moreover, we need explicit recursion, therefore we have lost the ability to make anonymous rewriting system. Finally, use of structures fixes the number of their fields, so it is impossible to write a pattern like @racket[(Sum x ___)] and to have any number of arguments, which is reasonable when dealing with sums.

Another approach is to use lists and interpret their @racket[car]-s as tags.
@def+int[#:eval replace-eval
                (define calculate3
                  (replace-all-repeated 
                   `(N 0) --> 0
                   `(N ,n) --> `(1+ (N ,(- n 1)))
                   
                   `(Sum ,x 0) --> x
                   `(Sum ,x (1+ ,y)) --> `(1+ (Sum ,x ,y))
                   
                   `(Prod ,_ 0) --> 0
                   `(Prod ,x (1+ ,y)) --> `(Sum ,x (Prod ,x ,y))))
                
                (calculate3 '(Sum (N 2) (N 3)))
                (calculate3 '(Prod (N 2) (N 3)))]

Looks much better, but a bit prickly because of quotes and commas. It may become even worse-looking if we use blanks _ and ___ a lot. Using explicit @racket[list] constructor does not help either, it makes patterns more difficult to read and write: @racket[(list 'Sum x (list '1+ y))].

The package provides an abstraction named @emph{formal function} which work as a taged list constructor in expression position and as a structure constructor in patterns. With use of formal functions we may write clear definition of rewriting system for Peano's numerals without a single redundant word or symbol:
@defs+int[#:eval replace-eval
                 [(define-formal N 1+ Sum Prod)
                  (define calculate4
                    (replace-all-repeated 
                     (N 0) --> 0
                     (N n) --> (1+ (N (- n 1)))
                     
                     (Sum x 0) --> x
                     (Sum x (1+ y)) --> (1+ (Sum x y))
                     
                     (Prod _ 0) --> 0
                     (Prod x (1+ y)) --> (Sum x (Prod x y))))]
                 
                 (calculate4 (Sum (N 2) (N 3)))
                 (calculate4 (Prod (N 2) (N 3)))]

Besides, formal functions could be usefull in general. For example in exploring functional programming:

@interaction[#:eval replace-eval
                    (define-formal f g h)
                    (map f '(a b c))
                    (foldl g 'x0 '(a b c))
                    (foldr g 'x0 '(a b c))
                    ((compose f g h) 'x 'y)]

Examples @racket{peano.rkt} and @racket{logics.rkt} demonstrate the use of formal functions. 
Rules using structures are shown in @racket{turing.rkt}.

@subsection{Declaring Formal Functions}

@defform[(define-formal id ...)]{Declares identifiers @racket[id ...] to represent formal functions. Produces bindings for @racket[id?] symbols, which work as type predicates.}

@examples[#:eval replace-eval
                    (define-formal f)
                    (f 1)
                    (f 'a 'b)
                    (f? (f 2 3))
                    (f? '(f 2 3))]

@defproc[(formal? [v any/c]) boolean?]{Returns @racket[#t] if @racket[v] is a formal function, @racket[#f] otherwise.}
@deftogether[
[@defproc[(n/f-list? [v any/c]) boolean?]
@defproc[(n/f-pair? [v any/c]) boolean?]]]{Return @racket[#t] if @racket[v] is a list (pair), but not a formal function.}

@examples[#:eval replace-eval
                    (define-formal f)
                    (formal? f)
                    (list? (f 2 3))
                    (n/f-list? (f 2 3))
                    (n/f-list? '(x 2 3))]
In the last case @racket[x] was not declared as a formal function, so it is treated as a regular list.

@section{Utilities}
@defproc[(fixed-point [f procedure?] [#:same-test same? (any/c any/c -> boolean?) almost-equal?]) procedure?]{Returns a function that starting with given arguments, applies @racket[f] repeatedly until the result no longer changes. The function @racket[f] of arity @math{n} must produce @math{n} values.}

This function is used for repetitive rewriting.

@examples[#:eval replace-eval
((fixed-point cos) 1.)]

Implementation of the secant method for solving algebraic equations @math{f(x) = 0} numerically.
@def+int[#:eval replace-eval
(define (secant f)
  (fixed-point (λ(x y)
                 (let ([fx (f x)] [fy (f y)])
                   (values y (/ (- (* x fy) (* y fx))
                                (- fy fx)))))))
 ((secant (λ(x)(- (* x x) 20))) 1. 2.)]
Values returned by this function show the last two approximations to the solution of the equation @math{x^2 - 20 = 0}.
@interaction[(sqrt 20)]

@defproc[(almost-equal? [v1 any/c] [v2 any/c]) boolean?]{Returns @racket[#t] either if @racket[(equal? v1 v2)] yields @racket[#t], or if both @racket[v1] and @racket[v2] are inexact numbers, and they are equal with relative precision, given by the @racket[(tolerance)] parameter.}

@examples[#:eval replace-eval
(almost-equal? 1 (+ 1 1e-16))
(equal? 1 (+ 1 1e-16))]

@defproc[(tolerance) inexact-real?]{A parameter which sets the tolerance for the @racket[almost-equal?] predicate. The default value is @racket[5e-16].}

@examples[#:eval replace-eval
(parameterize ([tolerance 1e-3])
  ((secant (λ(x)(- (* x x) 20))) 1. 2.))]

With @racket[tolerance] set to @racket[0.001] iteration stop when only 3 significant digits of consequent approximations coinside.

@bibliography[ 
  @bib-entry[#:key "Baader99"
             #:title "Term Rewriting and All That"
             #:author "Baader, F. and Nipkow, T."
             #:is-book? #t
             #:date "1999"
             #:location "Cambridge University Press"
             #:url "http://books.google.com/books?id=N7BvXVUCQk8C"]
                           
  @bib-entry[#:key "Bezem03"
             #:title "Term rewriting systems"
             #:author "Bezem, M., Klop, J.W. and Vrijer, R."
             #:url "http://books.google.com/books?id=oe3QKzhFEBAC"
             #:date "2003"
             #:location "Cambridge tracts in theoretical computer science. Cambridge University Press"
             #:is-book? #t]
                           
  @bib-entry[#:key "Turchin89"
             #:title  "REFAL-5 Programming Guide and Reference Manual"
             #:author "Turchin, V. F."
             #:is-book? #t
             #:date "1989"
             #:location "The City College of New York, New England Publishing Co., Holyoke."]
                                                                                             
  @bib-entry[#:key "Surhone10"
             #:title  "Refal"
             #:author "Surhone, L.M., Timpledon, M.T. and Marseken, S.F."
             #:is-book? #t
             #:date "2010"
             #:location "VDM Verlag Dr. Mueller AG & Co. Kg"
             #:url "http://books.google.com/books?id=SH2rcQAACAAJ"]
                           
   @bib-entry[#:key "Wolfram"
             #:title  "Wolfram Mathematica"
             #:is-book? #f
             #:url "http://www.wolfram.com/mathematica/"]]