Minimal programs

DefinitionDescription length of a code#✓fully proved

For a code \(c\) of a partial recursive function, the description length of \(c\) is the number of binary digits of the encoding of \(c\) as a natural number, that is, the least \(k\) such that this encoding is less than \(2^k\) (so it is \(0\) when the encoding is \(0\)).

def descLength (c : Code) : ℕ := Nat.size (encode c)

Used by 3

Used byEvery language of a code has a minimal code · Minimal codes · Minimal codes are not recognizable

DefinitionMinimal codes#✓fully proved

A code \(c\) of a partial recursive function is minimal when no code with a shorter description has the same domain: for every code \(d\) whose description length is strictly less than that of \(c\), the domain of \(d\) (the set of inputs on which its evaluation is defined) differs from the domain of \(c\). The set of minimal codes is denoted \(\mathrm{MIN}\).

def MinimalCode (c : Code) : Prop :=
  ∀ d : Code, descLength d < descLength c → d.eval.Dom ≠ c.eval.Dom

Uses 1 · Used by 3

Statement usesDescription length of a code

Used byEvery language of a code has a minimal code · Minimal codes are unbounded · Minimal codes are not recognizable

TheoremCodes with singleton domain#✓fully proved

For every natural number \(n\) there is a code \(c\) of a partial recursive function whose evaluation is defined exactly at \(n\), that is, the domain of the partial function computed by \(c\) is \(\{n\}\).

theorem exists_code_dom_singleton (n : ℕ) : ∃ c : Code, c.eval.Dom = {n}

Used by 1

Used byMinimal codes are unbounded

TheoremEvery language of a code has a minimal code#✓fully proved

For every code \(c\) of a partial recursive function there is a minimal code \(D\) whose domain equals the domain of \(c\), where the domain of a code is the set of inputs on which its evaluation is defined.

theorem exists_minimalCode_dom (c : Code) :
    ∃ D : Code, MinimalCode D ∧ D.eval.Dom = c.eval.Dom

Uses 2 · Used by 1

Statement usesMinimal codes

Proof usesDescription length of a code

Used byMinimal codes are unbounded

TheoremMinimal codes are unbounded#✓fully proved

For every natural number \(N\) there is a minimal code \(D\) of a partial recursive function whose encoding as a natural number is greater than \(N\).

theorem exists_minimalCode_gt (N : ℕ) : ∃ D : Code, MinimalCode D ∧ N < encode D

Uses 3 · Used by 1

Statement usesMinimal codes

Proof usesCodes with singleton domain · Every language of a code has a minimal code

Used byMinimal codes are not recognizable

TheoremMinimal codes are not recognizable#✓fully proved

The set \(\mathrm{MIN}\) of minimal codes of partial recursive functions is not recognizable by a multi-stack Turing machine: there is no finite multi-stack machine that, for every code \(c\), halts on the binary encoding of the natural-number encoding of \(c\) exactly when \(c\) is minimal.

theorem not_tm2Recognizable_minimalCode : ¬TM2Recognizable MinimalCode

Sources

• M. Sipser, Introduction to the Theory of Computation, 3rd ed., Theorem 6.7.

Uses 5

Statement usesMinimal codes · Recognizability by multi-stack machines

Proof usesDescription length of a code · Minimal codes are unbounded · Multi-stack recognizable predicates are exactly the r.e. predicates

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.