#@title
!python -m pip install -U setuptools
!python -m pip install -U git+https://github.com/lmoss/onesharp.git@main
from onesharp.interpreter.with_traces import *
The T predicate#
If someone claims that \([\![p]\!](x)\!\!\downarrow\), what evidence could they bring to prove their point? In this section we develop an answer. We provide a notion of a trace of a computation. Here are the main points. First, traces are finite words; they cannot be infinite objects. Second, there is a total computable relation \(T(p,x,z)\) such that if \([\![p]\!](x)\!\!\downarrow\), then there is some \(z\) such that \(T(p,x,z)\). But if \([\![p]\!](x)\!\!\uparrow\), then there is no such \(z\). This relation \(T(p,x,z)\) is called the T-predicate.
Carrying out the definition of \(T(p,x,z)\) requires us to make a number of secondary definitions. Some of the discussion is technical because we need to code sequences of words by single words. Please do not get bogged down by the technical details; the ideas are more important, and they are actually easier to grasp without the details of the coding. In other words, the details are important, but they should not get in the way of understanding the ideas.
The foregoing paragraphs were about computation in 1#. After we do this work, we want to port the discussion from words to numbers. This again leads us to a mountain of details about coding. We show that the numerical version of \(T\) is primitive recursive. This leads to the a real result proved using the \(T\)-predicate, the fact that every partial \(\mu\)-recursive function of
numbers is 1#-computable.
Encoding#
We need several levels of encoding, taking ever more complicated types of objects into 1#-words.
Sequences of words as words#
Definition 12
We start by defining a specific encoding map
Here is how our map words first, we define a map
by
In other words, we put a \({\tt 1}\) before each letter in the input word \(a_1 a_2 \cdots a_k\).
Then for a sequence of words we take
We understand that \(c(\varepsilon) = {\tt \#\#}\).
Sequences of (sequences of words) as words#
We also need an encoding of sequences of sequences of words. (But fear not, we do not need to further in this direction.) We define
by
That is, we encode sequences of words using \(c\) from above, and then we use \({\tt \# 1}\) as a separator between such encondings.
Snapshots#
Recall that a snapshot is a number together with a finite sequence of words. We associate snapshots to executions of a program on some inputs; a snapshot is determined by a line number in a program, and with the contents of some finite set of registers. But we want a definition of a snapshot encoding that does not refer to a program or to anything else.
Definition 13
An encoded snapshot is a word of the form
That is, it is a finite sequence of 1s followed by ## followed by \(b(w_1)\) for some word \(w_1\), then ###, then
\(b(w_2)\) for some word \(w_2\), \(\ldots\), and finally \(b(w_{\ell})\) for some word \(w_{\ell}\).
New interface#
Here is a new interface for running program which includes a “mode” capability that includes the option of seeing all the snapshots and the overall trace.
step_by_step_with_snapshots('1#1#',['##'])
snapshot_check('111##1#11#1111##')
Definitions leading up to T#
Definition 14
\(Follows(p,s_1,s_2)\)
means that
\(Program(p)\)
\(Snapshot(s_1)\) and \(Snapshot(s_2)\)
The \(n\) involved in \(s_1\) (the number \(1^n\) at the start of \(s_1\)) is \(\leq\) the length of \(p\)
\(s_2\) is the snapshot that would follow after \(s_1\) according to what \(p\) says.
Definition 15
\(Suitable(p,s)\) means
\(Program(p)\)
\(Snapshot(s)\)
The number of registers represented in \(s\) is the maximum register number that \(p\) deals with, or \(1\) if \(p\) does not mention any registers at all.
In other words, if
then \(k\) is the largest register mentioned in the program \(p\). That is, \(k\) is largest so that \(p\) contains \(1^k \#\) or \(1^k \#\#\) or \(1^k \#^5\).
Definition 16
\(Starting-snapshot(p,w, s)\) means
\(Suitable(p,s)\), and thus \(Program(p)\) and \(Snapshot(s)\)
The instruction number \(n\) in \(s\) is \(1\).
\(w\) is a coded word-of-words
and \(s\) represents the snapshot where \(w_1\) is in R1, \(\ldots\), \(w_k\) is in Rk.
Definition 17
\(Halting-snapshot(p, s)\) means
\(Suitable(p,s)\), and thus \(Program(p)\) and \(Snapshot(s)\)
The instruction number \(n\) in \(s\) is \(1+ m\), where \(m\) is the the number of instructions in \(p\).
The registers coded in \(s\) are all empty, except possibly for R1.
Definition 18
\(Snapshot-seq(z)\) means that \(z\) is a word of the form
where \(Snapshot(s_i)\) for all \(i\).
Definition 19
\(T(p,x,z)\) means
\(Program(p)\)
\(Snapshot-seq(z)\), say \(z\) represents
\(Starting-snapshot(p,w, s_1)\),
where \(w\) is the code of \(\langle x\rangle\), the one-element sequence \(x\), and \(s_1\) is the first snapshot represented in \(z\)
For all \(1 \leq i \leq \ell\), \(Suitable(p,s_i)\)
For all \(1 \leq i < \ell\), \(Follows(p,s_i,s_{i+1})\)
\(Halting-snapshot(p, s_{\ell})\)
We need one more gadget, a function called \(upshot\).
Definition 20
If \(Snapshot-seq(z)\), say \(z\) is
then \(upshot(z)\) is the word in R1 in the last snapshot, \(s_{\ell}\).
If \(\neg Snapshot-seq(z)\), then
we (don’t care about the result and) set \(upshot(z)={\tt \#}\).
Theorem 6
For all words \(p\) and \(x\), \([\![ p]\!](x)\!\!\downarrow\) if and only if there is some \(z\) such that \(T(p,x,z)\).
Moreover, \(T\) is 1#-computable and total.
Indeed, all of the “helper functions” above are also 1#-computable and total.
Shortlex ordering of words#
Our next order of business is to rework everything which we have seen from words to numbers. This involves an encoding. So we start with a bijection \(s: N \to Words\).
\(n\) |
\(s(n)\) |
|---|---|
0 |
\(\varepsilon\) |
1 |
|
2 |
|
3 |
|
4 |
|
5 |
|
6 |
|
7 |
|
8 |
|
9 |
|
10 |
|
11 |
|
12 |
|
13 |
|
14 |
|
15 |
|
Being a bijection, this function \(s\) has an inverse \(s^{-1}\).
The idea now is to take all of the machinery which we have built in this notebook and use \(s\) and its inverse \(s^{-1}\) to transfer them to numbers. In the other direction, we want to take all of the primitive recursive functions of numbers and transfer them to 1#.
Accessing bits#
We next define three functions on the natural numbers. The first is called \(|n|\), and it gives the number of characters in \(s(n)\).
For all \(n\), \(|n|\) is the number of symbols in the string \(s(n)\). The expression above gives a formula for it. For all non-zero \(a\) and \(b\), \(rem(a,b)\) gives the remainder when \(a\) is divided by \(b\). When \(a = 0\), \(rem(a,b) = 0\) as well. When \(a >0\) and \(b = 0\),???
Since all of the quantifiers and \(\mu\)-operators are bounded, these functions are primitive recursive.
Here is a table of the values of this function for small numbers.
\(n\) |
\(s(n)\) |
\(|n|\) |
\((n)_0\) |
\((n)_1\) |
\((n)_2\) |
|---|---|---|---|---|---|
0 |
\(\varepsilon\) |
0 |
0 |
0 |
0 |
1 |
|
1 |
0 |
0 |
0 |
2 |
|
1 |
1 |
0 |
0 |
3 |
|
2 |
0 |
0 |
0 |
4 |
|
2 |
1 |
0 |
0 |
5 |
|
2 |
0 |
1 |
0 |
6 |
|
2 |
1 |
1 |
0 |
7 |
|
3 |
0 |
0 |
0 |
8 |
|
3 |
1 |
0 |
0 |
9 |
|
3 |
0 |
1 |
0 |
10 |
|
3 |
1 |
1 |
0 |
11 |
|
3 |
0 |
0 |
1 |
12 |
|
3 |
1 |
0 |
1 |
13 |
|
3 |
0 |
1 |
1 |
14 |
|
3 |
1 |
1 |
1 |
15 |
|
4 |
0 |
0 |
0 |
Here are some Python programs about this encoding.
import math
def log2int(x):
return(math.frexp(x)[1] - 1)
def length(n):
return(log2int(n+1))
def index(n,m): ## this is what I write as (n)_m
a = (n+1)%(2**(m+1))
b = 2**m
if a < b:
return(0)
else:
return(1)
def convert_numeral_to_onesharp(x):
if x == 0:
return('#')
else:
return('1')
def s(n):
k = length(n)
s = [convert_numeral_to_onesharp(index(n,k-i-1)) for i in range(k)]
t = "".join(s)
return(t)
def s_inverse(w):
n = len(w)
a = (2**n - 1)
b = [(2** (n-i-1)) for i in range(n) if (w[i] == '1')]
c = sum(b)
d = c+a
return(d)
print(s(143))
print(s_inverse('##11#1'))
print(s(s_inverse('##11#1')))
index(14,2)
[index(14,i) for i in range(5)]
## this will print (14)_0, (14)_1, (14)_2, (14)_3, (14)_4
Important
We have the following formulas
For all \(n\),
In these formulas, we identify # and the number \(0\).
Example
Let \(n = 101\). Note that \(2^7 = 128 > 101\), and \(7\) is the smallest with this property. Therefore \(|n| = 7-1 = 6\).
\(rem(102,2) = 0\). And \(0 < 2^0\), so \((102)_0 = 0\).
\(rem(102,4) = 2\). And \(2 \geq 2^1\), so \((102)_1 = 1\).
\(rem(102,8) = 6\). And \(6 \geq 4\), so \((102)_2 = 1\).
\(rem(102,16) = 6\). And \(6 < 8\), so \((102)_3 = 0\).
\(rem(102,32) = 6\). And \(6 < 16\), so \((102)_4 = 0\).
\(rem(102,64) = 42\). And \(42 \geq 32\), so \((102)_5 = 1\).
So we see that \(s(101) = 1 0 0 1 1 0 \). Trading in \(0\) for \(\#\), we get 1##11#.
Important
If \(w\) is any 1#-word, and if \(v\) is a subword of \(w\), or even a word which is smaller in length than \(w\), then as numbers
This is important because it leads to the fact that various functions are primitive recursive.
The point of all of this coding#
What want to associate functions on words with functions on numbers, and vice-versa. Here is how we take a function from words to words and associate a function from numbers to numbers.
Given \(f: Words \to Words\), we associate \(g: N \to N\) by \(g = s^{-1}\circ f \circ s\). That is,
We go back similarly.
We are especially interested in this when \(f\) is \([\![p]\!]\) for some program \(p\), and when \(f:N\to N\) is primitive recursive.
So given a program \(p\), we define a partial function \(\varphi_p: N\to N\) by
In our next section, we’ll see that the functions \(\varphi_p\), as \(p\) ranges over \(N\), are exactly the \(\mu\)-computable functions. Our definition takes them to be the coded versions of the 1#-computable functions.