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
While chatting with Andrew Appel in the early days of the 2006 Federated Logic Conference, I explained a little about the way I simplify Lisp’s fundamental data model for my miniature system, Miser. Appel suggested that, especially with immutability and no cycles, Miser should be very amenable to inductive proofs and related simplicities. But Andrew also thought that the way I made the primitive functions closed and total would turn out to be an ugly hack. Appel’s intuition is that the hack will make reasoning and proofs unnecessarily difficult. I see how that might be, although I remain attached to the hack until I can confirm the trade-off more closely.
I think the basic hack, to have the three primitive operations corresponding to those of Lisp be total, holds up. But there are other ways in which I will have to be very careful. Here’s the part that I think is safe enough.
oMiser, the pure, entry-level computational model for the Miser Project, uses a pure Lisp-like storage model and an untyped system. There is a single ground type (Ob, where in pure Lisp it is SEXPR) and the system is closed over that type—operations on elements determine elements only of that type and are defined only on elements of that type.
The computational model has unstratified control: any data structure is also program and vice versa. These qualities are fundamental to Miser. The implementation is as close to a theoretical model of universal computation as we can get, allowing us to explore and comprehend the opportunities and limitations of such models in concrete, demonstrable terms.
The basic data model involves the following functions, illustrated in the oMiser logo.
ob.c(x, y) corresponds to Lisp’s cons[x;y] and the result is the ordered pair that has x as its a-path and y as its b-path. (I refer to the components of ordered pairs as the a-path and b-path to emphasize that access is best thought of as navigation—movement of attention—not construction and destruction.)
ob.a(z) corresponds to Lisp’s car[z]. The choice of which of ob.a and ob.b are thought to be the first or second or left or right or other aspect of ordering is arbitrary. It is only necessary that we be consistent with whatever view is chosen. We will see, later on, that introduction of an asymmetry will predispose our choice of idioms for the natural representation of lists and other structures. Operationally, the implementation of ob.b is not allowed to be slower than that for ob.a.
ob.b(z) corresponds to Lisp’s cdr[z] and basically selects the component of z that is generally not the one ob.a determines (unless they happen to be the same).
If z = ob.c(x, y), then ob.a(z) = x and ob.b(z) = y, where “=” is equality in the system. This “=” corresponding to Lisp’s equal[x;y].
The First Hack
The first Miser hack is related to the differentiation between ordered pairs and individuals (the Miser counterparts of Lisp atoms and set-theoretic ur-Elements). Individuals are not themselves ordered pairs and must in some way be simply taken as given.
In Lisp, there are elements, m, for which it cannot be shown that there are x and y such that m = cons[x, y]. The Lisp atoms have this quality: it is inadmissible to suppose car[m] or cdr[m] in the case atom[m]. That is, car and cdr are undefined on atoms.
It has been my thinking that having ob.a and ob.b be total (defined for all elements) enriches the availability of programming idioms and simplifies implementations by avoiding exception checks. I was inspired by those practical considerations and the useful fact that there are never, ever cyclic structures in Miser Obs.
So I make ob.a and ob.b total: ob.a(x) and ob.b(x) are each defined on all elements x.
The Miser individual is the counterpart of the Lisp atom (in Lisp, satisfying atom[x]). For every Miser individual, x, ob.a(x) = ob.b(x) = x. Furthermore, ob.c(ob.a(z),ob.b(z)) is never z when is-individual(z), but it is always z when z is some ob.c(x, y).
The only difference in this case is that instead of requiring some oracle to determine atom[x], we have a structural feature of the system of elements that allows individuals to be distinguished by inspection (which is to say that “=” has all of the oracular power that we require).
Furthermore, needing to qualify certain theorems/axioms by whether or not there are individuals involved is no more difficult, I claim, than the current situation with Lisp when certain functions are undefined for atoms.
Justifying the Hack
As for Lisp, the equality of Miser objects is definable as a structural identity that preserves the equality-by-parts that is fundamental to the nature of ordered pairs: if the corresponding parts of two ordered pairs are the same, the pairs are equal and the pairs are different otherwise.
In both Lisp and Miser, equality-by-parts applies only for constructions (that is, elements z that are asserted to be determined by cons[x;y] or ob.c(x, y)). That is sufficient.
If you look at a procedure for implementation of Lisp equal[x;y] or the Miser x=y, the occurrence of atoms (or individuals) is separated out and some different implementation-specific oracle is used to determine whether atoms (individuals) are the same or not.
The Lisp hack involves reliance on use of atom[x] and eq[x; y] for atoms x and y. With Miser the means for differentiating individuals is not visible, but one can always determine computationally when a Miser individual is in hand by virtue of ob.a(x) = x being satisfied. (The choice of ob.a is related to the second hack, visible in the diagram above but not yet addressed in this discussion.)
I claim that either approach is equally tractable (or equally intractable if you prefer). Atoms (individuals) are distinguishable from ordered pairs, and the principles for inference of characteristics of pairs are essentially the same.
I realize that there is the odd case where one cannot make deductions about x and y based on ob.a(x) = ob.a(y) without determining whether both are individuals or not. This is not a new problem. With the Lisp model, one must avoid applying deductions that are valid when z is a cons[x;y] and not when atom[z]. The guards that must be incorporated in deductions and in identities are essentially the same.
Going Too Far?
If I had stopped here, I think there is no problem and I would be confident that I need not be too concerned about Appel’s objection. I would certainly keep his warning in mind and be on the lookout for difficulties when I have more practice at reasoning about Miser and its programs.
But I didn’t stop here, and I will take up the next hack in a separate note.
Updated 2007–05–02: The link to the image was broken as a result of web site transfer. I restored it for now. The image will be moved shortly and I will need to correct it again. [This update also plants the just-added ClustrMap on this article.]
Updated 2007–05–03: I moved the image as part of refreshing the Miser Project site; I have returned to correct the image in this post one more time. I don’t know why the 2007–05–02 change did not take effect.
|You are navigating The Miser Project.|