Equations vs. Definitions

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 my own study of equations (this time of the differential 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.

(= 1 1) ;; -> #t
(= 1 2) ;; -> #f

Equations are combinations whose head is the equals symbol, like:

(= 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:

(let ((y 4) (x 2)) (= y (* 2 x))) ;; -> #t

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:

(∀ ((n ℕ)) (= (+ n n) (* 2 n)))

Definitions are compound terms whose evaluation has the side-effect of installing a new variable-to-value binding into the current environment:

(define f (λ (x) (* 2 x)))
f ;; -> $<proc:...>

Finally, assignments are terms (whose evaluation) or statements (whose execution) has the side-effect of performing writes to a store: