Lambda the Ultimate

Here, I will attempt to cool down controversy on LtU over Hewitt's construction of Real by explaining it in more familiar terms. I think this will help to shed some light on Direct Logic and begin to hint why it is interesting in a PLT context.

I will borrow conceptually from John H. Conway who wrote, in "On numbers and games":

Let us see how those were good at constructing numbers have approached this problem in the past.

Dedekind (and before him the author -- thought to be Eudoxus -- of the fifth book of Euclid) constructed the real numbers from the rationals. His method was to divide the rationals into two sets L and R in such a way that no number of L was greater than any number of R, and use this "section" to define a new number {L|R} in the case that neither L nor R had an extremal point.

His method produces a logically sound collection of real numbers (if we ignore some objections on the grounds of ineffectivity, etc.), but has been criticised on several counts. Perhaps the most important is that the rationals are supposed to have been already constructed in some other way, and yet are "reconstructed" as certain real numbers. The distinction between the "old" and "new" rationals seems artificial but essential.

Cantor constructed the infinite ordinal numbers. Supposing the integers 1,2,3... given he observed that their order-type ω was a nwe (and infinite) number greater than all of them. Then the order-type of {1,2,3...,ω} is a still greater number ω + 1, and so on, and on, and on. The similar objections to Cantor's procedure have already been met by von Neumann, who observes that it unnecessary to suppose 1,2,3,... given and that it is natural to start at 0 rather than 1. He also takes each ordinal as the set (rather than the order-type) of all previous ones. Thus for von Neumann, 0 is the empty set, 1 the set {0}, 2, the set {0, 1}, ..., ω the set {0, 1, 2, ...} and so on.

In this chapter [Conway teases] we intend to show that these two methods are in reality part of a simpler and more general method by which we can construct a very large Class No of numbers, including at the same time the real numbers and the ordinal numbers, and others such as those mentioned above [e.g. infinitessimals] [....]

Hewitt can be read as constructing Real by specifying a set of 3-way partitions of the dyadic fractions between 0 and 1.

Every Real in [0..1] corresponds to three sets: {L | M | R}

The sets are ordered so that no member of L is greater than or equal to any member of M or R, no member of M is greater than or equal to any member of R.

  Zero:

  0 ≡ {{} | {} | Dyad} 
  where Dyad is the set of all dyadic fractions between 0 and 1

  One:
  1 ≡ {Dyad | {} | {}} 

Hopefully the dyadic fractions are themselves members of Real and we can memorialize that fact in a manner similar to Dedekind:

  ∀d ∈ Dyad, {dl | { d } | dr } ∈ ℝ

  where dl ≡ { x ∈ Dyad | x < d }
    and dr ≡ { x ∈ Dyad | x > d }

  Note: the Real {dl | { d } | dr } is called d.

The rationals in general correspond to regular languages as follows:

  Let Rat be the set of of sets of finite strings of 0 and 1 such that:

  ∀r in Rat, r is a regular language
    r is well ordered by a prefix relation
    ∀s in r, s is finite length and ends with 1

    rl ≡ { d ∈ Dyad | ∃x ∈ r, x > d }
    rm ≡ { d ∈ r | ∀x ∈ r, x <= d }
    rr ≡ { d ∈ Dyad | ∃x ∈ r, x < d }

   Note: the Real { rl, rm, rr } is called r }

As you can see, the subset of Real given by Rat is the set of all rational fractions between 0 and 1.

The rationals are given by certain regular languages over the alphabet {0,1}. Similarly, the constructible reals are given by certain recursivvely enumerable languages.

  Let Tructable be the set of all recursively enumerable sets of finite 
  strings of 0s and 1s, each string ending with a 1, such that each member
  of Tructable is well ordered by a prefix relation.

  By analogous construction to the rationals:

  ∀ t ∈ Tructable, { tl, tm, tr } is in Real

All rationals (dyadic and otherwise) are Tructable.

Finally, we consider a set of languages of finite strings for which the generator functions are non-deterministic.

  Let Fracs be the set of all sets of finite strings of 0s and 1s, 
  each string ending with a 1, such that each member of Fracs is
  well ordered by a prefix relation.

  By analogous construction, 

  ∀ f ∈ Fracs, { fl, fm, fr } is in Real

Note that if a member f of Fracs has a maximal element, then f is also a dyadic rational.

Note that if a member f is a regular language over {0,1}, then it is a rational.

Note that if a member of f is a recursively enumerable set, then it is a tructable real.

There are other possibilities. By a diagonalization argument, we know that Fracs contains members f which are not recursively enumerable. Those f are the unconstructible reals.

Let's suppose that the real world contains fair randomness. For example, there is a coin flip or some other kind of measurement we can repeat that will produce random outcomes. Neither heads or tails will be permanently starved. A sequence of coinflips on a given world-line will eventually produce both a 0 and a 1. Furthermore, on some world-lines, the sequence of coin flips is not described by any recursively enumerable function (at least assuming that there is no upper bound on the number of times we get to flip the coin).

The number of possible world-lines on which coin flips might be recorded is uncountable and, indeed, corresponds nicely to the members of Fracs.

In other words, a machine can enumerate the members of any f in Fracs, from shortest to longest. Such a machine, on a particular world-line, is pretty much what Hewitt means by an "Actor address".