Tidy programs#
The idea of tidiness is that it should be a condition on programs \(p\) which ensures that no matter what the registers contain when we begin executing \(p\), no instruction can possibly take us outside of \(p\), except for going “one instruction below the end”. The execution might not halt due to an infinite loop that is inside of \(p\), but it will not halt improperly. For example, line \(3\) cannot be \(\onett^3\hash^4\).
This description of tidiness is semantic: it has to do with program execution. We will eventually see that this kind of condition is undecidable. What we are after is a syntactic condition that is strong enough to do what we want, and yet be decidable. We also want to know that every program is equivalent to a tidy program.
!python -m pip install -U setuptools
!python -m pip install -U git+https://github.com/lmoss/onesharp.git@main
from onesharp.interpreter.interpreter import *
Here are some examples of what we are after. if the last line of a program \(p\) is 1#, then that line transfers control outside of \(p\), but only one line below the end. On the other hand, if a program \(q\) has exactly \(10\) lines, then we do not want line \(8\) to be 1111###, since executing this line would take us to “line 12”. So a run of \(q\) which reached line \(8\) would not halt.
We would prefer to rewrite \(q\) to point to an infinite loop inside of the program.
(There are reasons that we prefer programs to have explicit infinite loops instead of pointing to unwanted places. One such reason appears in on-tidiness below. Other reasons for this preference will be revealed in due course.)
Informally, we say that a program \(p\) is tidy if no instruction can possibly take us outside the program, except for going “one instruction below the end” of \(p\).
What we are after here is a formal definition of tidiness.
Definition
Suppose that \(p\) is a program with \(N\) instructions. Here are the requirements for \(p\) to be tidy:
(a) If line \(i\) is a forward transfer instruction
1\(k\)###, then \(i +k \leq N+1\).
(b) If line \(i\) is a backward transfer instruction 1\(k\)####, then \(i-k \geq 1\).
(c) If line \(i\) is a case instruction 1\(k\)#####, then \(k+2 \leq N\).
Here is a comment on condition (c).
Suppose that \(p\) had \(N\) lines, and line \(N\) were a case instruction
1\(k\)#####. If Rk started with a #, then executing 1\(k\)##### would take us to line \(N+3\), and there is no such line.
For the same reason, lines \(N-1\) and \(N-2\) cannot be case instructions.
Exercise 48
Prove that every program is strongly equivalent to a program in which the none of the last three instructions are case instructions 1^n #^5.
Proposition 7
Every program is strongly equivalent to a tidy program. Moreover, there is a program tidy such that for all programs \(p\),
\([\![tidy]\!](p)\) is a tidy program strongly equivalent to \(p\).
Exercise 49
Prove this proposition. (Alternatively, write a program in either Python or 1# which found a tidy version of an input program.)
Exercise 50
If \(p\) is tidy, show that \(p\) is strongly equivalent to every program of the form
1### 1### \(\cdots\) 1### p 1### 1### \(\cdots\) 1###
Show that all three parts of the definition of tidiness are needed in order to show this fact.
Exercise 51
Find a program \(p\) which is not tidy and yet has the property that no matter what the registers contain when we begin executing \(p\), control is never taken outside of \(p\), except for going “one instruction below the end”. The point is that our syntactic condition of tidiness is sufficient for the semantic condition that we want, but it is not necessary.
Exercise 52
Let \(q\) be tidy, and assume that \([\![ p ]\!](x) \simeq y\). Show that the following are equivalent:
\([\![ p+q ]\!](x)\!\downarrow\).
\([\![ q ]\!](y)\!\!\downarrow\).
\(([\![ q ]\!]\circ [\![ p ]\!])(x)\!\!\downarrow\).
(Joshua Burns) Show that in general we need \(q\) to be tidy to have (1)\(\Rightarrow\)(2).
Exercise 53
Let \(p\) be a tidy program. Show that there is a program \(q\) with the following properties:
\(q\) is strongly equivalent to \(p\).
In \(q\), every backward-transfer instruction points to the top of the program. That is, if line \(i\) of \(q\) is \(\one^k \hash^4\), then \(k = i-1\).
Exercise 54
Show that the union of two computably enumerable sets is computably enumerable.
[Hint: use Exercise 53.]