Lax132576.TransducerCodes

Codes of automata with output, and decidability under a promise

concepts/Lax132576/TransducerCodes.lean · lax-132576

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 62 of the paper of lax-157538, Transducers

Definition

The decidability statements of the book are about algorithms whose inputs are automata. An automaton with output whose states and letters are natural numbers is described by a finite code: the list of its transitions $(p, u, v, q)$ — from state $p$ to state $q$ , reading $u$ and writing $v$ — and the lists of its initial and final states. A code mentions only finitely many letters, its alphabet; a string over that alphabet is a code word. A code is functional if the relation it describes is a total function on the code words: every code word has exactly one output.

A problem "given an automaton satisfying a promise, decide whether it has a property" is decidable if there is a computable Boolean-valued function on codes that answers correctly on every code satisfying the promise. This is the form of Theorems B.3.4, B.4.2 and Lemma B.4.3 (and of Theorem C.1.4 in Part C).

Lean source view on GitHub

1	import Mathlib.Computability.Halting
2	import Lax132576.RationalRelations
3
4	/-!
5	---
6	title: Codes of automata with output, and decidability under a promise
7	type: definition
8	---
9	The decidability statements of the book are about algorithms whose inputs are
10	automata. An automaton with output whose states and letters are natural numbers
11	is described by a finite code: the list of its transitions $(p, u, v, q)$ —
12	from state $p$ to state $q$ , reading $u$ and writing $v$ — and the lists of its
13	initial and final states. A code mentions only finitely many letters, its
14	alphabet; a string over that alphabet is a code word. A code is
15	functional if the relation it describes is a total function on the code words:
16	every code word has exactly one output.
17
18	A problem "given an automaton satisfying a promise, decide whether it has a
19	property" is decidable if there is a computable Boolean-valued function on
20	codes that answers correctly on every code satisfying the promise. This is the
21	form of Theorems B.3.4, B.4.2 and Lemma B.4.3 (and of Theorem C.1.4 in Part C).
22
23	# Formalization notes
24
25	`RelCode` is a structure with the three lists as named fields; it is
26	`Primcodable` through the evident bijection with a tuple, so that
27	computability of functions on codes is mathlib's `Computable`. `codeAut c` is
28	the automaton with output over the alphabet `ℕ` that the code describes, and
29	`codeRel c` its relation. Totality over all of `ℕ*` cannot be asked for — a
30	code reads only the letters of its alphabet, so no code describes a total
31	function on `ℕ*` — which is why the promise `CodeFunctional` and the decided
32	properties are relativised to the code words; `DecidableUnderPromise promise P`
33	is the existence of a computable decision procedure correct under the promise.
34	-/
35
36	namespace Lax132576.TransducerCodes
37
38	open Lax132576.LabelledAutomata Lax132576.RationalRelations
39
40	/-- A code of an automaton with output over the alphabet `ℕ` with states in `ℕ`:
41	its transitions `(p, u, v, q)` and its initial and final states. -/
42	structure RelCode where
43	/-- The transitions `(p, u, v, q)`: from `p` to `q`, reading `u`, writing `v`. -/
44	transitions : List (ℕ × List ℕ × List ℕ × ℕ)
45	/-- The initial states. -/
46	init : List ℕ
47	/-- The final states. -/
48	final : List ℕ
49
50	/-- A code is the tuple of its three lists. -/
51	def relCodeEquiv : RelCode ≃ List (ℕ × List ℕ × List ℕ × ℕ) × List ℕ × List ℕ where
52	toFun c := (c.transitions, c.init, c.final)
53	invFun x := ⟨x.1, x.2.1, x.2.2⟩
54	left_inv := by rintro ⟨t, i, f⟩; rfl
55	right_inv := by rintro ⟨t, i, f⟩; rfl
56
57	instance : Primcodable RelCode := Primcodable.ofEquiv _ relCodeEquiv
58
59	/-- The automaton with output described by a code. -/
60	def codeAut (c : RelCode) : NFAO ℕ ℕ ℕ where
61	init := {q \| q ∈ c.init}
62	final := {q \| q ∈ c.final}
63	δ := {t \| t ∈ c.transitions}
64	δ_finite := c.transitions.finite_toSet
65
66	/-- The rational relation described by a code. -/
67	def codeRel (c : RelCode) : List ℕ → List ℕ → Prop := (codeAut c).rel
68
69	/-- The alphabet of a code: the letters occurring in the input strings of its
70	transitions. -/
71	def codeAlphabet (c : RelCode) : List ℕ := c.transitions.flatMap (fun t => t.2.1)
72
73	/-- A string over the alphabet of the code. -/
74	def CodeWord (c : RelCode) (w : List ℕ) : Prop := ∀ x ∈ w, x ∈ codeAlphabet c
75
76	/-- The relation described by the code is a total function on the code words. -/
77	def CodeFunctional (c : RelCode) : Prop := ∀ w, CodeWord c w → ∃! v, codeRel c w v
78
79	/-- A property `P` is decidable under a promise if a computable Boolean-valued
80	function answers `P` correctly on every input satisfying the promise. -/
81	def DecidableUnderPromise {α : Type} [Primcodable α] (promise P : α → Prop) : Prop :=
82	∃ D : α → Bool, Computable D ∧ ∀ a, promise a → (D a = true ↔ P a)
83
84	end Lax132576.TransducerCodes
85

Formalization notes

$RelCode$ is a structure with the three lists as named fields; it is $Primcodable$ through the evident bijection with a tuple, so that computability of functions on codes is mathlib's $Computable$ . $codeAut c$ is the automaton with output over the alphabet $ℕ$ that the code describes, and $codeRel c$ its relation. Totality over all of $ℕ*$ cannot be asked for — a code reads only the letters of its alphabet, so no code describes a total function on $ℕ*$ — which is why the promise $CodeFunctional$ and the decided properties are relativised to the code words; $DecidableUnderPromise promise P$ is the existence of a computable decision procedure correct under the promise.

Builds on

Lax132576.RationalRelations

Used by

From Mathlib

Mathlib.Computability.Halting

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