TCS: Advanced Computability

Advanced Computability

Programs That Know Their Own Descriptions

A program description is finite data. Given a string $s$, an algorithm can generate the description of a program that ignores its input and prints $s$. Constructing this printer requires no execution of the program encoded by $s$

Self-reference becomes possible when a program combines stored data with a procedure that turns that data into code. A self-printing program, or quine, reconstructs its full description from these two parts

Kleene’s recursion theorem generalizes this idea: a program can use its own description as an argument to an arbitrary computation

A Compiler-Based Proof

Let $\varphi_e$ denote the partial function computed by program $e$. A total computable specialization function $s(e,a)$ produces a program that fixes the first argument of a two-argument program

$$\varphi_{s(e,a)}(w)\simeq\varphi_e(a,w)$$

Construct a two-argument program $P$ whose behavior is

$$P(z,w)\simeq t(s(z,z),w)$$

Let $p$ be the code of $P$, and define $r=s(p,p)$. Then

$$\varphi_r(w) \simeq\varphi_p(p,w) \simeq t(s(p,p),w) =t(r,w)$$

Thus the program with code $r$ has the required behavior. The specialization operation generates code syntactically, so there is no circular request to finish executing a program before constructing it

Choosing $t(e,w)=e$ gives a self-printing program immediately

Applications of the Recursion Theorem

An Undecidability Proof

Suppose $H$ decides whether a program accepts an input. By the recursion theorem, construct $D$ that obtains its own code, asks $H$ whether $D$ accepts the current input, and returns the opposite answer

$$D(w)=1-H(\langle D\rangle,w)$$

Either answer contradicts the specification of $H$. The recursion theorem packages the self-reference that otherwise appears as an explicit diagonal input

Minimal Programs

Fix a machine encoding. A program $M$ is minimal if no shorter program computes the same partial function

Assume an enumerator lists exactly the minimal programs. Construct $C$ that knows the length of its own description, waits for an enumerated program $D$ longer than itself, and then simulates $D$ on the current input

There are infinitely many partial computable functions, hence minimal descriptions of unbounded length. The waiting stage therefore finishes. But $C$ computes exactly the same partial function as the longer program $D$, contradicting the minimality of $D$

The same reasoning rules out every infinite recognizable subset of minimal programs

Rogers’ Fixed-Point Theorem

For every total computable transformation $f$ of program descriptions, there is a program $R$ such that

$$\varphi_{\langle R\rangle} \simeq\varphi_{f(\langle R\rangle)}$$

To obtain $R$, use the recursion theorem with a computation that transforms its own code by $f$ and simulates the resulting program. The fixed point is behavioral: the two descriptions need not be identical strings

Syntax, Semantics and Proof

A first-order language specifies variables, logical connectives, quantifiers, and symbols for constants, functions and relations. A structure assigns those nonlogical symbols meanings over a nonempty domain

For example, a sentence about addition can be interpreted in the natural numbers or in another structure. A sentence can be true in one structure without being valid in every structure

A proof calculus is sound when derivability implies semantic consequence, and complete when semantic consequence implies derivability

Gödel’s Completeness Theorem

For classical first-order logic,

$$T\vdash\varphi\quad\Longleftrightarrow\quad T\models\varphi$$

This completeness concerns all structures satisfying the axioms. A separate question asks whether a fixed effective theory proves every sentence true in the intended structure $\mathbb N$

Formal proofs are finite strings. For an effectively axiomatized theory, proofs can be effectively enumerated; for a decidable axiom set, a candidate derivation can be checked directly. A computably enumerable axiom set can instead be handled by recording finite witnesses to the enumeration of each axiom used

Gödel’s First Incompleteness Theorem

Here consistent means that the theory does not prove a sentence and its negation. The computability argument below uses a theory strong enough to represent program execution and reason about finite computation traces

A Machine That Opposes Proofs

Using the recursion theorem, define a machine $D$ with access to its own description. It enumerates $T$-proofs and searches for either of two sentences about itself

1. If it finds a proof that $D$ halts, it enters an explicit infinite loop
2. If it finds a proof that $D$ never halts, it halts

Assume $T$ is consistent. If $T$ proved that $D$ never halts, no proof of the opposite sentence could appear. The search would eventually find the nonhalting proof and halt. That finite execution supplies a formal proof of halting, contradicting consistency

If $T$ proved that $D$ halts, the search would instead reach the explicit loop. A finite trace establishes that $D$ has entered a state from which it can never halt, giving a proof of nonhalting and the same contradiction

Therefore neither sentence is provable. Externally, $D$ runs forever because neither triggering proof exists. Its nonhalting statement is a true arithmetic sentence unprovable in $T$

Adding this sentence as an axiom gives another effective theory to which the construction can be applied again

Gödel’s Second Incompleteness Theorem

Write $\operatorname{Con}(T)$ for the usual arithmetic sentence asserting that no $T$-proof of a contradiction exists

The first argument used consistency to conclude that its self-referential machine never halts. When the reasoning and the usual provability conditions are formalized inside the theory, they connect its consistency statement to an unprovable sentence

If $T$ could prove its own consistency, it could complete that internal argument and prove the sentence already shown to be unprovable. The full theorem requires the standard arithmetization of proofs; finite proof checking alone is not its entire proof

The completeness and incompleteness theorems fit together: a sentence true in $\mathbb N$ but unprovable from $T$ must fail in some other model of $T$