Gödel numbering for sequences

From Wikipedia, the free encyclopedia

Any function can be regarded as a Gödel numbering for sequences, that fulfills the following specification:

it should enable us to inject (embed) the set of sequences of natural numbers to the set of natural numbers;
in many applications, we may expect it also to be effective in some sense (e.g. being a total recursive function).

It is usually used to build sequential “data types” in the realm of arithmetic-based formalizations of some foundamental notions of mathematics. It is a specific case of the more general idea of Gödel numbering.

E.g. recursive function theory can be regarded as a formalization of notion “algorithm”, and if we regard it as a programming language, we can mimic arrays, lists by encoding a sequence of natural numbers in a single natural number — to achieve this, we can use various number theoretic ideas. Using fundamental theorem of arithmetic is a straightforward way, but there are also more ergonomic approaches, e.g. using pairing function combined with Chinese remainder theorem in a sophisticated way, see a detailed treatment in ^[1] ^[2].

[edit] Gödel numbering

Main article: Gödel number

It is a sweeping idea, it can be used to not only sequences, but also whole “architectures” of sophisticated “machines”. We can encode e.g. Markov algorithms, and also Turing machines in the realm of natural numbers, this can be used e.g. to prove that the expressing power of recursive function theory is no less than that of the former machine-like formalizations of algorithm. See details in ^[1].

[edit] Access of members

Here, we want to build sequences. Let us formalize what we want — by specification: We want a function $β$ satisfying

$\forall a_0,\dots, a_{n-1}\;\exists s\;\forall i < n \; \beta(s,i) = a_i$

[edit] Using a pairing function

Our specific solution will depend on a pairing function — there are several ways to implement the latter, let us select one. Now, we can abstract from the details of the “implementation” of the pairing function, we need only to know its “interface”: let $π$ , K, L denote the pairing function and its two projection functions, respectively, satisying specification

$K\left(\pi\left(x,y\right)\right) = x$

$L\left(\pi\left(x,y\right)\right) = y$

we shall not discuss and formalize the axiom for excluding alien objects here, it is now not so important.

[edit] Using the Chinese remainder theorem

[edit] Implementation of the β function

Using the Chinese remainder theorem, we can prove that implementing $β$ as

$\beta(s,i) = \mathrm{rem}\left(K\left(s\right),\left(i+1\right)\cdot L\left(s\right)+1\right)$

will work, according to the specification we expect $β$ to satisfy. We can use a more concise form by an abuse of notation (sort of pattern matching):

$\beta\left(\pi\left(x_0,m\right),i\right) = \mathrm{rem}\left(x_0, \left(i+1\right)\cdot m+1\right)$

Let us achive even more readability by more modularity and reuse ^[3]: defining $\forall i<n$ the sequence $m_i = (i+1)\cdot m+1$ , enables us to write

$\beta\left(\pi\left(x_0,m\right),i\right) = \mathrm{rem}\left(x_0, m_i\right)$

We shall use this $m i$ notation also in the proof.

[edit] Hand-tuned assumptions

For proving the correctness of the above definition of $β$ function, we shall use (and prove) several auxiliary theorems, lemmas . These have their own assumptions. Now we try to find out these assumptions, tuning their strength carefully: they should not be said in an either superfluously sharp, or unsatisfactorily weak form.

Let $a_0,\dots a_{n-1}$ be a sequence of natural numbers. Let m be chosen to satisfy

$\forall i \in \overline n \setminus \left\{0\right\} \left(i \mid m\right)$

$\forall i < n \left( a_i < m_i \right)$

The first assumption is meant as

$1 \mid m \land \dots \land n-1 \mid m$

It is needed to achive that the assumption of the Chinese remainder theorem (that of being pairwise coprime) can be met. In the literature, sometimes this requirement is replaced with a stronger one, e.g. constructively built with the factorial function ^[1], but the proof uses just that many strength as formulated here.

The second assumption does not concern the Chinese remainder theorem in any way. It will have importance in proving that the specification for $β$ is met eventually. In the literature, sometimes it is replaced by a more strong requirement, e.g. $\forall i < n \; (a_i < m)$ , see ^[1] ^[2], but the proof uses just that many strength as formulated previously.

[edit] Proof that (coprimality) assumption for Chinese remainder theorem is met

We shall prove that the (coprimality) assumption for Chinese remainder theorem is met.

As mentioned in section #Hand-tuned assumptions, we prescribed that

$\forall i \in \overline n \setminus \left\{0\right\} \left(i \mid m\right)$

thus we can use it.

What we want to prove is that we can produce a sequence of pairwise coprime numbers in a way that will turn out to correspond to the #Implementation of the β function in a sense.

In details:

$\forall i<n,j < n \; \left( i \neq j \rightarrow \mathrm{coprime}\left(m_i,m_j\right) \right)$

let us remember, $\forall i<n$ we defined $m_i = (i+1)\cdot m+1$ .

Let us use reductio ad absurdum!

Nagation of the original statement:

$\exists i<n,j < n \; \left( i \neq j \land \lnot \mathrm{coprime}\left(m_i,m_j\right) \right)$

[edit] First steps

We know what “coprime” relation means (in a lucky way, its negation can be formulated in a concise form), thus, let us substitute in the appropriate way:

$\exists i<n,j < n \; \left( i \neq j \land \exists p \in \mathrm{Prime} \; \left( p \mid m_i \land p \mid m_j \right) \right)$

Using a “more” prenex normal form (but note allowing a constraint-like notation in quantifiers):

$\exists i<n,j < n,p \in \mathrm{Prime} \; \left( i \neq j \land p \mid m_i \land p \mid m_j \right)$

Because of a theorem on divisibility, $p \mid m_i \land p \mid m_j$ allows us to say also

$p \mid m_i - m_j$

Substituting the definens of $m_\dots$ -sequence notation, we get $m_i - m_j = (i-j) \cdot m$ , thus (as equality axioms postulate identity to be a congruence relation ^[4]) we get

$p \mid (i-j) \cdot m$

Using that p is a prime element (note: not the irreducible element property is used!), we get

$p \mid i-j \lor p \mid m$

[edit] Resorting to the first hand-tuned assumption

Now this is the point in the proof where we must resort to our assumption

$\forall i \in \overline n \setminus \left\{0\right\} \left(i \mid m\right)$

let us remember, we have planned this assumption carefully to be as weak as possible, but strong enough to enable us to use it now.

The assumed negation of the original statement (let us remember, we use reductio ad absurdum) contains an appropriate existential statement using indices $i<n\land j<n \land i\neq j$ , this entails $i-j \in \overline n \setminus \left\{0\right\}$ , thus the mentioned assumption can be applied, so $i-j \mid m$ holds.

[edit] Using an (object) theorem of the propositional calculus as a lemma

We can prove by several means ^[5] known in propositional calculus, that

$\left(A \lor \left( A \rightarrow B\right)\right) \leftrightarrow B$

holds.

Because $i-j \mid m$ entails (by the transitivity property of the divisibility relation) that $p \mid i-j \rightarrow p \mid m$ , thus (as equality axioms postulate identiy to be a congruence relation ^[4])

$p \mid m$

can be proven.

[edit] Reaching the contradiction

The negation of original statement contained

$p \mid m_i$

and we have just proved

$p \mid m$

thus also

$p \mid m_i - \left(i+1\right)\cdot m$

should hold. But, after substituting the definiens for $m i$ , we shall see

$m_i - \left(i+1\right) = 1$

Thus, summarizing the above three statements, by transitivity of the equality, also

$p \mid 1$

should hold. But let us look up the quantification of p in the negation of the original statement: p is existentially quantified and restricted to primes $\exists p \in \mathrm{Prime}$

The above statement together with the above quantification of p establish the contradiction we wanted to reach.

[edit] End of reductio ad absurdum

By reaching contradiction with its negation, we have just proven the original statement:

$\forall i<n,j<n \; \left( i \neq j \rightarrow \mathrm{coprime}\left(m_i,m_j\right)\right)$

[edit] The system of simultaneous congruences

We build a system of simultaneous congruences

$x \equiv a_0 \pmod{m_0}$

$\vdots$

$x \equiv a_{n-1} \pmod{m_{n-1}}$

We can write it in a more concise way:

$\forall i < n \; \left(x \equiv a_i \pmod{m_i}\right)$

In the followings, many statements will be said, all beginning with $\forall i < n \; \left(\dots\right)$ . To achieve a more ergonomic treatment, from now on all statements will be regarded in the scope of an $\forall i < n \; \left(\dots\right)$ qantification. Thus: $\forall i < n ($ begins!

Let us chose a solution $x 0$ for the system of simultaneous congruences. At least one solution must exist, because $m_0,\dots m_{n-1}$ are pairwise comprime (that's what we have been proving so long in the previous sections!), thus we can refer to the Chinese remainder theorem's ensuring solution. Thus, from now on, we can regard $x 0$ satisfying

$x_0 \equiv a_i \pmod{m_i}$

it means (by definition of modular arithmetic) that

$\mathrm{rem}\left(x_0,m_i\right) = \mathrm{rem}\left(a_i,m_i\right)$

[edit] Resorting to the second hand-tuned assumption

Again, we must resort to the assumptions whose strength we specifically “tuned” for using in the proof. But now, it is the second assumption (which does not concern the Chinese remainder theorem in any way) that we need: “ $\forall i < n \; \left(a_i < m_i \right)$ ”. Let us remember: we are now in the scope of a “big” quantification for i, thus we don't repeat its quantification for each statement.

The second hand-tuned assumption $a i < m i$ will join in at this point, because it entails that

$\mathrm{rem}\left(a_i,m_i\right) = a_i$

Now by transitivity of equality we get

$\mathrm{rem}\left(x_0,m_i\right) = a_i$

[edit] QED

Our original goal was to prove that the definition

$\beta\left(\pi\left(x_0,m\right),i\right) = \mathrm{rem}\left(x_0,m_i\right)$

is good for achiving what we declared in the specification of $β$ : we want $\beta\left(\pi\left(x_0,m\right),i\right) = a_i$ to hold.

That's it, it can be seen now by transitivity of equality, looking at the above three equations.

Scope of i ends here.

[edit] Existence and uniqueness

We have just proven the correctness of the definition of $β$ : its specification requiring

$\forall a_0,\dots, a_{n-1}\;\exists s\;\forall i < n \; \beta(s,i) = a_i$

is met. Although proving this was the most important, if we want to establish an encoding scheme for sequences, but we have to fill in some gaps yet. These are related notions similar to existence and uniqueness (although on uniqueness, “at most one” should be meant here, and the conjunction of both is delayed as a final result).

[edit] Uniqueness of encoding, achieved by minimalization

Because let us remember, our ultimate question is: what number should stand for the encoding of sequence $\left\langle a_0,\dots,a_{n-1}\right\rangle$ ? The specification declares only a existential quantification, not yet a functional connection. We want a constructive and algorithmic way, even more, a (total) recursive function for the encoding.

[edit] Totality, because minimalization is restricted to special functions

This gap can be filled in in a straightforward way: we shall use minimalization, and the totality of the resulting function is ensured by everything we have proven till now (i.e. the correctness of the definition of $β$ by meeting its specification). In fact, the specification

$\forall a_0,\dots, a_{n-1}\;\exists s\;\forall i < n \; \beta(s,i) = a_i$

plays a role here of a more general notion (which is called special function in ^[1]). The importance of this notion is that it enables us to split off the (sub)class of (total) recursive functions from the (super)class of partial recursive functions. In brief, the specification says exacly: a function f ^[6] satisfying specification

$f\left(a_0,\dots, a_{n-1}, s\right) = 0 \leftrightarrow \forall i < n \; \left(\beta(s,i) = a_i\right)$

is a special function, i.e. for each fixed combination of all-but-last arguments, the function f has root in its last argument:

$\forall a_0,\dots,a_{n-1}\;\exists s\; \left(f\left(a_0,\dots,a_{n-1},s\right)=0\right)$

[edit] The Gödel numbering function g can be chosen to be total recursive

Thus, let us chose the minimal possible number that fits well in the specification of the $β$ function ^[2]:

$g : \mathbb N^n \to \mathbb N$

$\left\langle a_0,\dots,a_{n-1}\right\rangle \longmapsto \mu a . \left[ \forall i < n \; \left(\beta\left(a,i\right) = a_i\right)\right]$

and it can be proven (using the notions of the previous section ) that g is (total) recursive.

[edit] Access of length

If we use the above sceme for encoding sequences only in contexts where the length of the sequences is fixed, then no problem arises. In other words, we can use them in an analogous way as arrays are used in programming.

But sometimes we need dynamically stretching sequences, or we need to deal with sequences whose length cannot be typed in a static way. In other words, we may encode sequences in an analogous way as we use lists in programming.

An example for both case ^[1]: if we make the Gödel numbering of a Turing machine, then the matrix of the “program” can be made with sequences of fixed length (thus, without storing the length), because the number of the columns is fixed. But if we want to reason about configuration-like things (of Turing-machines), and specially, we want to encode the significant part of the tape of a running Turing machine, then we have to deal with dynamically stretching sequences.

Length can be stored stored simply as a surplus member^[2]:

$g : \mathbb N^* \to \mathbb N$

$\left\langle a_0,\dots,a_{n-1}, a_n\right\rangle \longmapsto \mu a . \left[ a_0 = n \land \forall i < n \; \left(\beta\left(a,i+1\right) = a_i\right)\right]$

The corresponding modification of the proof is straightforward, by adding a surplus

$x \equiv n \pmod{m_0}$

to the system of simultaneous congruences (provided that the surplus member index is chosen to be 0). Also the assumptions etc. have to be modificated accordingly.

[edit] Notes

^ ^a ^b ^c ^d ^e ^f Monk, J. Donald: Mathematical Logic. Springer-Verlag, New York • Heidelberg • Berlin, 1976.
^ ^a ^b ^c ^d Csirmaz, László and Hajnal, András: Matematikai logika. Eötvös Loránd University, Budapest, 1994. (online available, in Hungarian)
^ The notions of code reuse and modularity, an their importance is treated in details in John Hughes' article Why Functional Programming Matters
^ ^a ^b see also related notions, e.g. “equals for equals” (referential transparency), and another related notion Leibniz's law / identity of indiscernibles
^ truth table, algebraic steps, Venn diagram, or Veitch diagram / Karnaugh map etc.
^ E.g. defined by

$f : \mathbb N^{n+1} \to \mathbb N$

$f\left(a_0,\dots, a_{n-1}, s\right) = \begin{cases}0 & \mathrm{if}\;\forall i < n \; \left(\beta(s,i) = a_i\right) \\ 1 & \mathrm{if}\;\exists i < n \; \left( \beta(s,i) \neq a_i \right)\end{cases}$