Lax314295.MSOTransductions

String-to-string MSO transductions

concepts/Lax314295/MSOTransductions.lean · lax-314295

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 125 of the paper of lax-157538, Transducers

Definition

A string-to-string mso transduction (Definition C.4.7 of Transducers) is given by an input alphabet $A$ , an output alphabet $B$ , a linear type $\tau = k \cdot n + c$ — on an input of length $n$ it has $k$ copies of each input position and $c$ extra elements — and mso formulas over $A$ : a universe formula $\varphi_{\mathrm{univ}}(x : \tau)$ , a letter formula $\varphi_b(x : \tau)$ for each $b \in B$ , and an order formula $\varphi_\le(x : \tau, y : \tau)$ . It is required that for every input, every element selected by the universe formula satisfies exactly one letter formula and the order formula is a linear order on the selected elements. The output on $w$ is then the string obtained by taking the selected elements of $\tau(w)$ , ordering them by the order formula and labelling them by the letter formulas. Linearity of $\tau$ keeps the output of linear size; string-to-string mso transductions define exactly the regular functions (Theorem C.4.8).

Lean source view on GitHub

1	import Lax314295.MSOLogic
2
3	/-!
4	---
5	title: String-to-string MSO transductions
6	type: definition
7	---
8	A string-to-string mso transduction (Definition C.4.7 of Transducers) is
9	given by an input alphabet $A$ , an output alphabet $B$ , a linear type
10	$\tau = k \cdot n + c$ — on an input of length $n$ it has $k$ copies of each
11	input position and $c$ extra elements — and mso formulas over $A$ : a *universe
12	formula* $\varphi_{\mathrm{univ}}(x : \tau)$ , a letter formula
13	$\varphi_b(x : \tau)$ for each $b \in B$ , and an order formula
14	$\varphi_\le(x : \tau, y : \tau)$ . It is required that for every input, every
15	element selected by the universe formula satisfies exactly one letter formula
16	and the order formula is a linear order on the selected elements. The output on
17	$w$ is then the string obtained by taking the selected elements of $\tau(w)$ ,
18	ordering them by the order formula and labelling them by the letter formulas.
19	Linearity of $\tau$ keeps the output of linear size; string-to-string mso
20	transductions define exactly the regular functions (Theorem C.4.8).
21
22	# Formalization notes
23
24	A variable of the linear type $\tau = k \cdot n + c$ is a case distinction over
25	its $k + c$ variants, so the formulas are given per variant: `univP i` and
26	`labP i b` with the free variable `x₀` for the copies of the positions,
27	sentences `univC j`, `labC j b` for the extra elements, and four families of
28	order formulas according to the variants of the two arguments, with free
29	variables `x₀, x₁`. The elements of $\tau(w)$ are `Elt = (Fin copies × ℕ) ⊕ Fin
30	extra`, `selected` those chosen by the universe formulas, `ordRel` and `labRel`
31	the relations defined by the order and letter formulas, and `Outputs T w v`
32	says that `v` lists the selected elements in the order, with their letters.
33	`Proper` is the requirement of the definition — exactly one letter formula per
34	selected element, and a linear order (reflexive, antisymmetric, transitive,
35	total) on the selected elements; without it every length preserving function
36	would be a transduction and Theorem C.4.8 would fail, so it is part of
37	`IsMSOTransduction`.
38	-/
39
40	namespace Lax314295.MSOTransductions
41
42	open Lax314295.MSOLogic
43
44	/-- A string-to-string mso transduction of the linear type `copies · n + extra`,
45	presented by families of ordinary mso formulas indexed by the variants of the
46	type. -/
47	structure MSOTransduction (A B : Type) where
48	/-- The number of copies of the input positions. -/
49	copies : ℕ
50	/-- The number of extra (constant) elements. -/
51	extra : ℕ
52	/-- Universe formulas for the copies of the positions; free variable `x₀`. -/
53	univP : Fin copies → MSO A
54	/-- Universe formulas for the extra elements; sentences. -/
55	univC : Fin extra → MSO A
56	/-- Letter formulas for the copies of the positions; free variable `x₀`. -/
57	labP : Fin copies → B → MSO A
58	/-- Letter formulas for the extra elements; sentences. -/
59	labC : Fin extra → B → MSO A
60	/-- Order formulas between two copies of positions; free variables `x₀, x₁`. -/
61	ordPP : Fin copies → Fin copies → MSO A
62	/-- Order formulas between a copy of a position and an extra element. -/
63	ordPC : Fin copies → Fin extra → MSO A
64	/-- Order formulas between an extra element and a copy of a position. -/
65	ordCP : Fin extra → Fin copies → MSO A
66	/-- Order formulas between two extra elements. -/
67	ordCC : Fin extra → Fin extra → MSO A
68
69	namespace MSOTransduction
70
71	variable {A B : Type}
72
73	/-- The elements of the type `copies · n + extra`, before selection. -/
74	abbrev Elt (T : MSOTransduction A B) : Type := (Fin T.copies × ℕ) ⊕ Fin T.extra
75
76	/-- The elements selected by the universe formulas. -/
77	def selected (T : MSOTransduction A B) (w : List A) : T.Elt → Prop
78	\| Sum.inl (i, p) => p < w.length ∧ MSO.Sat w (fun _ => p) (fun _ => ∅) (T.univP i)
79	\| Sum.inr j => MSO.Sat w (fun _ => 0) (fun _ => ∅) (T.univC j)
80
81	/-- The order defined by the order formulas. -/
82	def ordRel (T : MSOTransduction A B) (w : List A) : T.Elt → T.Elt → Prop
83	\| Sum.inl (i, p), Sum.inl (i', p') =>
84	MSO.Sat w (fun v => if v = 0 then p else p') (fun _ => ∅) (T.ordPP i i')
85	\| Sum.inl (i, p), Sum.inr j => MSO.Sat w (fun _ => p) (fun _ => ∅) (T.ordPC i j)
86	\| Sum.inr j, Sum.inl (i, p) => MSO.Sat w (fun _ => p) (fun _ => ∅) (T.ordCP j i)
87	\| Sum.inr j, Sum.inr j' => MSO.Sat w (fun _ => 0) (fun _ => ∅) (T.ordCC j j')
88
89	/-- The labelling defined by the letter formulas. -/
90	def labRel (T : MSOTransduction A B) (w : List A) : T.Elt → B → Prop
91	\| Sum.inl (i, p), b => MSO.Sat w (fun _ => p) (fun _ => ∅) (T.labP i b)
92	\| Sum.inr j, b => MSO.Sat w (fun _ => 0) (fun _ => ∅) (T.labC j b)
93
94	/-- The transduction outputs `v` on `w`: `v` lists the selected elements, without
95	repetition, in the order of the order formula, each labelled by a letter of
96	its letter formulas. -/
97	def Outputs (T : MSOTransduction A B) (w : List A) (v : List B) : Prop :=
98	∃ es : List T.Elt,
99	es.Nodup ∧
100	(∀ x, x ∈ es ↔ T.selected w x) ∧
101	(∀ (i j : ℕ) (hi : i < es.length) (hj : j < es.length),
102	i < j → T.ordRel w (es.get ⟨i, hi⟩) (es.get ⟨j, hj⟩)) ∧
103	es.length = v.length ∧
104	∀ (i : ℕ) (hi : i < es.length) (hi' : i < v.length),
105	T.labRel w (es.get ⟨i, hi⟩) (v.get ⟨i, hi'⟩)
106
107	/-- The requirement of Definition C.4.7: on every input, every selected element
108	satisfies exactly one letter formula, and the order formula is a linear order
109	on the selected elements. -/
110	def Proper (T : MSOTransduction A B) : Prop :=
111	∀ w : List A,
112	(∀ x, T.selected w x → ∃! b, T.labRel w x b) ∧
113	(∀ x, T.selected w x → T.ordRel w x x) ∧
114	(∀ x y, T.selected w x → T.selected w y →
115	T.ordRel w x y → T.ordRel w y x → x = y) ∧
116	(∀ x y z, T.selected w x → T.selected w y → T.selected w z →
117	T.ordRel w x y → T.ordRel w y z → T.ordRel w x z) ∧
118	(∀ x y, T.selected w x → T.selected w y → T.ordRel w x y ∨ T.ordRel w y x)
119
120	/-- All formulas of the transduction are first-order. -/
121	def AllFO (T : MSOTransduction A B) : Prop :=
122	(∀ i, (T.univP i).IsFO) ∧ (∀ j, (T.univC j).IsFO) ∧
123	(∀ i b, (T.labP i b).IsFO) ∧ (∀ j b, (T.labC j b).IsFO) ∧
124	(∀ i i', (T.ordPP i i').IsFO) ∧ (∀ i j, (T.ordPC i j).IsFO) ∧
125	(∀ j i, (T.ordCP j i).IsFO) ∧ (∀ j j', (T.ordCC j j').IsFO)
126
127	end MSOTransduction
128
129	/-- A function defined by a string-to-string mso transduction satisfying the
130	requirements of the definition. -/
131	def IsMSOTransduction {A B : Type} (f : List A → List B) : Prop :=
132	∃ T : MSOTransduction A B, T.Proper ∧ ∀ w, T.Outputs w (f w)
133
134	/-- A function defined by a first-order transduction. -/
135	def IsFOTransduction {A B : Type} (f : List A → List B) : Prop :=
136	∃ T : MSOTransduction A B, T.Proper ∧ T.AllFO ∧ ∀ w, T.Outputs w (f w)
137
138	end Lax314295.MSOTransductions
139

Formalization notes

A variable of the linear type $\tau = k \cdot n + c$ is a case distinction over its $k + c$ variants, so the formulas are given per variant: $univP i$ and $labP i b$ with the free variable $x₀$ for the copies of the positions, sentences $univC j$ , $labC j b$ for the extra elements, and four families of order formulas according to the variants of the two arguments, with free variables $x₀, x₁$ . The elements of $\tau(w)$ are $Elt = (Fin copies × ℕ) ⊕ Fin extra$ , $selected$ those chosen by the universe formulas, $ordRel$ and $labRel$ the relations defined by the order and letter formulas, and $Outputs T w v$ says that $v$ lists the selected elements in the order, with their letters. $Proper$ is the requirement of the definition — exactly one letter formula per selected element, and a linear order (reflexive, antisymmetric, transitive, total) on the selected elements; without it every length preserving function would be a transduction and Theorem C.4.8 would fail, so it is part of $IsMSOTransduction$ .

Builds on

Lax314295.MSOLogic

Used by

From Mathlib

none

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