Lax251941.Acceptance

The acceptance problem for machines

concepts/Lax251941/Acceptance.lean · lax-251941

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

Following Sipser's Introduction to the Theory of Computation, Section 4.2, a machine $M$ run on an input $w$ either accepts, rejects, or loops; $M$ recognises the language $A$ if it accepts exactly the words of $A$ , and decides $A$ if moreover it halts on every input, accepting or rejecting. A language is Turing-recognisable if some machine recognises it and decidable if some machine decides it. The acceptance problem is the language

A_{TM} = \{\langle M, w\rangle \mid M \text{ is a machine and } M \text{ accepts } w\},

where $\langle M, w \rangle$ encodes a machine together with an input word.

Lean source view on GitHub

1	import Mathlib.Computability.PartrecCode
2
3	/-!
4	---
5	title: The acceptance problem for machines
6	type: definition
7	---
8	Following Sipser's Introduction to the Theory of Computation, Section 4.2, a
9	machine $M$ run on an input $w$ either accepts, rejects, or loops; $M$
10	recognises the language $A$ if it accepts exactly the words of $A$ , and
11	decides $A$ if moreover it halts on every input, accepting or rejecting. A
12	language is Turing-recognisable if some machine recognises it and decidable
13	if some machine decides it. The acceptance problem is the language
14	$A_{TM} = \{\langle M, w\rangle \mid M \text{ is a machine and } M \text{ accepts } w\},$
15	where $\langle M, w \rangle$ encodes a machine together with an input word.
16
17	# Formalization notes
18
19	Sipser's argument is about an arbitrary universal model of computation; the
20	machines here are mathlib's partial recursive programs `Nat.Partrec.Code`, which
21	supply exactly the two ingredients his proof needs — a universal machine
22	(`Nat.Partrec.Code.eval_part`: evaluation is itself computable) and the ability
23	to program every partial recursive function as a machine
24	(`Nat.Partrec.Code.exists_code`). Inputs and outputs are natural numbers, which
25	play the role of strings; a machine accepts by halting with output `1` and
26	rejects by halting with output `0`, so that accepting, rejecting and looping
27	are the three mutually exclusive outcomes of Sipser's definition. The pair
28	$\langle M, w\rangle$ is the Cantor pairing of the code of `M` (mathlib's
29	`Encodable.encode`, under which the programs are `Denumerable`) with `w`.
30	Turing machines in the literal sense, with a tape, appear in `TuringMachines`;
31	they are where the reduction to the Post correspondence problem lives.
32	-/
33
34	namespace Lax251941.Acceptance
35
36	/-- A machine: a partial recursive program. -/
37	abbrev Machine := Nat.Partrec.Code
38
39	/-- `M` accepts `w` if it halts on `w` with output `1`. -/
40	def Accepts (M : Machine) (w : ℕ) : Prop := M.eval w = Part.some 1
41
42	/-- `M` rejects `w` if it halts on `w` with output `0`. -/
43	def Rejects (M : Machine) (w : ℕ) : Prop := M.eval w = Part.some 0
44
45	/-- A machine is a decider if it accepts or rejects every input, i.e. never loops.
46	-/
47	def IsDecider (M : Machine) : Prop := ∀ w, Accepts M w ∨ Rejects M w
48
49	/-- `M` recognises the language `A` if it accepts exactly the words of `A`. -/
50	def Recognizes (M : Machine) (A : Set ℕ) : Prop := ∀ w, w ∈ A ↔ Accepts M w
51
52	/-- `M` decides `A` if it is a decider that recognises `A`. -/
53	def Decides (M : Machine) (A : Set ℕ) : Prop := IsDecider M ∧ Recognizes M A
54
55	/-- A language is Turing-recognisable if some machine recognises it. -/
56	def TuringRecognizable (A : Set ℕ) : Prop := ∃ M, Recognizes M A
57
58	/-- A language is decidable if some machine decides it. -/
59	def TuringDecidable (A : Set ℕ) : Prop := ∃ M, Decides M A
60
61	/-- The acceptance problem `A_TM`: the pairs `⟨M, w⟩`, encoded by Cantor pairing
62	of the code of `M` with `w`, such that `M` accepts `w`. -/
63	def ATM : Set ℕ := {n \| Accepts (Denumerable.ofNat Machine n.unpair.1) n.unpair.2}
64
65	end Lax251941.Acceptance
66

Formalization notes

Sipser's argument is about an arbitrary universal model of computation; the machines here are mathlib's partial recursive programs $Nat.Partrec.Code$ , which supply exactly the two ingredients his proof needs — a universal machine ( $Nat.Partrec.Code.eval_part$ : evaluation is itself computable) and the ability to program every partial recursive function as a machine ( $Nat.Partrec.Code.exists_code$ ). Inputs and outputs are natural numbers, which play the role of strings; a machine accepts by halting with output $1$ and rejects by halting with output $0$ , so that accepting, rejecting and looping are the three mutually exclusive outcomes of Sipser's definition. The pair $\langle M, w\rangle$ is the Cantor pairing of the code of $M$ (mathlib's $Encodable.encode$ , under which the programs are $Denumerable$ ) with $w$ . Turing machines in the literal sense, with a tape, appear in $TuringMachines$ ; they are where the reduction to the Post correspondence problem lives.

Builds on

none

Used by

Lax251941.AcceptanceUndecidable

From Mathlib

Mathlib.Computability.PartrecCode

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

The acceptance problem for machines

Flags

Flag this concept