2.7.15.2 Operator Generalization

Each set in the hierarchy induces a structure preserving cons operator, denoted cons_n for the nth level set, and satisfying this equation.

E10

cons_n(x_n,y_n) = (cons(x,y))_n

It will be convenient to generalize all of these cons operators to be defined on members of other sets than their own.

E11

For m greater than n,       cons_n(x_m,y_p) = x_m

In this equation, p is unrestricted. The intuition is that if the left operand of a cons is the result of a computation that went wrong due to an exceptional condition (more exceptional than n, the level already in effect), then the exceptional result becomes the whole result.

It is tempting to hazard a slightly stronger statement, which is that this equation holds even if y_p is equal to some expression f x that is undefined according to the operator semantics. This stipulation would correspond to an implementation in which the right operand isn't evaluated after an error is detected in the left, but there are two problems with it.

• This semantics might unreasonably complicate a concurrent implementation of the virtual machine. If evaluation leads to non-termination in some cases where the result is undefined (as it certainly would in any possible implementation consistent with cases where it's defined), then the mechanism that evaluates the right side of a pair must be interruptible in case an exception is detected in the left.
• It is beyond the expressive power of the present mathematical framework to make such a statement, because it entails universal quantification over non-members of the constructed sets, which includes almost everything.

Nevertheless, the implementation in avram is sequential and does indeed behave as proposed, with no practical difficulty. As for any deficiency in the theory, it could be banished by recasting the semantics in terms of a calculus of expressions with formal rules of manipulation. An operand to the cons operator would be identified not with a member of a semantic domain, but with the expression used to write it down, and then even “undefinedness” could be defined. However, the present author's preference in computing as in life is to let some things remain a mystery rather than to abandon the quest for meaning entirely.

A comparable condition applies in cases where the right side of a pair represents an exceptional result.

E12

For m greater than n,     cons_n(x_n,y_m) = y_m

Whereas an infinitude of cons operators has been needed, it will be possible to get by with only one invisible operator, as before, by generalizing it in the following way to operands on any level of the hierarchy.

P43

f_n x_n = (f x)_n

P44

For distinct n and m,  f_n x_m = x_m

That is, the result of evaluating two operands on the same level is the image relative to that level of the result of their respective images on the bottom level, but the result of evaluating two operands on different levels is the same as the right operand.