Sat Apr 17 12:22:28 EDT 2010

Abstract Machines and Semantics

The LC is a formal system; there is nothing up the sleeves except for
formula on paper and ways to rewrite those formula.

Abstract machines with environments are a more concrete form used to
get something that behaves like one particular form of LC, the
call-by-value lambda calculus (CBV-LC).  Environments mainly allow
substitution to be delayed to improve efficiency.  I.e. you move from
CBV-LC's "global" substitution rule to a machine that implements its
substitution operation in a more low-level fashon, one step at a time.
The machine is still a formal system consisting of formula and ways to
rewrite those formula.

Once you have such a machine, you can start moving into different
directions.  One popular direction is to move away from the guiding
light of the CBV-LC you started from, and represent side effects such
as assignments and continuations because they are essentially right in
front of you, as part of the machine representation.

What is not so easy to understand is the other way around: how can a
particular abstract machine that has been soiled by locally
implemented side-effects be re-abstracted?  The subject of
denotational semantics seems to be mostly about this: how to
re-abstract things globally as functions that were easy to express as
machines locally.  These higher abstraction can then yield some
insights by making it possible to prove properties of a machine that
are completely intractable in the local machine view.