User loginNavigation |
Dedekind, Cantor, Conway, & Hewitt (w/ some Chomsky)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":
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". By Thomas Lord at 2015-06-22 20:53 | LtU Forum | previous forum topic | next forum topic | other blogs | 3977 reads
|
Browse archives
Active forum topics |
Recent comments
20 weeks 1 day ago
20 weeks 1 day ago
20 weeks 1 day ago
42 weeks 2 days ago
46 weeks 4 days ago
48 weeks 1 day ago
48 weeks 1 day ago
50 weeks 6 days ago
1 year 3 weeks ago
1 year 3 weeks ago