% Equations vs. Definitions
% Michael Stone
% February 5, 2012
About a year ago, in the context of a course on Scheme, a friend and colleague
asked me:
> *What's the difference between an equation and a definition?*
Here is my much-belated answer, resurrected as a reminder and a guide to myself
as I [begin][last week] my own study of equations (this time of the
[differential][diffeq] variety)...
The character "`=`" is commonly used to signify six different things; namely:
* an equivalence relation
* the standard (numeric) equality procedure
* equations
* identities
* definitions
* assignments
Equivalence relations are reflexive, symmetric, and transitive binary
relations.
The standard (numeric) equality procedure is a procedure whose application to
arguments evaluates to `#t` when all arguments are numerically equal and to
`#f` otherwise.
~~~~ { .scheme }
(= 1 1) ;; -> #t
(= 1 2) ;; -> #f
~~~~
Equations are combinations whose head is the equals symbol, like:
~~~~ { .scheme }
(= y (* 2 x))
~~~~
Like any syntax, equations can be assigned several interpretations. One
interpretation that is popular in math is to treat equations as defining
relations; that is, as describing one or more sets of solutions of the
equation(s).
A solution is an environment in which a set of equations all evaluate to `#t`.
For example, the evaluation of the following "let" expression proves that
`(4, 2)` is a solution of the equation `y = 2*x`:
~~~~ { .scheme }
(let ((y 4) (x 2)) (= y (* 2 x))) ;; -> #t
~~~~
Identities[^identities] are equations that have been (perhaps implicitly) universally
quantified over a set of satisfying assignments. Identities are mostly used to
relate values like `2`, `+`, and `*` as in:
~~~~ { .scheme }
(∀ ((n ℕ)) (= (+ n n) (* 2 n)))
~~~~
[^identities]: While there are few identities written in Scheme, there are
several computer algebra systems written in Scheme-like languages in which
plenty of identities have been written.
Definitions are compound terms whose evaluation has the side-effect of
installing a new variable-to-value binding into the current environment:
~~~~ { .Scheme }
(define f (λ (x) (* 2 x)))
f ;; -> $
~~~~
Finally, assignments are terms (whose evaluation) or statements (whose
execution) has the side-effect of performing writes to a store:
language assignment
-------- ----------
python `x = 2 * x`
C `x = 2 * x;`
pascal `x := 2`
scheme `(set! x (* 2 x))`
C redux `*(int*)0x12345678 = 0;`
[diffeq]: http://www.amazon.com/Introduction-Ordinary-Differential-Equations-Mathematics/dp/0486659429
[last week]: http://mstone.info/posts/thoughts-20120129/