make-ord is used rather than cons is that it
allows us to reason more abstractly about the ordinals, without
having to worry about the underlying representation.
Major Section: PROGRAMMING
Make-ord is the ordinal constructor. Its use is recommended instead of
using cons to make ordinals. For a discussion of ordinals,
see ordinals.
For any ordinal, alpha < epsilon-0, there exist natural numbers p and
n, positive integers x1, x2, ..., xn and ordinals
a1 > a2 > ... > an > 0 such that alpha > a1 and
alpha = w^(a1)x1 + w^(a2)x2 + ... + w^(an)xn + p. We call a1 the ``first
exponent'', x1 the ``first coefficient'', and the remainder
(w^(a2)x2 + ... + w^(an)xn + p) the ``rest'' of alpha.
(Make-ord fe fco rst) corresponds to the ordinal
(w^fe)fco + rst. Thus the first infinite ordinal, w (omega), is
constructed by
(make-ord 1 1 0)and, for example, the ordinal
(w^2)5 + w2 + 7 is constructed by:
(make-ord 2 5 (make-ord 1 2 7)) .
The reason make-ord is used rather than cons is that it
allows us to reason more abstractly about the ordinals, without
having to worry about the underlying representation.