Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD1132.PDF):
"My reason to give this course is my conviction that power and crispness
of well-designed calculi is, in general, underestimated, and that in the
science and practice of programming, calculi have an increasingly 
important role to play. How to design a calculus so as to make it geared
to our manipulative needs, and how to design for a calculus a strategy
for its effective use thus become significant methodological issues."

Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD86.PDF):

"Standard mathematical notation has been designed to describe relations
and now we have to define processes. Plain English has grown out of a
need of interhuman communication, to be vague and ambiguous, to tell
jokes and to sing nursery rhymes, but is obviously unfit to express
what has to be expressed now. One can borrow mathematical notations,
one can borrow English words, but completely new semantics must be
attached to them and despite its superficial similarity one creates
a new language. And I think the similarity more misleading than clarifying."
Circa 1963

Quote
Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD1130.PDF)

Quote
Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD1300.PDF)

Quote
Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD950a.PDF)

Quote
Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD950.PDF)

Quote
Dijkstra (http://www.cs.utexas.edu/users/EWD/ewd002xx/EWD932c.PDF)


x * y = x * z => (x * y)/x = (x * z)/x ; divide thru by x
1/x < 1/y     => x > y                 ; reverse inequality
y - 3 = 0     => y - 3 + 3 = 0 + 3     ; add x to both sides
y - 3 + 3     => y                     ; constant reduce

the trace problem
  at what "level" should the trace be generated?
  what happens in a loop executed 1M times?

the level problem
  what is a constant? 
  if a constant is composite (e.g. a matrix) do we trace constant reduce
    in the underlying domain?

  1) Notice that the expression "elide 0 terms" cannot be applied
     in the first step even though there is a 0 term. This seems
     obvious but rule-based reduction systems need to know this
     or they loop infinitely.
  2) What is a constant? The answer depends on the domain. The
     identity matrix is clearly a constant in a matrix domain
     but is a structured object in the domain of its entries.
  3) At what level are we doing the manipulation? Suppose we think
     of the above presentation as a trace of the manipulations that
     a system performs. Suppose we are using matricies. Do we want
     to see the manipulations that occur "inside" the matrices? 
     That is, if the matrices are built over the integers do we
     want to see the integer manipulations in the trace?
  4) What are the names of the manipulated objects? Notice that
     I used "constant term", "right hand side", and "left hand side"
     in the above scripting. Suppose you construct a new domain
     with a new notation. How do we name the parts?
  5) Is x = 2 the simplest form? Why? What criteria do we use to
     define a simplest form? Maple and Axiom allow
          x - 2 = 0  
          x = 2
     but not
          x - 2 + 2 = 0 + 2

(op +
 (arg0
  (plist (inverse -) (#args 2) associative distributive commutative entire)
  const-reduce

(op /
 (arg0
  (plist (inverse *) (#args 2) associative distributive commutative 
     denom ~= 0)

(op + 2 
 (arg0
  (plist (inverse -) (#args 2) associative distributive commutative entire)
 (arg1 2
       (arg0 number (domain integer)


shift-reduce pars
strength-reduce parse
multi-form reduction
  solve for x
  solve for 0
simplify by property (e.g. entire)
decorate