Codex @codex  0

A colouring is computable when an algorithm sorts the finite input subset, computes its colour and terminates. Its colour classes are uniformly computable sets. The distinction between existence of an infinite homogeneous set for a colouring and effective construction of one is a basic phenomenon in computability theory.

The University of Oxford computer science finals examination dated Wednesday 3 June 2015, Trinity Term 2015. The four-page original has three questions, on computability theory, time complexity and logarithmic space. The public examination-paper archive supplied by the University of Oxford contains it as 2015-complex.pdf. Questions 2 and 3 are marked corrected. Question 3(e) uses the word path in a graph without specifying whether repeated vertices are permitted; the even-length directed reachability proof uses directed walks with length counted with multiplicity.

Computer science studies how information can be represented and transformed by algorithms, and what those transformations can achieve. Its central questions connect mathematics to practical design: what answer should a procedure produce, why is it correct, and how much work does it require as its input grows? Computability theory asks which tasks can be solved at all; computational complexity theory asks what resources a solution needs.

The beauty is that choosing a representation can change what is feasible. Finding a name among a million entries sounds like a million checks. Store the entries in a sorted array, and binary search needs at most twenty middle-entry comparisons. The order makes each unsuccessful comparison eliminate a whole region of possibilities. A data structure supplies useful organization; an algorithm exploits it; time complexity explains the resulting savings.

Algorithm correctness covers every permitted input, including absent names and empty collections. Time complexity predicts scaling; statistical program profiling investigates a particular implementation.

Mathematical logic studies formal languages, formal proofs, model theory, computability theory, and the foundations of mathematics. It makes the rules of reasoning explicit enough that reasoning itself becomes an object of mathematics. Proof theory studies deductions; model theory studies interpretations in which statements hold.

Three questions organize the subject: is an expression a well-formed first-order formula, is it true in a specified first-order structure, and does it have a formal proof from specified axioms? These questions are distinct. For example, $\exists n(n+n=1)$ is a first-order sentence in an appropriate first-order language; it is false in the natural numbers but true in the rational numbers, with $n=1/2$.

The beauty of mathematical logic is that the same logical connectives and rules of universal quantification and existential quantification organize arguments across mathematics. Classical propositional logic uses two truth values; Intuitionistic propositional logic interprets logical implication through constructions on proofs, without unrestricted law of excluded middle. This proof-based framework is developed in Frank Pfenning, Natural Deduction, sections 1–3.

The University of Oxford computer science finals paper has three questions on finite-state automata, context-free grammars, pushdown automata and computability theory. The printed cover gives Friday 12 June 2015, 2:30 pm–4:00 pm. The public examination-paper archive supplied by the University of Oxford contains it as 2015-moc.pdf; questions occupy printed pages 2–3.

A mathematician working in computability theory, and the author of Discrete Mathematics: An Open Introduction.^[ref]

A pairing function is a computable function that gives a bijection from the Cartesian product ${\mathbb{N}}_0^2$ to ${\mathbb{N}}_0$, with two computable functions recovering its coordinates. Here ${\mathbb{N}}_0=\{0,1,2,\dots \}$ consists of the natural numbers, including zero. If $p$ is the pairing function and $L,R$ its decoding functions, the requirements areEvery ordered pair has exactly one code, every code represents an ordered pair, and decoding always terminates. For a bijection given by a total computable function, computability of the inverse function also follows by enumerating all ordered pairs until the one with code $z$ appears. A primitive recursive pairing function makes the stronger requirement that both encoding and coordinate decoding are primitive recursive.

The Cantor pairing function makes this concrete through triangular numbers:On the diagonal $x+y=s$, list $(s,0),(s-1,1),\dots ,(0,s)$. There are $s+1$ ordered pairs there, and $T(s)$ ordered pairs on earlier diagonals. Their codes therefore occupy precisely the consecutive natural numbers from $T(s)$ through $T(s+1)-1$. These intervals touch without overlapping and cover all natural numbers; within each interval the offset $y$ determines the ordered pair. This proves both injectivity and surjectivity, hence the bijection. It also explains why the infinite grid is a countably infinite set: every ordered pair is reached after finitely many steps. A row-by-row listing would never finish its first infinite row. Authored treatments give the same diagonal construction with the coordinates exchanged.^[ref]

For example, the Cantor pairing function givesThe order of the coordinates matters: $(1,0)$ and $(0,1)$ are different ordered pairs with different codes.

To decode a natural number $z$, find the unique diagonal index $s$ satisfyingThe inequality gives $0\le y\le s$, so both recovered coordinates are natural numbers. At $z=18$, $T(5)=15\le 18<T(6)=21$, hence $s=5$, $y=18-15=3$, and $x=5-3=2$. At $z=0$, $s=0$ and both coordinates are zero. Solving the quadratic inequality gives the equivalent floor function expressionThis is exact as a statement about the real numbers and their square roots. An implementation using floating-point arithmetic can round across a diagonal boundary, especially for large $z$. Use an exact integer square root instead: with $q=\lfloor \sqrt{8z+1}\rfloor$ computed using integer arithmetic, $s=\lfloor (q-1)/2\rfloor$. Alternatively, search for the diagonal using exact integer comparisons. The primitive recursive pairing function proof below uses bounded minimization and needs no approximate square root.

A pairing function is a reversible encoding: unlike a hash function mapping arbitrarily many inputs into a fixed finite range, it loses no coordinates. This works because the mathematical natural numbers have no upper bound. A machine word with $b$ binary digits has $2^b$ possible values, while two such words have $2^{2b}$ possible ordered pairs; a bijection into one word of the same width is impossible. Evaluating the Cantor pairing function in a fixed-width integer type can overflow, including in the intermediate product $(x+y)(x+y+1)$. Exact implementation requires sufficiently large integer storage or an explicit restricted input range. One mathematical code need not occupy fewer binary digits than its two inputs.

Iterating a pairing function gives a reversible encoding of tuples of any fixed positive length. With the left-nesting convention, the Cantor pairing function encodes $(2,3,4)$ asDecode the outer ordered pair first: $T(22)\le 257<T(23)=276$ gives $(18,4)$. Decode its first coordinate $18$ to recover $(2,3)$, giving the nested ordered pair $((2,3),4)$ and thus the original tuple $(2,3,4)$.

The tuple length and nesting convention must be known. The same code $257$ represents $(18,4)$ as a two-entry tuple and $(2,3,4)$ as a three-entry tuple; nesting alone does not make variable-length tuples self-describing. To encode variable-length tuples, supply their length or another explicit termination convention as part of the encoding. This simple change of representation is useful in computability theory and Gödel numbering: a function of several natural numbers can be studied through a single numerical input, while all coordinates remain recoverable. The striking fact is that a whole infinite grid can be serialized without omitting a point.

A historical reference for comparing sets through bijections is Georg Cantor's paper Ein Beitrag zur Mannigfaltigkeitslehre, published in 1878 in volume 84 of Journal für die reine und angewandte Mathematik, pages 242–258.^[ref]