Lax314295.MSOLogic

Monadic second-order logic on strings

concepts/Lax314295/MSOLogic.lean · lax-314295

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 118 of the paper of lax-157538, Transducers

Definition

A string $w \in A^*$ is a structure whose universe is the set of positions of $w$ , with the order $x \le y$ on positions and, for every letter $a \in A$ , the unary predicate $a(x)$ "position $x$ carries the letter $a$ ". Monadic second-order logic (mso) has first-order variables ranging over positions and second-order variables ranging over sets of positions, the atomic formulas $x \le y$ , $a(x)$ and $x \in X$ , Boolean connectives, and existential quantification over both kinds of variables (Section C.4.1 of Transducers). A sentence — a formula without free variables — defines the language of the strings that satisfy it; the first-order fragment is the set of formulas that use neither set variables nor membership. A formula with free variables is evaluated on a string together with a valuation, which the book represents by annotating the string: the string $w \otimes \{x_1\} \otimes \cdots \otimes X_\ell$ over the alphabet $A \times 2^{k + \ell}$ carries at every position the bits saying which of the variables point to it.

Lean source view on GitHub

1	import Mathlib.Computability.DFA
2	import Mathlib.Data.Fintype.Basic
3
4	/-!
5	---
6	title: Monadic second-order logic on strings
7	type: definition
8	---
9	A string $w \in A^*$ is a structure whose universe is the set of positions of
10	$w$ , with the order $x \le y$ on positions and, for every letter $a \in A$ , the
11	unary predicate $a(x)$ "position $x$ carries the letter $a$ ". *Monadic
12	second-order logic* (mso) has first-order variables ranging over positions and
13	second-order variables ranging over sets of positions, the atomic formulas
14	$x \le y$ , $a(x)$ and $x \in X$ , Boolean connectives, and existential
15	quantification over both kinds of variables (Section C.4.1 of Transducers).
16	A sentence — a formula without free variables — defines the language of the
17	strings that satisfy it; the first-order fragment is the set of formulas that
18	use neither set variables nor membership. A formula with free variables is
19	evaluated on a string together with a valuation, which the book represents by
20	annotating the string: the string $w \otimes \{x_1\} \otimes \cdots \otimes X_\ell$
21	over the alphabet $A \times 2^{k + \ell}$ carries at every position the bits
22	saying which of the variables point to it.
23
24	# Formalization notes
25
26	Variables of both kinds are named by natural numbers, and a valuation is a pair
27	of functions `ℕ → ℕ` (positions of the first-order variables) and `ℕ → Set ℕ`
28	(sets of positions of the second-order variables); quantifiers range over
29	positions `p < w.length` and subsets of them. Satisfaction, the first-order
30	fragment, the quantifier rank and the free variables of a formula are defined
31	by recursion on the syntax; `MSODefinable L` asks for a formula satisfied by
32	exactly the strings of `L` under every valuation, which for a sentence is the
33	usual notion and for a formula with free variables is the same as for its
34	universal closure. `annotate k l w fo so` is the annotated string of a valuation
35	of the variables `0, …, k-1` and `0, …, l-1`, and `extFO`/`extSO` extend such a
36	valuation to all variables. Alphabets are arbitrary types; finiteness is a
37	hypothesis of the theorems.
38	-/
39
40	namespace Lax314295.MSOLogic
41
42	/-- Formulas of monadic second-order logic over strings with letters in `A`;
43	first-order and second-order variables are named by natural numbers. -/
44	inductive MSO (A : Type) : Type
45	/-- The order test `x_i ≤ x_j`. -/
46	\| le : ℕ → ℕ → MSO A
47	/-- The label test `a (x_i)`. -/
48	\| lab : A → ℕ → MSO A
49	/-- The membership test `x_i ∈ X_j`. -/
50	\| mem : ℕ → ℕ → MSO A
51	/-- Negation. -/
52	\| not : MSO A → MSO A
53	/-- Conjunction. -/
54	\| and : MSO A → MSO A → MSO A
55	/-- Disjunction. -/
56	\| or : MSO A → MSO A → MSO A
57	/-- First-order existential quantification `∃ x_i`. -/
58	\| exFO : ℕ → MSO A → MSO A
59	/-- Second-order existential quantification `∃ X_i`. -/
60	\| exSO : ℕ → MSO A → MSO A
61
62	namespace MSO
63
64	variable {A : Type}
65
66	/-- Satisfaction of a formula in a string under a valuation of the first-order
67	variables by positions and of the second-order variables by sets of positions. -/
68	def Sat (w : List A) : (ℕ → ℕ) → (ℕ → Set ℕ) → MSO A → Prop
69	\| fo, _, le i j => fo i ≤ fo j
70	\| fo, _, lab a i => w[fo i]? = some a
71	\| fo, so, mem i j => fo i ∈ so j
72	\| fo, so, not φ => ¬ Sat w fo so φ
73	\| fo, so, and φ ψ => Sat w fo so φ ∧ Sat w fo so ψ
74	\| fo, so, or φ ψ => Sat w fo so φ ∨ Sat w fo so ψ
75	\| fo, so, exFO i φ => ∃ p < w.length, Sat w (Function.update fo i p) so φ
76	\| fo, so, exSO i φ => ∃ S ⊆ {p \| p < w.length}, Sat w fo (Function.update so i S) φ
77
78	/-- A formula is first-order if it uses neither set quantification nor membership.
79	-/
80	def IsFO : MSO A → Prop
81	\| le _ _ => True
82	\| lab _ _ => True
83	\| mem _ _ => False
84	\| not φ => IsFO φ
85	\| and φ ψ => IsFO φ ∧ IsFO ψ
86	\| or φ ψ => IsFO φ ∧ IsFO ψ
87	\| exFO _ φ => IsFO φ
88	\| exSO _ _ => False
89
90	/-- The quantifier rank: the maximal number of nested quantifiers. -/
91	def qrank : MSO A → ℕ
92	\| le _ _ => 0
93	\| lab _ _ => 0
94	\| mem _ _ => 0
95	\| not φ => qrank φ
96	\| and φ ψ => max (qrank φ) (qrank ψ)
97	\| or φ ψ => max (qrank φ) (qrank ψ)
98	\| exFO _ φ => qrank φ + 1
99	\| exSO _ φ => qrank φ + 1
100
101	/-- The free first-order variables of a formula. -/
102	def freeFO : MSO A → Set ℕ
103	\| le i j => {i, j}
104	\| lab _ i => {i}
105	\| mem i _ => {i}
106	\| not φ => freeFO φ
107	\| and φ ψ => freeFO φ ∪ freeFO ψ
108	\| or φ ψ => freeFO φ ∪ freeFO ψ
109	\| exFO i φ => freeFO φ \ {i}
110	\| exSO _ φ => freeFO φ
111
112	/-- The free second-order variables of a formula. -/
113	def freeSO : MSO A → Set ℕ
114	\| le _ _ => ∅
115	\| lab _ _ => ∅
116	\| mem _ j => {j}
117	\| not φ => freeSO φ
118	\| and φ ψ => freeSO φ ∪ freeSO ψ
119	\| or φ ψ => freeSO φ ∪ freeSO ψ
120	\| exFO _ φ => freeSO φ
121	\| exSO i φ => freeSO φ \ {i}
122
123	end MSO
124
125	/-- A language is definable in monadic second-order logic. -/
126	def MSODefinable {A : Type} (L : Language A) : Prop :=
127	∃ φ : MSO A, ∀ (w : List A) (fo : ℕ → ℕ) (so : ℕ → Set ℕ), MSO.Sat w fo so φ ↔ w ∈ L
128
129	/-- A language is definable in first-order logic. -/
130	def FODefinable {A : Type} (L : Language A) : Prop :=
131	∃ φ : MSO A, φ.IsFO ∧
132	∀ (w : List A) (fo : ℕ → ℕ) (so : ℕ → Set ℕ), MSO.Sat w fo so φ ↔ w ∈ L
133
134	open scoped Classical in
135	/-- The annotation `w ⊗ {x₁} ⊗ ⋯ ⊗ {x_k} ⊗ X₁ ⊗ ⋯ ⊗ X_l` of a string by the values
136	of `k` first-order and `l` second-order variables. -/
137	noncomputable def annotate {A : Type} (k l : ℕ) (w : List A)
138	(fo : Fin k → ℕ) (so : Fin l → Set ℕ) : List (A × (Fin k → Bool) × (Fin l → Bool)) :=
139	w.zipIdx.map (fun z => (z.1, fun i => decide (fo i = z.2), fun j => decide (z.2 ∈ so j)))
140
141	/-- Extend a valuation of the first-order variables `0, …, k-1` to all variables. -/
142	def extFO (k : ℕ) (fo : Fin k → ℕ) : ℕ → ℕ :=
143	fun i => if h : i < k then fo ⟨i, h⟩ else 0
144
145	/-- Extend a valuation of the set variables `0, …, l-1` to all variables. -/
146	def extSO (l : ℕ) (so : Fin l → Set ℕ) : ℕ → Set ℕ :=
147	fun j => if h : j < l then so ⟨j, h⟩ else ∅
148
149	end Lax314295.MSOLogic
150

Formalization notes

Variables of both kinds are named by natural numbers, and a valuation is a pair of functions $ℕ → ℕ$ (positions of the first-order variables) and $ℕ → Set ℕ$ (sets of positions of the second-order variables); quantifiers range over positions $p < w.length$ and subsets of them. Satisfaction, the first-order fragment, the quantifier rank and the free variables of a formula are defined by recursion on the syntax; $MSODefinable L$ asks for a formula satisfied by exactly the strings of $L$ under every valuation, which for a sentence is the usual notion and for a formula with free variables is the same as for its universal closure. $annotate k l w fo so$ is the annotated string of a valuation of the variables $0, …, k-1$ and $0, …, l-1$ , and $extFO$ / $extSO$ extend such a valuation to all variables. Alphabets are arbitrary types; finiteness is a hypothesis of the theorems.

Builds on

none

Used by

From Mathlib

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