HOME

TheInfoList



OR:

In
mathematics Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
, a Gödel numbering for sequences provides an effective way to represent each finite sequence of natural numbers as a single natural number. While a set theoretical
embedding In mathematics, an embedding (or imbedding) is one instance of some mathematical structure contained within another instance, such as a group (mathematics), group that is a subgroup. When some object X is said to be embedded in another object Y ...
is surely possible, the emphasis is on the effectiveness of the functions manipulating such representations of sequences: the operations on sequences (accessing individual members, concatenation) can be "implemented" using total recursive functions, and in fact by
primitive recursive function In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
s. It is usually used to build sequential “
data type In computer science and computer programming, a data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on these values, and/or a representation of these ...
s” in arithmetic-based formalizations of some fundamental notions of mathematics. It is a specific case of the more general idea of
Gödel numbering In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. Kurt Gödel developed the concept for the proof of his incom ...
. For example, recursive function theory can be regarded as a formalization of the notion of an
algorithm In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
, and can be regarded as a
programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
to mimic
list A list is a Set (mathematics), set of discrete items of information collected and set forth in some format for utility, entertainment, or other purposes. A list may be memorialized in any number of ways, including existing only in the mind of t ...
s by encoding a sequence of natural numbers in a single natural number. Monk 1976: 56–58 Csirmaz 1994: 99–100 (se
online


Gödel numbering

Besides using Gödel numbering to encode unique sequences of symbols into unique natural numbers (i.e. place numbers into
mutually exclusive In logic and probability theory, two events (or propositions) are mutually exclusive or disjoint if they cannot both occur at the same time. A clear example is the set of outcomes of a single coin toss, which can result in either heads or tails ...
or
one-to-one correspondence In mathematics, a bijection, bijective function, or one-to-one correspondence is a function between two sets such that each element of the second set (the codomain) is the image of exactly one element of the first set (the domain). Equivale ...
with the sequences), we can use it to encode whole “architectures” of sophisticated “machines”. For example, we can encode
Markov algorithm In theoretical computer science, a Markov algorithm is a string rewriting system that uses grammar-like rules to operate on strings of symbols. Markov algorithms have been shown to be Turing-complete, which means that they are suitable as a gen ...
s, Monk 1976: 72–74 or
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
s Monk 1976: 52–55 into natural numbers and thereby prove that the expressive power of recursive function theory is no less than that of the former machine-like formalizations of algorithms.


Accessing members

Any such representation of sequences should contain all the information as in the original sequence—most importantly, each individual member must be retrievable. However, the length does not have to match directly; even if we want to handle sequences of different length, we can store length data as a surplus member, or as the other member of an
ordered pair In mathematics, an ordered pair, denoted (''a'', ''b''), is a pair of objects in which their order is significant. The ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a''), unless ''a'' = ''b''. In contrast, the '' unord ...
by using a
pairing function In mathematics, a pairing function is a process to uniquely encode two natural numbers into a single natural number. Any pairing function can be used in set theory to prove that integers and rational numbers have the same cardinality as natural ...
. We expect that there is an effective way for this
information retrieval Information retrieval (IR) in computing and information science is the task of identifying and retrieving information system resources that are relevant to an Information needs, information need. The information need can be specified in the form ...
process in form of an appropriate total recursive function. We want to find a totally recursive function ''f'' with the property that for all ''n'' and for any ''n''-length sequence of natural numbers \langle a_0,\dots a_ \rangle, there exists an appropriate natural number ''a'', called the Gödel number of the sequence, such that for all ''i'' where 0\le i \le n-1, f(a,i) = a_i. There are effective functions which can retrieve each member of the original sequence from a Gödel number of the sequence. Moreover, we can define some of them in a constructive way, so we can go well beyond mere proofs of existence.


Gödel's β-function lemma

By an ingenious use of the
Chinese remainder theorem In mathematics, the Chinese remainder theorem states that if one knows the remainders of the Euclidean division of an integer ''n'' by several integers, then one can determine uniquely the remainder of the division of ''n'' by the product of thes ...
, we can constructively define such a recursive function \beta (using simple number-theoretical functions, all of which can be defined in a total recursive way) fulfilling the
specification A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specificati ...
s given above. Gödel defined the \beta function using the Chinese remainder theorem in his article written in 1931. This is a
primitive recursive function In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
. Thus, for all ''n'' and for any ''n''-length sequence of natural numbers \langle a_0,\dots a_ \rangle, there exists an appropriate natural number ''a'', called the Gödel number of the sequence such that \beta(a,i) = a_i. Monk 1976: 58 (= Thm 3.46)


Using a pairing function

Our specific solution will depend on a pairing function—there are several ways to implement the pairing function, so one method must be selected. Now, we can abstract from the details of the
implementation Implementation is the realization of an application, execution of a plan, idea, scientific modelling, model, design, specification, Standardization, standard, algorithm, policy, or the Management, administration or management of a process or Goal ...
of the pairing function. We need only to know its “ interface”: let \pi, ''K'', and ''L'' denote the pairing function and its two
projection Projection or projections may refer to: Physics * Projection (physics), the action/process of light, heat, or sound reflecting from a surface to another in a different direction * The display of images by a projector Optics, graphics, and carto ...
functions, respectively, satisfying
specification A specification often refers to a set of documented requirements to be satisfied by a material, design, product, or service. A specification is often a type of technical standard. There are different types of technical or engineering specificati ...
: :K\left(\pi\left(x,y\right)\right) = x :L\left(\pi\left(x,y\right)\right) = y


Remainder for natural numbers

We shall use another auxiliary function that will compute the remainder for natural numbers. Examples: * \mathrm(5, 3) = 2 * \mathrm(7, 2) = 1 It can be proven that this function can be implemented as a recursive function.


Using the Chinese remainder theorem


= Implementation of the β function

= Using the
Chinese remainder theorem In mathematics, the Chinese remainder theorem states that if one knows the remainders of the Euclidean division of an integer ''n'' by several integers, then one can determine uniquely the remainder of the division of ''n'' by the product of thes ...
, we can prove that implementing \beta as :\beta(s,i) = \mathrm\left(K\left(s\right),\left(i+1\right)\cdot L\left(s\right)+1\right) will work, according to the specification we expect \beta to satisfy. We can use a more concise form by an
abuse of notation In mathematics, abuse of notation occurs when an author uses a mathematical notation in a way that is not entirely formally correct, but which might help simplify the exposition or suggest the correct intuition (while possibly minimizing errors an ...
(constituting a sort of
pattern matching In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually must be exact: "either it will or will not be a ...
): :\beta\left(\pi\left(x_0,m\right),i\right) = \mathrm\left(x_0, \left(i+1\right)\cdot m+1\right) Let us achieve even more readability by more
modularity Modularity is the degree to which a system's components may be separated and recombined, often with the benefit of flexibility and variety in use. The concept of modularity is used primarily to reduce complexity by breaking a system into varying ...
and
reuse Reuse is the action or practice of using an item, whether for its original purpose (conventional reuse) or to fulfill a different function (creative reuse or repurposing). It should be distinguished from recycling, which is the breaking down of ...
(as these notions are used in computer science Hughes 1989 (se
online
)
): by defining \forall i the sequence m_i = (i+1)\cdot m+1, we can write :\beta\left(\pi\left(x_0,m\right),i\right) = \mathrm\left(x_0, m_i\right). We shall use this m_i notation in the proof.


= Hand-tuned assumptions

= For proving the correctness of the above definition of the \beta function, we shall use several lemmas. These have their own assumptions. Now we try to find out these assumptions, calibrating and tuning their strength carefully: they should not be said in an either superfluously sharp, or unsatisfactorily weak form. Let a_0,\dots a_ be a sequence of natural numbers. Let ''m'' be chosen to satisfy :\forall i \in \overline n \setminus \left\ \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 meet an assumption of the Chinese remainder theorem (that of being pairwise
coprime In number theory, two integers and are coprime, relatively prime or mutually prime if the only positive integer that is a divisor of both of them is 1. Consequently, any prime number that divides does not divide , and vice versa. This is equiv ...
). In the literature, sometimes this requirement is replaced with a stronger one, e.g. constructively built with the
factorial In mathematics, the factorial of a non-negative denoted is the Product (mathematics), product of all positive integers less than or equal The factorial also equals the product of n with the next smaller factorial: \begin n! &= n \times ...
function, but the stronger premise is not required for this proof. The second assumption does not concern the Chinese remainder theorem in any way. It will have importance in proving that the specification for \beta is met eventually. It ensures that an \tilde x solution of the simultaneous congruence system :x \equiv a_i \pmod for each ''i'' where 0\le i \le n-1 also satisfies :a_i = \mathrm(\tilde x, m_i). Csirmaz 1994: 100 (se
online
Burris 1998: Supplementary Text
Arithmetic I
Lemma 4
A stronger assumption for ''m'' requiring \forall i < n \; (a_i < m) automatically satisfies the second assumption (if we define the notation m_i as above).


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

In the section Hand-tuned assumptions, we required that :\forall i \in \overline n \setminus \left\ \left(i \mid m\right). What we want to prove is that we can produce a sequence of pairwise
coprime In number theory, two integers and are coprime, relatively prime or mutually prime if the only positive integer that is a divisor of both of them is 1. Consequently, any prime number that divides does not divide , and vice versa. This is equiv ...
numbers in a way that will turn out to correspond to the Implementation of the β function. In detail: :\forall i remembering that \forall i we defined m_i = (i+1)\cdot m+1. The proof is by contradiction; assume the negation of the original statement: :\exists i


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 Using a “more” prenex normal form (but note allowing a constraint-like notation in quantifiers): :\exists i Because of a theorem on
divisibility In mathematics, a divisor of an integer n, also called a factor of n, is an integer m that may be multiplied by some integer to produce n. In this case, one also says that n is a ''Multiple (mathematics), multiple'' of m. An integer n is divis ...
, p \mid m_i \land p \mid m_j allows us to also say :p \mid m_i - m_j. Substituting the
definition A definition is a statement of the meaning of a term (a word, phrase, or other set of symbols). Definitions can be classified into two large categories: intensional definitions (which try to give the sense of a term), and extensional definitio ...
s of m_k-sequence notation, we get m_i - m_j = (i-j) \cdot m, thus (as equality axioms postulate identity to be a
congruence relation In abstract algebra, a congruence relation (or simply congruence) is an equivalence relation on an algebraic structure (such as a group (mathematics), group, ring (mathematics), ring, or vector space) that is compatible with the structure in the ...
see also related notions, e.g. “equals for equals” (
referential transparency In analytic philosophy and computer science, referential transparency and referential opacity are properties of linguistic constructions, and by extension of languages. A linguistic construction is called ''referentially transparent'' when for an ...
), and another related notion Leibniz's law /
identity of indiscernibles The identity of indiscernibles is an ontological principle that states that there cannot be separate objects or entities that have all their properties in common. That is, entities ''x'' and ''y'' are identical if every predicate possessed by ...
) we get : p \mid (i-j) \cdot m. Since ''p'' is a
prime element In mathematics, specifically in abstract algebra, a prime element of a commutative ring is an object satisfying certain properties similar to the prime numbers in the integers and to irreducible polynomials. Care should be taken to distinguish ...
(note that the
irreducible element In algebra, an irreducible element of an integral domain is a non-zero element that is not invertible (that is, is not a unit), and is not the product of two non-invertible elements. The irreducible elements are the terminal elements of a factor ...
property is used), we get :p \mid i-j \lor p \mid m.


Resorting to the first hand-tuned assumption

Now we must resort to our assumption :\forall i \in \overline n \setminus \left\ \left(i \mid m\right). The assumption was chosen carefully to be as weak as possible, but strong enough to enable us to use it now. The assumed negation of the original statement contains an appropriate existential statement using indices i; this entails i-j \in \overline n \setminus \left\, thus the mentioned assumption can be applied, so i-j \mid m holds.


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

We can prove by several means known in
propositional calculus The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...
that :\left(A \land \left( A \rightarrow B\right)\right) \rightarrow B holds. Since i-j \mid m, by the transitivity property of the
divisibility In mathematics, a divisor of an integer n, also called a factor of n, is an integer m that may be multiplied by some integer to produce n. In this case, one also says that n is a ''Multiple (mathematics), multiple'' of m. An integer n is divis ...
relation, p \mid i-j \rightarrow p \mid m. Thus (as equality axioms postulate identity to be a congruence relation ) :p \mid m can be proven.


Reaching the contradiction

The negation of original statement contained :p \mid m_i and we have just proved :p \mid m. Thus, :p \mid m_i - \left(i+1\right)\cdot m should also hold. But after substituting the
definition A definition is a statement of the meaning of a term (a word, phrase, or other set of symbols). Definitions can be classified into two large categories: intensional definitions (which try to give the sense of a term), and extensional definitio ...
of m_i, :m_i - \left(i+1\right)\cdot m = 1 Thus, summarizing the above three statements, by transitivity of the equality, :p \mid 1 should also hold. However, in the negation of the original statement ''p'' is existentially quantified and restricted to primes \exists p \in \mathrm. This establishes the contradiction we wanted to reach.


End of reductio ad absurdum

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


The system of simultaneous congruences

We build a system of simultaneous congruences :x \equiv a_0 \pmod ::\vdots :x \equiv a_ \pmod We can write it in a more concise way: :\forall i < n \; \left(x \equiv a_i \pmod\right) Many statements will be said below, all beginning with "\forall i < n \; \left(\dots\right)". To achieve a more ergonomic treatment, from now on all statements should be read as being in the scope of an \forall i < n \; \left(\dots\right) quantification. Thus, \forall i < n ( begins here. Let us chose a solution x_0 for the system of simultaneous congruences. At least one solution must exist, because m_0,\dots m_ are pairwise comprime as proven in the previous sections, so we can refer to the solution ensured by the Chinese remainder theorem. Thus, from now on we can regard x_0 as satisfying :x_0 \equiv a_i \pmod, which means (by definition of
modular arithmetic In mathematics, modular arithmetic is a system of arithmetic operations for integers, other than the usual ones from elementary arithmetic, where numbers "wrap around" when reaching a certain value, called the modulus. The modern approach to mo ...
) that :\mathrm\left(x_0,m_i\right) = \mathrm\left(a_i,m_i\right)


Resorting to the second hand-tuned assumption

Recall the second assumption, “\forall i < n \; \left(a_i < m_i \right)”, and remember that we are now in the scope of an implicit quantification for ''i'', so we don't repeat its quantification for each statement. The second assumption a_i < m_i implies that :\mathrm\left(a_i,m_i\right) = a_i. Now by transitivity of equality we get :\mathrm\left(x_0,m_i\right) = a_i.


QED

Our original goal was to prove that the definition :\beta\left(\pi\left(x_0,m\right),i\right) = \mathrm\left(x_0,m_i\right) is good for achieving what we declared in the specification of \beta: we want \beta\left(\pi\left(x_0,m\right),i\right) = a_i to hold. This can be seen now by transitivity of equality, looking at the above three equations. (The large scope of ''i'' ends here.)


Existence and uniqueness

We have just proven the correctness of the definition of \beta: its specification requiring :\forall a_0,\dots, a_\;\exists s\;\forall i < n \; \beta(s,i) = a_i is met. Although proving this was most important for establishing an encoding scheme for sequences, we have to fill in some gaps yet. These are related notions similar to
existence Existence is the state of having being or reality in contrast to nonexistence and nonbeing. Existence is often contrasted with essence: the essence of an entity is its essential features or qualities, which can be understood even if one does ...
and
uniqueness Uniqueness is a state or condition wherein someone or something is unlike anything else in comparison, or is remarkable, or unusual. When used in relation to humans, it is often in relation to a person's personality, or some specific characterist ...
(although on uniqueness, “at most one” should be meant here, and the conjunction of both is delayed as a final result).


Uniqueness of encoding, achieved by minimalization

Our ultimate question is: what number should stand for the encoding of sequence \left\langle a_0,\dots,a_\right\rangle? The specification declares only an existential quantification, not yet a functional connection. We want a constructive and algorithmic connection: a (total) recursive function that performs the encoding.


Totality, because minimalization is restricted to special functions

This gap can be filled 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 \beta by meeting its specification). In fact, the specification :\forall a_0,\dots, a_\;\exists s\;\forall i < n \; \beta(s,i) = a_i plays a role here of a more general notion (“special function” Monk 1976: 45 (= Def 3.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 that a function ''f'' E.g. defined by :f : \mathbb N^ \to \mathbb N :f\left(a_0,\dots, a_, s\right) = \begin0 & \mathrm\;\forall i < n \; \left(\beta(s,i) = a_i\right) \\ 1 & \mathrm\;\exists i < n \; \left( \beta(s,i) \neq a_i \right)\end satisfying the specification :f\left(a_0,\dots, a_, s\right) = 0 \leftrightarrow \forall i < n \; \left(\beta(s,i) = a_i\right) is a special function; that is, for each fixed combination of all-but-last arguments, the function ''f'' has
root In vascular plants, the roots are the plant organ, organs of a plant that are modified to provide anchorage for the plant and take in water and nutrients into the plant body, which allows plants to grow taller and faster. They are most often bel ...
in its last argument: :\forall a_0,\dots,a_\;\exists s\; \left(f\left(a_0,\dots,a_,s\right)=0\right)


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

Thus, let us choose the minimal possible number that fits well in the specification of the \beta function: :g : \mathbb N^n \to \mathbb N :\left\langle a_0,\dots,a_\right\rangle \longmapsto \mu a . \left \forall i < n \; \left(\beta\left(a,i\right) = a_i\right)\right/math>. It can be proven (using the notions of the previous section ) that ''g'' is (total) recursive.


Access of length

If we use the above scheme 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
type Type may refer to: Science and technology Computing * Typing, producing text via a keyboard, typewriter, etc. * Data type, collection of values used for computations. * File type * TYPE (DOS command), a command to display contents of a file. * ...
d in a static way. In other words, we may encode sequences in an analogous way to
list A list is a Set (mathematics), set of discrete items of information collected and set forth in some format for utility, entertainment, or other purposes. A list may be memorialized in any number of ways, including existing only in the mind of t ...
s in programming. To illustrate both cases: if we form the Gödel numbering of a Turing machine, then the each row in the matrix of the “program” can be represented with tuples, sequences of fixed length (thus, without storing the length), because the number of the columns is fixed. Monk 1976: 53 (= Def 3.20, Lem 3.21) But if we want to reason about configuration-like things (of Turing-machines), and specifically if we want to encode the significant part of the tape of a running Turing machine, then we have to represent sequences together with their length. We can mimic dynamically stretching sequences by representing sequence concatenation (or at least, augmenting a sequence with one more element) with a totally recursive function. Csirmaz 1994: 101 (=Thm 10.7, Conseq 10.8), se
online
/ref> Length can be stored simply as a surplus member: :g : \mathbb N^* \to \mathbb N :\left\langle a_0,\dots,a_, 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/math>. The corresponding modification of the proof is straightforward, by adding a surplus :x \equiv n \pmod to the system of simultaneous congruences (provided that the surplus member index is chosen to be 0). Also, the assumptions have to be modified accordingly.


Notes


References

* * Each chapter is downloadable verbatim o
author's page
* * * * Translation of Smullyan 1992.


External links

* {{DEFAULTSORT:Godel Numbering For Sequences Computability theory Articles containing proofs