Collaborative articulation of how abstraction and language is employed in the computational manifestation of numbers -- including analysis of the role of syntax, semantics, and meaning in the specification and use of software interfaces.
The nfoCentrale Blog Conclave
nfoCentrale Associated Sites
Technorati Tags: orcmid, Andrew Appel, FLoC2006, Miser, Lisp, primitive operations, computational model, abstract data, array theory, axiomatic data structures, Trenchard More
In Miser Hacks I: Floating Along the Ground (2006-08-21), I described how the Miser Ob data type has an equivalent structure to the fundamental data structure of Lisp.
Lisp has a supply of atoms, the cons[x;y] pair operation, and the access functions car[z] and cdr[z].
In Lisp, the structure is completed by equal[x;y] and by atom[x], the "oracle" that informs us when some z is not a cons[x;y] and for which car[z] and cdr[z] are consequently undefined (and, in modern implementations, these are invalid operations). Lisp is defined with another oracular operation, eq[x;y] that for atoms, reports whether or not x and y are determined to be the same atom (or not).
Lisp is computationally universal and profoundly interesting by virtue of a specified universal function by which all computable functions on these structures can be carried out using programs coded in such structures.
Miser uses a similar approach, having a supply of individuals and corresponding functions ob.c(x, y), ob.a(z), and ob.b(z), with "=" for equality among obs. (There is a function ob.d(x, y) that determines equality/inequality within the computational model of the system. That is different than "=" since there are no obs that are recognized as true/false although there are idioms that tend to serve that purpose. That's another hack to be described, and it is an elegant one although I once muddied it by adding more hack than needed.)
The Story So Far
For Miser Ob, the functions ob.a and ob.b are total. Whether or not ob z can be formed by some ob.c(x,y), ob.a(z) and ob.b(z) always determine obs. The Miser individual is the counterpart of the Lisp atom. It is the case that z is an individual if and only if ob.a(z) = z. Technically, the oracular power necessary to distinguish atoms has been moved entirely to "=" in Miser. This works because it is impossible, in Miser, that there be any z such that ob.c(z, x) = z, even when ob.a(z) = z. So we can define our equivalent of atom[z] as simply
If is-individual(z), it is also the case that z = ob.b(z), but z = ob.a(z) is sufficient to discriminate all individuals.
In Miser Hacks I, I argued that having a structural distinction that discriminates atoms (i.e., individuals) entirely within the system is no more of a problem than having to condition certain statements and derivations depending on the presence of atoms. The guarding of deductions about Miser with is-individual conditions is no different than the need to be guarded with atom conditions in Lisp.
Clinging to Idioms
I claim that having structural features for discrimination is advantageous in the ease with which useful idioms become available, idioms that don't require us to have to be cautious against performance of undefined or invalid operations. So I am clinging to this idiomatic power in Miser. There will be many manifestations of such idioms.
An example of an idiomatic usage of Lisp is in the notion of list. In pure Lisp with no additional types (pretty much ditto for oMiser), there are only atoms and cons pairs. The fundamental data structure is a binary tree. (We ignore the prospect of cycles among cons-pairs, permitted in Lisp but impossible in Miser.) The representation of lists in Lisp is by transiting the cdr-path all the way until an atom (the NUL) is reached. At each point, starting with the whole list, and excluding the terminal atom, the list elements are the car-values at each cons-pair node along that cdr-taken path. That is so useful it is the default sense of the Lisp data structure in common usage. It is the typical representation of Lisp symbolic expressions (SEXPRs).
Singletons and Enclosures
In my preference for idiomatic cases and my yearning for additional representation opportunities, I take advantage of another structural distinction in defining the Miser Ob structure.
Singletons. Any ob, z, for which ob.b(z) = z is a singleton.
Individuals are singletons. In the diagram, the ob identified as x and found at both ob.a(z) and ob.a(ob.b(z)) is an individual and a singleton. This is a structural quality. The names chosen for these qualities has to do with an intended usage, but it is not necessitated by the structure. So we are fashioning idioms and metaphors already.
Enclosures. The other kind of singleton is an enclosure. An enclosure satisfies the condition
is-enclosure(z) = is-singleton(z) and not is-individual(z)
where is-singleton(z) = (ob.b(z) = z)
as expected. In the diagram, ob.b(z) is the enclosure, y, defined as ob.e(x).
Now, just as for individuals, it is impossible for there to be an ob.c(x, y) such that
Making enclosures with ob.e. We've managed to finesse where individuals come from (there being guaranteed to be at least one, designated ob-null), and here comes a completely-separate breed of ob. The Miser function ob.e(x) takes any ob and provides an enclosure of it. That is,
Idiomatically, an ob enclosure can be viewed as a container that wraps up an ob and distinguishes it as a singleton. One might choose to use it, in a Miser application, as a way to separate out enclosures for treatments like individuals rather than a continuation of some represented data structure, such as a tree or a list. Also, notice how one might consider to treat individuals as literals: singletons that enclose themselves (metaphorically of course: no individual is an enclosure).
The use of enclosures for various practical purposes is not determined by the the Ob-structure theory.
Enclosures as Quotations
There is a place where enclosures (and individuals and ob.c constructions) are interpreted in a particular way. That is in the context of the standard oMiser universal function. That function, ob.ap(f, x), and its companion, ob.ev(f, x, p), treat enclosures as quotations. ob.e(x) is Miser's structural counterpart to the Lisp use of cons[QUOTE; x] in the standard Lisp universal function.
To illustrate (but not explain) how this works for Miser,
Other features of oMiser and the Frugal processor (which provides a way to input and operate Miser programs) reinforce the enclosure-as-quotation interpretation. It is not the only interpretation, any more than a Lisp occurrence of the QUOTE atom is compelled to have anything to do with quotation in the context of the Lisp universal function.
It is very handy to have a structural form of quotation that is completely separate from the use of atoms or individuals as markers. The use of enclosures in Miser accomplishes that. There will also be use of distinct individuals as special markers in ob.ev operation but those hacks come up later. Other markers are introduced in ad hoc conventions such as ones for ascribing types to enclosures. Those practices are unrelated to the definition of the universal oMiser function and the axiomatic theory of ob structures.
Justifying the Hack
The main purpose of enclosures is to provide a structural mechanism that is easily used to control the depth to which various procedures intrude into the structure of an ob (ob.ap and ob.ev procedures being two examples). Enclosures are a simple, primitive device that supports this need for quotation by structural means along.
There is precedent for a structural quotation feature. It matters in array theory where one wants sub-arrays or sub-something as elements of the arrays that contain them. In this respect, the Miser nomenclature around individuals and singletons honors the array-theory work of Trenchard More.
Another precedent, and the one that I learned first, has to do with stratified strings: strings that can have strings as their individual "beads." This sort of string was defined for ALGOL 60, which introduced a notation for strings as elements (not sub-strings) of containing strings. Although the mechanism did not survive ALGOL 60 where it was seriously under-developed, it offered an existence case for an use of quotation to make string elements out of entire strings.
Christopher Strachey developed a general-purpose macro processor (affectionately known as McG in one implementation) that relied upon stratified strings in a way quite similar to the use of enclosure in the Miser universal function. It was recognition of an omission that prevented universality over such strings that started me on the road that led to the current formulation of oMiser.
Finally, it is useful in theory-focused settings to notice that introduction of enclosures does not in any way extend the cardinality of Ob, the set of all obs. That is, Ob with enclosures is just as denumerable as Ob without them. In this sense, enclosures do not add any inherent power to Miser, yet they simplify the expression of certain kinds of data representations and provide a simpler expression of a universal function. The way that this miniature feature facilitates expressiveness is an useful subject of study and analysis.
Finally, as you can tell, I am infatuated with this feature and will not surrender it lightly. There are enclosures and they harmonize in the play of singletons and individuals and obs composed via ob.c. I like it that way.
Gone Too Far Yet?
What has me look at enclosure as a Miser hack is the degree to which their possibility complicates reasoning about ob structures, the concern that Andrew Appel raised over having ob.a and ob.b be total and defined on individuals. I don't think it complicates reasoning about the universal function much at all. It singles out quotation for the added attention I think it deserves, and however quotation is handled (such as in Lisp) it has to be singled out in the universal function. It is the means by which data is embedded in procedure embedded in data embedded in ... , and it demonstrates that quite simply. Since this is a fundamental matter in computing and its quasi-linguistic character, enclosures seem like an useful idea.
The introduction of enclosures does add cases that must be accounted for in the low-level derivation of proofs about algorithms on obs and the correctness of representations of one kind or another. I haven't found that to be a problem at the low-level so far. I expect that, when one moves up to higher levels of abstraction, any complication due to enclosures becomes irrelevant and disappears. I am open to challenge as I move along. I would be surprised to have to abandon enclosures at some future time.
But Wait, There's More!
There is another hack that qualifies for my ugliest language-theory hack ever. I was proud of that one too until I found the counter-example that defeated the whole enterprise. To show that I am not totally unwilling to reconsider my pet features, I'll show you the hack I'm too embarrassed to keep around even though no substitute is particularly pleasant.
Stay tuned ...
I know it's been a long time since Miser Hack I and the inspiration that I took out of FLoC 2006 and the subsequent ICFP 2006 in Portland, Oregon. I have been working along silently and infrequently. Meanwhile, I on a different commitment unrelated to functional programming and applicative systems such as Miser. Some of that work is useful as preparation for a Miser implementation. I think I have found an appropriate way to break out of my silence and proceed in parallel with that other work.
This break in my prolonged silence was inspired by Charles Petzold's announcement of his forthcoming book, The Annotated Turing. Without knowing anything about how that work will unfold, I feel kinship with the spirit of that effort and this is my offering from the chorus, uh ... peanut gallery, oh uh ... rooting section.
[update 2007-11-12 There is a completely incorrect and misleading statement that I had to repair. I have stricken out the bogus statement and replaced it with an appropriate one around how no ob.c(x, y) can ever be a singleton.]
|You are navigating The Miser Project.|