- #1
SSequence
- 557
- 95
Background:
This is going to be a shorter thread compared to the last thread I made, which was quite long. It is related to a question I posted on MSE/mathoverflow few weeks ago (https://math.stackexchange.com/questions/3403361/eventual-writability-general). The linked thread also contains the link to mathoverflow version. For the notion of EW-real see definition-3.10 (https://arxiv.org/abs/1512.06101). Note that the context in which the definition is posted is quite advanced, but the definition itself is fairly simple to understand.
The stabilization time is the smallest time at which the output stabilizes. To summarize, what I essentially posted there was that stabilization times for every program can't be ##<\omega^L_1##. In other words, the supremum of stabilization times must be greater than ##\omega^L_1##. The answers on both sites confirmed that there must be programs with stabilization times ##
\geq \omega^L_1##. A simpler way to see it (than I described) was given in the answer to mathoverflow version (the last paragraph of the answer there).
For the rest of the post I will write "eventually writable" as EW. Also, "code for ordinal ##\alpha##" means "a well-order of ##\mathbb{N}## (in suitably encoded form) with order-type ##\alpha##".
Some Context:
There are two notions in which ordinals can be naturally related to stabilization:
(1) The output section of the program stabilizes with a code for an ordinal, never to change again. Note that this is the definition for an EW-ordinal. That is, an ordinal ##\alpha## is EW iff there exists a program whose output section stabilizes while containing a code for the ordinal ##\alpha##. In this case we say ##\alpha## is an EW-ordinal.
(2) There is a variable (say ##v##) in a program which stabilizes permanently to ##\alpha## (never to change its value again). We say that ##\alpha## is eventually markable ordinal. Or, in other words, we can say that the given program eventually marks ##\alpha##.
Few points to note before proceeding:
(i) The programs always start completely blank (no input or parameters etc.).
(ii) In point-(1) a program may stabilize permanently without containing a code for an ordinal. In that case still the real number that stabilizes on the output is an EW-real.
(iii) The definition given in point-(2) above might seem to be specific to computational model. But it isn't too difficult to give an equivalent definition in terms of OTMs (see the answer to MO version of the question for example).
I want to discuss a notion which is more strict than the notion of eventually markable.
(3) There is a variable (say ##v##) in a program which stabilizes permanently to ##\alpha## (never to change its value again) without the variable ##v## ever descreasing. In this case we say that ##\alpha## is eventually pointable ordinal. Or, in other words, we can say that the given program eventually points to ##\alpha##.
For this definition, we may suitably restrict ourselves to program where there is no command decreasing the value of ##v##.
Summary:
Let ##\eta## be sup of EW-ordinals. Let ##\eta_0## be sup of those ordinals whose code has eventually stabilized on the output at some time ##<\omega^L_1##. Obviously we have ##\eta_0<\eta##. Another thing to note is that the sup of markable ordinal which have eventually stabilized on the output at some time ##<\omega^L_1## is also ##\eta_0##. Generally the sup of markable ordinals will be well-beyond ##\omega^L_1## (as was noted in linked threads).
Now one immediate question is that what is the sup of those eventually pointable ordinals which are countable (note that sup of pointable ordinals isn't countable because ##\omega^L_1## can be shown to be pointable). It can be shown that this is ##\eta_0## too. The next question is that whether the pointable ordinals below ##\eta_0## have jumps/gaps or not? In other words, is there an ordinal ##<\eta_0## which isn't pointable. I think it can be shown that, in fact, there are gaps in the countable pointable ordinals. And it shouldn't be difficult to show.
For this, we want to define a notion of ##C_i## (with ##i \in Ord##). Define ##C_0## be to be sup of clockable values. Define ##C_{i+1}## (from##C_i##) to be sup of ordinals that are clockable given arbitrary parameters ##\leq C_i##. For limit values ##j## define ##C_j## as:
##C_j=sup\{C_i|i<j\}##
With this we can show the following:
---- ##C_{\omega^L_1}=\omega^L_1##
---- ##\eta_0## is one of the ##C_i##'s. In other words, there exists a ##q<\omega^L_1## such that ##\eta_0=C_q##
---- All stabilizations for EW-ordinals that occur in countable time in fact occur below ##\eta_0## time (and actually, the supremum of the stabilization times for these specific stabilizations is ##\eta_0##). So, in that sense, the initial comment on the MSE answer is right.
---- The set of pointable ordinals below ##\eta_0## have jumps/gaps.
P.S.
Now the last point isn't problematic. After all there are gaps in clocking/halting positions too (on empty input). However, there is something that is strange for me here specifically. I will describe it in the next post.
This is going to be a shorter thread compared to the last thread I made, which was quite long. It is related to a question I posted on MSE/mathoverflow few weeks ago (https://math.stackexchange.com/questions/3403361/eventual-writability-general). The linked thread also contains the link to mathoverflow version. For the notion of EW-real see definition-3.10 (https://arxiv.org/abs/1512.06101). Note that the context in which the definition is posted is quite advanced, but the definition itself is fairly simple to understand.
The stabilization time is the smallest time at which the output stabilizes. To summarize, what I essentially posted there was that stabilization times for every program can't be ##<\omega^L_1##. In other words, the supremum of stabilization times must be greater than ##\omega^L_1##. The answers on both sites confirmed that there must be programs with stabilization times ##
\geq \omega^L_1##. A simpler way to see it (than I described) was given in the answer to mathoverflow version (the last paragraph of the answer there).
For the rest of the post I will write "eventually writable" as EW. Also, "code for ordinal ##\alpha##" means "a well-order of ##\mathbb{N}## (in suitably encoded form) with order-type ##\alpha##".
Some Context:
There are two notions in which ordinals can be naturally related to stabilization:
(1) The output section of the program stabilizes with a code for an ordinal, never to change again. Note that this is the definition for an EW-ordinal. That is, an ordinal ##\alpha## is EW iff there exists a program whose output section stabilizes while containing a code for the ordinal ##\alpha##. In this case we say ##\alpha## is an EW-ordinal.
(2) There is a variable (say ##v##) in a program which stabilizes permanently to ##\alpha## (never to change its value again). We say that ##\alpha## is eventually markable ordinal. Or, in other words, we can say that the given program eventually marks ##\alpha##.
Few points to note before proceeding:
(i) The programs always start completely blank (no input or parameters etc.).
(ii) In point-(1) a program may stabilize permanently without containing a code for an ordinal. In that case still the real number that stabilizes on the output is an EW-real.
(iii) The definition given in point-(2) above might seem to be specific to computational model. But it isn't too difficult to give an equivalent definition in terms of OTMs (see the answer to MO version of the question for example).
I want to discuss a notion which is more strict than the notion of eventually markable.
(3) There is a variable (say ##v##) in a program which stabilizes permanently to ##\alpha## (never to change its value again) without the variable ##v## ever descreasing. In this case we say that ##\alpha## is eventually pointable ordinal. Or, in other words, we can say that the given program eventually points to ##\alpha##.
For this definition, we may suitably restrict ourselves to program where there is no command decreasing the value of ##v##.
Summary:
Let ##\eta## be sup of EW-ordinals. Let ##\eta_0## be sup of those ordinals whose code has eventually stabilized on the output at some time ##<\omega^L_1##. Obviously we have ##\eta_0<\eta##. Another thing to note is that the sup of markable ordinal which have eventually stabilized on the output at some time ##<\omega^L_1## is also ##\eta_0##. Generally the sup of markable ordinals will be well-beyond ##\omega^L_1## (as was noted in linked threads).
Now one immediate question is that what is the sup of those eventually pointable ordinals which are countable (note that sup of pointable ordinals isn't countable because ##\omega^L_1## can be shown to be pointable). It can be shown that this is ##\eta_0## too. The next question is that whether the pointable ordinals below ##\eta_0## have jumps/gaps or not? In other words, is there an ordinal ##<\eta_0## which isn't pointable. I think it can be shown that, in fact, there are gaps in the countable pointable ordinals. And it shouldn't be difficult to show.
For this, we want to define a notion of ##C_i## (with ##i \in Ord##). Define ##C_0## be to be sup of clockable values. Define ##C_{i+1}## (from##C_i##) to be sup of ordinals that are clockable given arbitrary parameters ##\leq C_i##. For limit values ##j## define ##C_j## as:
##C_j=sup\{C_i|i<j\}##
With this we can show the following:
---- ##C_{\omega^L_1}=\omega^L_1##
---- ##\eta_0## is one of the ##C_i##'s. In other words, there exists a ##q<\omega^L_1## such that ##\eta_0=C_q##
---- All stabilizations for EW-ordinals that occur in countable time in fact occur below ##\eta_0## time (and actually, the supremum of the stabilization times for these specific stabilizations is ##\eta_0##). So, in that sense, the initial comment on the MSE answer is right.
---- The set of pointable ordinals below ##\eta_0## have jumps/gaps.
P.S.
Now the last point isn't problematic. After all there are gaps in clocking/halting positions too (on empty input). However, there is something that is strange for me here specifically. I will describe it in the next post.
Last edited: