*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

- the names have no internal structure

*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

- Red/black sets

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).

## 16 comments:

你的文章給我力量！感謝您!!!............................................................

Hi, Greg,

It's going to take me a few readings to get any sort of deeper understanding of what's going on here, but I have what I hope is a more basic question.

Can you shed any light on the relationship between a logical 'or' and numeric addition in the context of the derivatives that you refer to in this post? I've known that the '+' symbol is occasionally used to refer to a logical or operation, but have never understand why the symbology is shared with numeric addition. Is there some more fundamental common principle?

Dear Kris,

Are you familiar with what's called a Boolean Algebra which is also a Boolean Ring? Are you familiar with the notion of model? The power set of a set provides a most basic model of these algebraic structures. i ask these questions to get some context to understand how to answer your question.

Best wishes,

--greg

Purely Functional Structured Programming was posted today on the list and its use of rebinding names to retain idiomatic control structures while avoiding side effects reminded me of this stuff. :)

I don't find it any more intuitive than traditional FP approaches but maybe some old imperative dogs could learn some new tricks this way?

人們不缺少力量，他們缺少意志。..................................................

臨淵羨魚,不如退而結網。............................................................

成熟，就是有能力適應生活中的模糊。............................................................

Learning makes a good man better and ill man worse.............................................................

信心是命運的主宰!! trust yourself!!!............................................................

愛，拆開來是心和受兩個字。用心去接受對方的一切，用心去愛對方的所有。......................................................................

I love readding, and thanks for your artical.............................................................

做些小善事，說些愛的字句，世界更快樂。..................................................

Pen and ink is wits plough...................................................................

成熟，就是有能力適應生活中的模糊。............................................................

原來這世上能跟你共同領略一個笑話的人竟如此難得......................................................................

感謝你的分享 要繼續發表好文章喔..................................................

Post a Comment