| Summary: | This paper is concerned with the form of typed name binding used by the
FreshML family of languages. Its characteristic feature is that a name binding
is represented by an abstract (name,value)-pair that may only be deconstructed
via the generation of fresh bound names. The paper proves a new result about
what operations on names can co-exist with this construct. In FreshML the only
observation one can make of names is to test whether or not they are equal.
This restricted amount of observation was thought necessary to ensure that
there is no observable difference between alpha-equivalent name binders. Yet
from an algorithmic point of view it would be desirable to allow other
operations and relations on names, such as a total ordering. This paper shows
that, contrary to expectations, one may add not just ordering, but almost any
relation or numerical function on names without disturbing the fundamental
correctness result about this form of typed name binding (that object-level
alpha-equivalence precisely corresponds to contextual equivalence at the
programming meta-level), so long as one takes the state of dynamically created
names into account.
|
|---|