Tidy programs

Open In Colab

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.

!python -m pip install -U setuptools
!python -m pip install -U git+https://github.com/lmoss/onesharp.git@main
from onesharp.interpreter.interpreter import *

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 \(\onett^k \hash\hash\hash\), then \(i +k \leq N +1\).

(b) If line \(i\) is a backward transfer instruction \(\onett^k \hash\hash\hash\hash\), then \(i-k \geq \onett\).

(c) If line \(i\) is a case instruction \(\onett^k \hash\hash\hash\hash\hash\), 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. \(\onett^k \hash\hash\hash\hash\hash\). If Rk started with a \(\hash\), then executing \(\onett^k\ \hash\hash\hash\hash\hash\) would take us to line \(N+3\), and there is no such line. For the same reason, lines \(N-\onett\) and \(N-2\) cannot be case instructions.

Exercise 52

Prove that every program is strongly equivalent to a program in which the none of the last three instructions are case instructions \(\onett^n \hash^5\).

Proposition 7

Every program is strongly equivalent to a tidy program. Moreover, there is a program \(\tidyprog\) such that for all programs \(p\), \([\![\tidyprog]\!](p)\) is a tidy program strongly equivalent to \(p\).

Exercise 53

Prove this proposition. (Alternatively, write a program in either Python or \(\onesharp\) which found a tidy version of an input program.)

Exercise 54

If \(p\) is tidy, show that \(p\) is strongly equivalent to every program of the form

\[ \onett\hash^3 \cdots \onett\hash^3 \quad p \quad \onett\hash^3 \cdots \onett\hash^3 \]

Show that all three parts of the definition of tidiness are needed in order to show this fact.

Exercise 55

Let \(q\) be tidy, and assume that \([\![ p ]\!](x) \simeq y\). Show that the following are equivalent:

  1. \([\![ p+q ]\!](x)\!\downarrow\).

  2. \([\![ q ]\!](y)\!\!\downarrow\).

  3. \(([\![ q ]\!]\circ [\![ p ]\!])(x)\!\!\downarrow\).

(Joshua Burns) Show that in general we need \(q\) to be tidy to have (1)\(\Rightarrow\)(2).

Exercise 56

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 57

Let \(p\) be a tidy program. Show that there is a program \(q\) with the following properties:

  1. \(q\) is strongly equivalent to \(p\).

  2. 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 58

Show that the union of two computably enumerable sets is computably enumerable.

[Hint: use Exercise 57.]