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