Languages and Derivatives of Evaluation Semantics

Brief thought. A program language is at a minimum a syntax definition and a set of evaluation semantics of the form a → b, meaning "a gets rewritten as b" (of course, they are terms in reality). So lambda calculus looks like:

t := n
| λn.t
| t t

and has three evaluation rules:

t1 λn.t2 → [t1/n]t2
t1 → t1' ⇒ t1 t2 → t1' t2
t2 → t2' ⇒ t1 t2 → t1 t2'

Only the first is of any real substance. The last two say that an application steps to a particular point if one of its sub-terms steps to a particular point.

Essentially, these evaluation rules are a vector field, or a system of equations. They tell you, for a given point, what the next point is. This is important, of course, because we do need to know where to go. We can even apply a logic system that operates over the syntax of the language to restrict the possibilities to programs that never have undefined behavior (aka a type system).

In my previous entries, I discussed concurrency and linearizability (and its similarity to limit cycles in chaos). For this, it's nice to know the difference between our present state and the next one. For this, we need differentiation.

So an interesting thing might be to take a language, and develop both it's operational semantics and its derivative semantics, and develop some theorems relating them to the equivalent concepts in calculus. What's also nice is that the corresponding type judgments over derivative semantics give a very straightforward notion of linearization points (see below).

More on this later.