What's *in* a name?

i recently read Alexander Kurz, et al's paper on algebraic theories over nominal sets with great interest. In connection with that i would like to argue that i believe there is a fundamental flaw in the perception that names should be atomic (without internal structure). However, i believe that that flaw can be easily rectified. Moreover, i believe that work conducted as if names were atomic remains largely undisturbed by the change, but can be enriched by the techniques i present below.

Why names cannot be atomic

The argument against atoms in (foundational) computational theories is straightforward. Algebras and calculi that purport to be foundational accounts of computing, such as the λ-calculus or the π-calculus, endure a fundamental dependency on a theory of names. Specifically, the collection of names in these calculi and other nominal algebras must succumb to the following desiderata.

• it supports a decidable equality
• it is at least countably infinite

now for the questionable desiderata

• the names have no internal structure

When taken together all three require the equality to be an infinite table, an unrealizable oracle. It's not good for a foundational account of computation (or any structure we would like to practically employ in computing, really) to endure a dependency on an unrealizable oracle. Of the three desiderata, there's clearly one that can -- and, i argue, should be -- dropped, namely, the last.

Where does name structure come from?

If we agree -- as every programmer who has to implement any of these structures does -- that names have internal structure, then where does that structure come from? In foundational accounts of computing this question is vital, for if we sneak into our foundational account of computing (such as the λ-calculus or the π-calculus) a dependency on another structure that is computationally complete, then we have robbed out foundational account of computing of it's claim to be foundational. So, where can we look for nominal structure? Why not the proposed theory of computation, itself?

Some examples

The syntax of the λ- and π-calculi can be presented in terms of bi-functors.

// The λ-calculus with an explicit representation of divergence
M[V,A] = 1 + V + VxA + AxA

// The reflective higher order π-calculus
M[V,A] = 1 + VxVxA + VxA + AxA + V

If we fix V as constant for the moment, then we find our usual suspects as the least fixed points of these functors, µM, w.r.t. A. It turns out that it is perfectly sane to now look for the fixed point w.r.t. V. Then µµM are perfectly realizable types with lots of inhabitants. Moreover, they give rise to a richer notion of substitution (as laid out by Meredith and Radestock). The crucial point is that technique is extensible to virtually every nominal algebra.

Doesn't this conflict with Fraenkl-Mostowski Set Theory?

It turns out that FM-Set Theory, as it is employed by Gabbay and Pitts in their seminal work on nominal theories, does not need its "atoms" to avoid internal structure. Rather, it requires that the operations of the set theoretic apparatus to be inured to it. Using this little observation, we can employ exactly the same trick as above to rid FM-Set Theory of a dependency on an unrealizable oracle.

In my view, heavily influenced by computing as it is, i see the basics of set theory as providing some operations for constructing and inspecting, de-structing a data type called Set. Very primitively, we have operations for

• extensionally constructing sets, '{ ... }' and
• operations for intensionally constructing sets '{ ... | ... }' (comprehensions)
• operations for inspecting sets 'x in ... '

In this view, nothing prevents me from imagining two different versions of this data type. One of which i will call the 'black' version and one of which i will call the 'red' version. Initially, i might imagine these data types as copies of each other; but, we can only construct and inspect 'black sets' with 'black' braces and 'black' in predicate; and likewise for the 'red sets'. So, never the twain shall meet.

Now, once we've built such a structure, there's nothing to prevent us from imagining that the 'atoms' of a 'black' FM-set theory are none other than 'red sets'. Symmetrically, nothing prevents us from imagining that the 'atoms' of a 'red' FM-set theory are none other than 'black sets'. A suggestive use of data type specifications might illustrate the idea

• Ordinary sets

Set ::= '{' Set* '}'

• Red/black sets

BlackSet ::= '{b|' (BlackSet + RedAtom)* '|b}'
RedSet ::= '{r|' (RedSet + BlackAtom)* '|r}'
RedAtom ::= RedSet
BlackAtom ::= BlackSet

It should be possible to use algebraic set theory to give a presentation of this idea as an instance of the idea used above.

Conclusions

Lots of useful and interesting computational theory and implementation can take place without inspecting the internal structure of names. Thus, the current state of the theory nominal computational phenomena represents a useful separation of concerns. However, when we acknowledge the real burden on theories of computation that endure a dependency on an unrealizable oracle, we can also begin to explore some of the things that become possible with nominal structure. As mentioned previously, this sort of structure leads to a host of new substitution strategies, only one of which is investigated in Meredith and Radestock's papers. There are other potential benefits as well.

It turns out that McBride and others have given a completely generic and precise definition of location within a structure determined by the kinds of functors we see in nominal algebras. Specifically, they demonstrate that the type of pairs ∂µM x µM -- where ∂µM is the type of contexts of µM, and is calculated according to rules that exactly match the calculations of a derivative in ordinary differential calculus -- represents the type of location as originally investigated by Huet in the functional pearl on the Zipper. It becomes possible to realize nominal algebras in which the internal structure of names is given in terms of locations in the terms of the algebras. Formally, M[∂µM x µM,µM] will provide this kind of capability. You can see functioning Haskell code realizing this for the λ-calculus, here. This sort of structure is of great interest to those who -- like every programmer on the web -- recognize that there is some basic relationship between names like URLs and the basic structure of the containers they access (like websites).