def Decidability.IsCountable {α : Type u_1} (s : Set α) : Prop

A set s : Set α is countable if it is finite or has the same size as ℕ.

theorem Decidability.set_not_countable_of_countable_infinite {α : Type u_1} [Countable α] [Infinite α] : ¬Countable (Set α)

For any countably infinite type α, the power set Set α is uncountable. This is a form of Cantor's theorem and underlies the proof that some language is undecidable.

theorem Decidability.languages_uncountable (Alphabet : Type u_1) [Nonempty Alphabet] [Countable Alphabet] : ¬Countable (Language Alphabet)

Corollary (Sipser Lecture 8). The set ℒ of all languages over a nonempty countable alphabet is uncountable. Combined with the countability of Turing machines, this shows that some language is not Turing-decidable.

structure TuringMachine.TMDesc (Γ : Type) : Type 1

A TMDesc packages a Turing machine together with its (decidable) state type and an input string. This corresponds to the encoded pair ⟨M, w⟩ used throughout Sipser's undecidability arguments — for example, the input to a putative decider for A_TM.

• Q : Type
• decEq : DecidableEq self.Q
• tm : TM self.Q Γ
• input : List Γ

def TuringMachine.TMDesc.accepts {Γ : Type} (d : TMDesc Γ) : Prop

d.accepts holds when the underlying TM d.tm accepts the input d.input.

def TuringMachine.TMDesc.halts {Γ : Type} (d : TMDesc Γ) : Prop

d.halts holds when the underlying TM d.tm halts (accepts or rejects) on the input d.input.

theorem TuringMachine.TM.run_add {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (m n : ℕ) : M.run c (m + n) = M.run (M.run c m) n

Additivity of run: running M for m + n steps equals running it for m steps and then for an additional n steps.

structure TuringMachine.TMEncoding (Γ : Type) : Type 1

A TMEncoding over alphabet Γ is a bundle of all the encoding/universal-machine machinery used informally in Sipser. It provides:

• an injective encoding encode : TMDesc Γ → List Γ with a decoder,
• a self-reference principle (used for the Recursion Theorem / diagonal argument),
• a universal TM U that simulates encoded TMs whenever they halt,
• sequential composition of a decider with another TM, and
• transducer composition with computable functions, as used in mapping reductions.

• encode : TMDesc Γ → List Γ
• decode : List Γ → Option (TMDesc Γ)
• encode_injective : Function.Injective self.encode
• decode_encode (d : TMDesc Γ) : self.decode (self.encode d) = some d
• selfRef {Q₀ : Type} [DecidableEq Q₀] (M : TM Q₀ Γ) : ∃ (d : TMDesc Γ), d.accepts ↔ M.accepts (self.encode d)
• universalSim : ∃ (QU : Type) (x : DecidableEq QU) (U : TM QU Γ), (∀ (d : TMDesc Γ), d.halts → U.halts (self.encode d)) ∧ (∀ (d : TMDesc Γ), d.halts → (U.accepts (self.encode d) ↔ d.accepts)) ∧ ∀ (s : List Γ), U.accepts s → ∃ (d : TMDesc Γ), self.encode d = s ∧ d.accepts
• sequentialComposition {QR QU : Type} [DecidableEq QR] [DecidableEq QU] (R : TM QR Γ) (U : TM QU Γ) : R.isDecider → (∀ (w : List Γ), R.accepts w → U.halts w) → ∃ (QS : Type) (x : DecidableEq QS) (S : TM QS Γ), S.isDecider ∧ ∀ (w : List Γ), S.accepts w ↔ R.accepts w ∧ U.accepts w
• transducerComposition (f : List Γ → List Γ) : IsComputableFunction f → ∀ {QR : Type} [inst : DecidableEq QR] (R : TM QR Γ), R.isDecider → ∃ (QS : Type) (x : DecidableEq QS) (S : TM QS Γ), S.isDecider ∧ ∀ (w : List Γ), S.accepts w ↔ R.accepts (f w)

theorem TuringMachine.parallel_simulation {Γ Q₁ Q₂ : Type} [DecidableEq Q₁] [DecidableEq Q₂] (M₁ : TM Q₁ Γ) (M₂ : TM Q₂ Γ) (hcov : ∀ (w : List Γ), M₁.accepts w ∨ M₂.accepts w) : ∃ (Q : Type) (x : DecidableEq Q) (T : TM Q Γ), T.isDecider ∧ ∀ (w : List Γ), T.accepts w ↔ M₁.accepts w

Dovetailing simulation. Given TMs M₁, M₂ such that for every input w at least one of them accepts, one can construct a decider T that simulates both in parallel and accepts iff M₁ accepts. This is the technical content behind Sipser's Lecture 8 theorem "If A and Aᶜ are T-recognizable then A is decidable."

theorem TuringMachine.recognizable_complement_decidable {Γ : Type} {A : Set (List Γ)} (hA : IsTuringRecognizable A) (hAc : IsTuringRecognizable Aᶜ) : IsTuringDecidable A

Theorem (Sipser Lecture 8). If both A and its complement Aᶜ are Turing-recognizable then A is Turing-decidable. The proof runs the two recognizers in parallel and accepts/rejects according to whichever halts first.

def TuringMachine.A_TM {Γ : Type} (enc : TMEncoding Γ) : Set (List Γ)

The acceptance problem for Turing machines: A_TM = {⟨M, w⟩ | M accepts w}. The classical Sipser theorem says this language is undecidable but Turing-recognizable.

def TuringMachine.HALT_TM {Γ : Type} (enc : TMEncoding Γ) : Set (List Γ)

The halting problem: HALT_TM = {⟨M, w⟩ | M halts on w}, also undecidable.

theorem TuringMachine.TM.halts_of_accepts {Γ Q : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) (h : M.accepts w) : M.halts w

If a TM accepts an input then it halts on that input (accepting is a form of halting).

theorem TuringMachine.A_TM_subset_HALT_TM {Γ : Type} (enc : TMEncoding Γ) : A_TM enc ⊆ HALT_TM enc

Acceptance implies halting at the level of languages: A_TM ⊆ HALT_TM.

def TuringMachine.TM.flip {Q : Type} (Γ : Type) [DecidableEq Q] (H : TM Q Γ) : TM Q Γ

The "flipped" TM H.flip swaps the accept and reject states of H. If H is a decider then H.flip decides the complement of L(H). This is the standard construction used in the diagonal proof that A_TM is undecidable.

theorem TuringMachine.TM.flip_step {Q Γ : Type} [DecidableEq Q] (H : TM Q Γ) (c : Config Q Γ) : (flip Γ H).step c = H.step c

Swapping accept/reject states does not change the one-step transition function of the TM on non-halting configurations, and on halting configurations both sides idle, so the step functions agree pointwise.

theorem TuringMachine.TM.flip_run {Q Γ : Type} [DecidableEq Q] (H : TM Q Γ) (c : Config Q Γ) (n : ℕ) : (flip Γ H).run c n = H.run c n

The n-step run is the same for H and H.flip, since their step functions agree pointwise.

theorem TuringMachine.TM.flip_accepts_iff {Q Γ : Type} [DecidableEq Q] (H : TM Q Γ) (hH : H.isDecider) (w : List Γ) : (flip Γ H).accepts w ↔ ¬H.accepts w

If H is a decider then its flip H.flip accepts w iff H does not accept w. This is the crucial property that allows the flip to decide the complement language.

theorem TuringMachine.A_TM_not_decidable {Γ : Type} (enc : TMEncoding Γ) : ¬IsTuringDecidable (A_TM enc)

Theorem (Sipser, undecidability of A_TM). The acceptance problem A_TM = {⟨M, w⟩ | M accepts w} is not Turing-decidable. The proof is the classical Turing diagonal argument: assuming a decider H exists, the flipped machine D = H.flip (which decides whether H rejects) leads to a contradiction via the self-reference principle provided by TMEncoding.

theorem TuringMachine.A_TM_decidable_of_HALT_TM_decidable {Γ : Type} (enc : TMEncoding Γ) (hHalt : IsTuringDecidable (HALT_TM enc)) : IsTuringDecidable (A_TM enc)

A decider for HALT_TM yields a decider for A_TM. This is the standard reduction A_TM ≤ HALT_TM: first use the HALT_TM-decider to check that M halts on w, then run the universal TM U (which is guaranteed to halt on inputs whose underlying TM halts) to determine whether M accepts. Together with the undecidability of A_TM this implies the undecidability of HALT_TM.

theorem TuringMachine.HALT_TM_not_decidable {Γ : Type} (enc : TMEncoding Γ) : ¬IsTuringDecidable (HALT_TM enc)

Theorem (Sipser). The halting problem HALT_TM = {⟨M, w⟩ | M halts on w} is undecidable, by reduction from A_TM.

@[implicit_reducible]

instance Decidability.instFintypeDirection : Fintype TuringMachine.Direction

The head movement directions L and R form a two-element Fintype.

def Decidability.IsTuringDecidableFinite {Γ : Type} (A : Set (List Γ)) : Prop

A language is "finitely Turing-decidable" if it is decided by some TM whose state set is Fin n for some n. Up to renaming of states this is no weaker than IsTuringDecidable, but restricting to Fin n makes the collection of such machines countable.

@[reducible, inline]

abbrev Decidability.TMDescType (Γ : Type) : Type

The raw data of a finite-state Turing machine over Γ: a state count n, a blank symbol, a transition function, and start/accept/reject states. This is the carrier used to enumerate TMs in a countable family.

instance Decidability.tmDescType_countable (Γ : Type) [Fintype Γ] [DecidableEq Γ] : Countable (TMDescType Γ)

For finite alphabets, the set of finite-state TM descriptions is countable.

noncomputable def Decidability.tmDescToLang (Γ : Type) [DecidableEq Γ] : TMDescType Γ → Set (List Γ)

Map a piece of raw TM data to its language. If qAccept = qReject (ill-formed data) the language is empty; otherwise it is the language of the corresponding TM.

theorem Decidability.TM.language_eq_of_same_data {Q Γ : Type} [DecidableEq Q] (M₁ M₂ : TuringMachine.TM Q Γ) (hblank : M₁.blank = M₂.blank) (hδ : M₁.δ = M₂.δ) (hq₀ : M₁.q₀ = M₂.q₀) (hqA : M₁.qAccept = M₂.qAccept) (hqR : M₁.qReject = M₂.qReject) : M₁.language = M₂.language

Two TMs that agree on blank, transition function, start, accept, and reject states accept the same language. The "extra" data in a TM record (e.g. inputAlpha) does not affect the language.

theorem Decidability.language_in_range_tmDescToLang {Γ : Type} [Fintype Γ] [DecidableEq Γ] {n : ℕ} (M : TuringMachine.TM (Fin n) Γ) : M.language ∈ Set.range (tmDescToLang Γ)

Every language of a TM with state set Fin n arises as tmDescToLang of some encoded description.

theorem Decidability.exists_undecidable_language (Γ : Type) [Fintype Γ] [DecidableEq Γ] [Nonempty Γ] : ∃ (L : Set (List Γ)), ¬IsTuringDecidableFinite L

Corollary (Sipser Lecture 8). Some language is not Turing-decidable. The argument is the cardinality argument: there are only countably many Turing machines but uncountably many languages, so some language cannot be decided.

theorem Decidability.exists_undecidable_language' {Γ : Type} (enc : TuringMachine.TMEncoding Γ) : ∃ (A : Set (List Γ)), ¬TuringMachine.IsTuringDecidable A

An explicit witness to "some language is undecidable": A_TM itself is undecidable.

theorem Decidability.some_language_not_decidable (Γ : Type) [Fintype Γ] [DecidableEq Γ] [Nonempty Γ] : ∃ (L : Set (List Γ)), ¬IsTuringDecidableFinite L

Restatement: there exists a language over Γ that is not Turing-decidable.

structure PostCorrespondence.Domino (α : Type) : Type

A domino in the Post Correspondence Problem is a pair of strings (top, bottom) over the alphabet α.

• top : List α
• bottom : List α

def PostCorrespondence.PCPInstance (α : Type) : Type

A PCP instance is a finite list of dominoes.

def PostCorrespondence.hasMatch {α : Type} (P : PCPInstance α) : Prop

A PCP instance P has a match if there is a nonempty sequence of indices i₁, …, iₖ such that concatenating the tops in order produces the same string as concatenating the bottoms in order. The PCP language is precisely the set of encoded instances with a match.

structure PostCorrespondence.PCPEncoding (Γ : Type) : Type

An injective encoding/decoding scheme that turns PCP instances over Γ into strings over Γ.

• encode : PCPInstance Γ → List Γ
• decode : List Γ → Option (PCPInstance Γ)
• encode_injective : Function.Injective self.encode
• decode_encode (P : PCPInstance Γ) : self.decode (self.encode P) = some P

def PostCorrespondence.PCP {Γ : Type} (enc : PCPEncoding Γ) : Set (List Γ)

The Post Correspondence Problem language PCP = {⟨P⟩ | P has a match}. By Sipser's Lecture 10 theorem, this language is undecidable.

structure LBADecidability.LBADesc (Γ : Type) : Type 1

An LBADesc packages a linearly bounded automaton (a finite-state TM constrained to its input region) with an input string. Following Sipser, LBA = ⟨B, w⟩ is the typical input to A_LBA.

• Q : Type
• decEq : DecidableEq self.Q
• finQ : Fintype self.Q
• lba : TuringMachine.LBA self.Q Γ
• input : List Γ

def LBADecidability.LBADesc.accepts {Γ : Type} (d : LBADesc Γ) : Prop

d.accepts holds when the LBA d.lba accepts the input string d.input.

structure LBADecidability.LBAEncoding (Γ : Type) : Type 1

Injective encoding/decoding of LBADescs into strings, used to formulate the language A_LBA.

• encode : LBADesc Γ → List Γ
• decode : List Γ → Option (LBADesc Γ)
• encode_injective : Function.Injective self.encode
• decode_encode (d : LBADesc Γ) : self.decode (self.encode d) = some d

def LBADecidability.A_LBA {Γ : Type} (enc : LBAEncoding Γ) : Set (List Γ)

The acceptance language for LBAs: A_LBA = {⟨B, w⟩ | LBA B accepts w}. Sipser's Lecture 10 theorem shows this language is decidable.

def LBADecidability.BoundedConfig (Q Γ : Type) (m : ℕ) : Type

A bounded configuration records only the data of an LBA configuration that can vary in the bounded simulation: state, head position in Fin m, and tape contents on the first m cells. The total number of such configurations is finite.

@[implicit_reducible]

noncomputable instance LBADecidability.instFintypeBoundedConfig (Q Γ : Type) (m : ℕ) [Fintype Q] [DecidableEq Γ] [Fintype Γ] : Fintype (BoundedConfig Q Γ m)

The set of bounded configurations of an LBA with state set Q, tape alphabet Γ, and input bound m is finite when Q and Γ are. This finiteness is the basis of the decidability of A_LBA: an LBA either accepts within |Q| · m · |Γ|^m steps or loops.

def LBADecidability.extractBoundedConfig {Q Γ : Type} (m : ℕ) (c : TuringMachine.Config Q Γ) (h0 : 0 ≤ c.headPos) (h1 : c.headPos < ↑m) : BoundedConfig Q Γ m

Extract the bounded-configuration view of a TM configuration whose head lies in [0, m).

theorem LBADecidability.lba_tape_outside_unchanged {Q Γ : Type} [DecidableEq Q] (B : TuringMachine.LBA Q Γ) (w : List Γ) (n : ℕ) (i : ℤ) (hi : i < 0 ∨ ↑(max 1 w.length) ≤ i) : (B.toTM.runOnInput w n).tape i = (B.toTM.initConfig w).tape i

An LBA never modifies tape cells outside the input region [0, max 1 |w|): for any position i outside this region, the tape symbol after n steps equals the initial symbol.

theorem LBADecidability.lba_configs_eq_of_bounded_eq {Q Γ : Type} [DecidableEq Q] (B : TuringMachine.LBA Q Γ) (w : List Γ) (n₁ n₂ : ℕ) (h : extractBoundedConfig (max 1 w.length) (B.toTM.runOnInput w n₁) ⋯ ⋯ = extractBoundedConfig (max 1 w.length) (B.toTM.runOnInput w n₂) ⋯ ⋯) : B.toTM.runOnInput w n₁ = B.toTM.runOnInput w n₂

If two configurations of an LBA running on input w agree on their bounded views (state, head position, and tape contents in [0, max 1 |w|)) then they are equal as full configurations, since the tape outside that window is fixed. This is the key lemma underlying the pigeonhole argument that bounds LBA running time.

@[implicit_reducible]

noncomputable instance LBADecidability.lbaDesc_accepts_decidable {Γ : Type} (d : LBADesc Γ) : Decidable d.accepts

Acceptance of an LBA description is decidable (classically). Constructively this follows from the finiteness of LBA configurations, which bounds the search for an accepting run.

theorem LBADecidability.A_LBA_bounded_simulator {Γ : Type} [Fintype Γ] (enc : LBAEncoding Γ) : ∃ (QU : Type) (x : DecidableEq QU) (U : TuringMachine.TM QU Γ), U.isDecider ∧ (∀ (d : LBADesc Γ), U.accepts (enc.encode d) ↔ d.accepts) ∧ ∀ (s : List Γ), U.accepts s → ∃ (d : LBADesc Γ), enc.encode d = s ∧ d.accepts

There is a universal TM U that, when run on the encoding of an LBADesc d, simulates the LBA d.lba on input d.input and decides whether it accepts. U always halts because LBAs have only finitely many configurations on a fixed input, so non-acceptance can be detected by pigeonhole.

theorem LBADecidability.A_LBA_decidable {Γ : Type} [Fintype Γ] (enc : LBAEncoding Γ) : TuringMachine.IsTuringDecidable (A_LBA enc)

Theorem (Sipser Lecture 10). A_LBA = {⟨B, w⟩ | LBA B accepts w} is Turing-decidable. The decider simulates B on w for enough steps that, by pigeonhole on bounded configurations, either acceptance has occurred or the LBA is in a loop.

structure ELBA.LBAMachineDesc (Γ : Type) : Type 1

An LBAMachineDesc is an LBA on its own (no input attached), used for the emptiness problem E_LBA.

• Q : Type
• decEq : DecidableEq self.Q
• finQ : Fintype self.Q
• lba : TuringMachine.LBA self.Q Γ

def ELBA.LBAMachineDesc.language {Γ : Type} (d : LBAMachineDesc Γ) : Set (List Γ)

The language accepted by an LBA description.

structure ELBA.LBAMachineEncoding (Γ : Type) : Type 1

Injective encoding/decoding of LBA machine descriptions, used to formulate E_LBA.

• encode : LBAMachineDesc Γ → List Γ
• decode : List Γ → Option (LBAMachineDesc Γ)
• encode_injective : Function.Injective self.encode
• decode_encode (d : LBAMachineDesc Γ) : self.decode (self.encode d) = some d

def ELBA.E_LBA {Γ : Type} (enc : LBAMachineEncoding Γ) : Set (List Γ)

The emptiness problem for LBAs: E_LBA = {⟨B⟩ | L(B) = ∅}. By Sipser's Lecture 10 theorem, this language is undecidable.

theorem compHistLBAConstruction {Γ : Type} (d : TuringMachine.TMDesc Γ) : ∃ (bd : ELBA.LBAMachineDesc Γ), bd.language = ∅ ↔ ¬d.accepts

Computation-history construction for E_LBA. Given a TM description d, one can build an LBA bd whose language is empty iff d does not accept. (The LBA recognizes valid accepting computation histories of d; emptiness corresponds to no accepting history existing, i.e. d does not accept.)

theorem compHistLBADefault {Γ : Type} : ∃ (bd : ELBA.LBAMachineDesc Γ), bd.language = ∅

A default LBA description whose language is empty, used for malformed inputs of the mapping reduction.

theorem compHistTransductionComputable {Γ : Type} (f : List Γ → List Γ) (tmEnc : TuringMachine.TMEncoding Γ) (lbaEnc : ELBA.LBAMachineEncoding Γ) (hValid : ∀ (d : TuringMachine.TMDesc Γ), ∃ (bd : ELBA.LBAMachineDesc Γ), f (tmEnc.encode d) = lbaEnc.encode bd ∧ (bd.language = ∅ ↔ ¬d.accepts)) (hInvalid : ∀ (w : List Γ), (∀ (d : TuringMachine.TMDesc Γ), tmEnc.encode d ≠ w) → ∃ (bd : ELBA.LBAMachineDesc Γ), f w = lbaEnc.encode bd ∧ bd.language = ∅) : TuringMachine.IsComputableFunction f

The transducer that maps a TM description to its computation-history LBA description is TM-computable. This is the computability side of the reduction A_TM ≤ₘ E_LBAᶜ.

theorem ELBA.compHistTransducer {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (lbaEnc : LBAMachineEncoding Γ) : ∃ (f : List Γ → List Γ), TuringMachine.IsComputableFunction f ∧ (∀ (d : TuringMachine.TMDesc Γ), ∃ (bd : LBAMachineDesc Γ), f (tmEnc.encode d) = lbaEnc.encode bd ∧ (bd.language = ∅ ↔ ¬d.accepts)) ∧ ∀ (w : List Γ), (∀ (d : TuringMachine.TMDesc Γ), tmEnc.encode d ≠ w) → ∃ (bd : LBAMachineDesc Γ), f w = lbaEnc.encode bd ∧ bd.language = ∅

Computation-history transducer for E_LBA. There exists a computable function f mapping TM encodings to LBA encodings such that on a valid TM input ⟨d⟩, f produces an LBA whose language is empty iff d does not accept, and on invalid inputs f produces an LBA with empty language. This is the engine of the reduction A_TM ≤ₘ (E_LBA)ᶜ.

theorem ELBA.A_TM_mapping_reduces_to_compl_E_LBA {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (lbaEnc : LBAMachineEncoding Γ) : TuringMachine.MappingReducible (TuringMachine.A_TM tmEnc) (E_LBA lbaEnc)ᶜ

Mapping reduction A_TM ≤ₘ (E_LBA)ᶜ. Using the computation-history construction, the acceptance problem for TMs many-one reduces to the non-emptiness problem for LBAs. Since A_TM is undecidable, so is (E_LBA)ᶜ, and hence so is E_LBA.

theorem ELBA.A_TM_decidable_of_E_LBA_decidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (lbaEnc : LBAMachineEncoding Γ) (hELBA : TuringMachine.IsTuringDecidable (E_LBA lbaEnc)) : TuringMachine.IsTuringDecidable (TuringMachine.A_TM tmEnc)

If E_LBA were decidable, so would A_TM be: combine a decider for E_LBA, flip it to decide the complement, and pre-compose with the computation-history transducer.

theorem ELBA.E_LBA_not_decidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (lbaEnc : LBAMachineEncoding Γ) : ¬TuringMachine.IsTuringDecidable (E_LBA lbaEnc)

Theorem (Sipser Lecture 10). The LBA emptiness problem E_LBA = {⟨B⟩ | L(B) = ∅} is undecidable.

theorem A_TM_recognizable {Γ : Type} (enc : TuringMachine.TMEncoding Γ) : TuringMachine.IsTuringRecognizable (TuringMachine.A_TM enc)

Theorem. A_TM is Turing-recognizable: the universal TM U provided by the encoding serves as a recognizer. On input ⟨M, w⟩, U simulates M on w and accepts iff M does.

theorem TuringMachine.A_TM_complement_not_recognizable {Γ : Type} (enc : TMEncoding Γ) : ¬IsTuringRecognizable (A_TM enc)ᶜ

Corollary (Sipser Lecture 8). The complement (A_TM)ᶜ is not Turing-recognizable. For if both A_TM and its complement were recognizable, then by the previous theorem A_TM would be decidable, contradicting the diagonal argument.

theorem A_TM_complement_not_TuringRecognizable {Γ : Type} (enc : TuringMachine.TMEncoding Γ) : ¬TuringMachine.IsTuringRecognizable (TuringMachine.A_TM enc)ᶜ

Restatement of the previous corollary in the root namespace: (A_TM)ᶜ is T-unrecognizable.

structure AllCFG.CFGEncoding (Γ : Type) : Type 1

An injective encoding/decoding scheme that turns context-free grammars over Γ into strings over Γ. Used to formulate ALL_CFG.

• encode : ContextFreeGrammar Γ → List Γ
• decode : List Γ → Option (ContextFreeGrammar Γ)
• encode_injective : Function.Injective self.encode
• decode_encode (g : ContextFreeGrammar Γ) : self.decode (self.encode g) = some g

theorem AllCFG.computationHistoryCFGExists {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (cfgEnc : CFGEncoding Γ) : ∃ (f : List Γ → List Γ), TuringMachine.IsComputableFunction f ∧ (∀ (d : TuringMachine.TMDesc Γ), ∃ (g : ContextFreeGrammar Γ), f (tmEnc.encode d) = cfgEnc.encode g ∧ (g.language = Set.univ ↔ ¬d.accepts)) ∧ ∀ (w : List Γ), (∀ (d : TuringMachine.TMDesc Γ), tmEnc.encode d ≠ w) → ∃ (g : ContextFreeGrammar Γ), f w = cfgEnc.encode g ∧ g.language = Set.univ

Computation-history reduction for ALL_CFG. There is a computable function f mapping TM encodings to CFG encodings such that, for any TM d, the CFG f(⟨d⟩) generates all strings iff d does not accept (so the strings not generated correspond to accepting computation histories of d), and on invalid inputs f outputs a universal CFG.

def AllCFG.ALL_CFG {Γ : Type} (enc : CFGEncoding Γ) : Set (List Γ)

The universality problem for CFGs: ALL_CFG = {⟨G⟩ | G is a CFG and L(G) = Σ*}. By Sipser's Lecture 10 theorem, this language is undecidable.

theorem AllCFG.computationHistoryCFGConstruction {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (cfgEnc : CFGEncoding Γ) : ∃ (f : List Γ → List Γ), TuringMachine.IsComputableFunction f ∧ (∀ (d : TuringMachine.TMDesc Γ), ∃ (g : ContextFreeGrammar Γ), f (tmEnc.encode d) = cfgEnc.encode g ∧ (g.language = Set.univ ↔ ¬d.accepts)) ∧ ∀ (w : List Γ), (∀ (d : TuringMachine.TMDesc Γ), tmEnc.encode d ≠ w) → ∃ (g : ContextFreeGrammar Γ), f w = cfgEnc.encode g ∧ g.language = Set.univ

Re-export of the computation-history CFG construction at the top level.

theorem AllCFG.A_TM_mapping_reduces_to_compl_ALL_CFG {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (cfgEnc : CFGEncoding Γ) : TuringMachine.MappingReducible (TuringMachine.A_TM tmEnc) (ALL_CFG cfgEnc)ᶜ

Mapping reduction A_TM ≤ₘ (ALL_CFG)ᶜ. Via the computation-history CFG construction, the acceptance problem reduces to the complement of CFG universality.

theorem AllCFG.A_TM_decidable_of_ALL_CFG_decidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (cfgEnc : CFGEncoding Γ) (hALL : TuringMachine.IsTuringDecidable (ALL_CFG cfgEnc)) : TuringMachine.IsTuringDecidable (TuringMachine.A_TM tmEnc)

If ALL_CFG were decidable, so would A_TM be: flip the ALL_CFG-decider and compose with the reduction f.

theorem AllCFG.ALL_CFG_not_decidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (cfgEnc : CFGEncoding Γ) : ¬TuringMachine.IsTuringDecidable (ALL_CFG cfgEnc)

Theorem (Sipser Lecture 10). ALL_CFG = {⟨G⟩ | L(G) = Σ*} is undecidable.

theorem ALL_CFG_undecidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (cfgEnc : AllCFG.CFGEncoding Γ) : ¬TuringMachine.IsTuringDecidable (AllCFG.ALL_CFG cfgEnc)

Restatement of ALL_CFG_not_decidable at the root namespace level.

theorem TuringMachine.isTuringDecidable_of_mappingReducible {Γ : Type} (enc : TMEncoding Γ) {A B : Set (List Γ)} (hAB : MappingReducible A B) (hB : IsTuringDecidable B) : IsTuringDecidable A

Sipser Lecture 9 (mapping reductions preserve decidability). If A ≤ₘ B and B is decidable, then so is A: compose the reduction transducer with the decider for B.

theorem PostCorrespondence.dominoConstructionIsComputable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (pcpEnc : PCPEncoding Γ) : ∃ (pcpFor : TuringMachine.TMDesc Γ → PCPInstance Γ), (∀ (d : TuringMachine.TMDesc Γ), hasMatch (pcpFor d) ↔ d.accepts) ∧ TuringMachine.IsComputableFunction fun (w : List Γ) => if h : ∃ (d : TuringMachine.TMDesc Γ), tmEnc.encode d = w then pcpEnc.encode (pcpFor h.choose) else pcpEnc.encode []

Sipser's PCP construction. There is a map pcpFor from TM descriptions to PCP instances such that the constructed instance has a match iff the TM accepts its input, and the overall input-to-encoding map is TM-computable. This is the technical heart of the reduction A_TM ≤ₘ PCP.

theorem PostCorrespondence.computationHistoryPCPConstruction {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (pcpEnc : PCPEncoding Γ) : ∃ (f : List Γ → List Γ), TuringMachine.IsComputableFunction f ∧ (∀ (d : TuringMachine.TMDesc Γ), ∃ (P : PCPInstance Γ), f (tmEnc.encode d) = pcpEnc.encode P ∧ (hasMatch P ↔ d.accepts)) ∧ ∀ (w : List Γ), (∀ (d : TuringMachine.TMDesc Γ), tmEnc.encode d ≠ w) → ∃ (P : PCPInstance Γ), f w = pcpEnc.encode P ∧ ¬hasMatch P

Computation-history PCP construction. A computable function f maps any TM encoding to a PCP-instance encoding so that the PCP instance has a match iff the TM accepts its input, and on inputs that are not TM encodings the resulting PCP instance has no match. Combined with the empty-list lemma, this yields the mapping reduction A_TM ≤ₘ PCP.

theorem PostCorrespondence.A_TM_reduces_to_PCP {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (pcpEnc : PCPEncoding Γ) : TuringMachine.MappingReducible (TuringMachine.A_TM tmEnc) (PCP pcpEnc)

Mapping reduction A_TM ≤ₘ PCP. Using the computation-history PCP construction, the acceptance problem many-one reduces to PCP.

theorem PostCorrespondence.A_TM_decidable_of_PCP_decidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (pcpEnc : PCPEncoding Γ) (hPCP : TuringMachine.IsTuringDecidable (PCP pcpEnc)) : TuringMachine.IsTuringDecidable (TuringMachine.A_TM tmEnc)

If PCP were decidable, so would A_TM be (immediate consequence of the mapping reduction and decidability transferring along mapping reductions).

theorem PostCorrespondence.PCP_not_decidable {Γ : Type} (tmEnc : TuringMachine.TMEncoding Γ) (pcpEnc : PCPEncoding Γ) : ¬TuringMachine.IsTuringDecidable (PCP pcpEnc)

Theorem (Sipser Lecture 10). The Post Correspondence Problem PCP = {⟨P⟩ | P has a match} is undecidable, by reduction from A_TM.