Lax314295.MSORelabellings

MSO relabellings

concepts/Lax314295/MSORelabellings.lean · lax-314295

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 120 of the paper of lax-157538, Transducers

Definition

An mso relabelling (Definition C.4.3 of Transducers) consists of an input alphabet $A$ , an output alphabet $B$ , a finite set $\Phi$ of mso formulas over $A$ each with exactly one free first-order variable, an output map $\Phi \to B^*$ , and a string in $B^*$ for the empty input, such that for every input string and every position in it exactly one formula of $\Phi$ is true at that position. The relabelling maps a nonempty input to the concatenation, over its positions, of the outputs of the unique formulas true there, and the empty input to the designated string. MSO relabellings define exactly the rational functions (Theorem C.4.4), and first-order relabellings — all of whose formulas are first-order — exactly the functions of aperiodic bimachines (Theorem C.4.16).

Lean source view on GitHub

1	import Lax314295.MSOLogic
2
3	/-!
4	---
5	title: MSO relabellings
6	type: definition
7	---
8	An mso relabelling (Definition C.4.3 of Transducers) consists of an input
9	alphabet $A$ , an output alphabet $B$ , a finite set $\Phi$ of mso formulas over
10	$A$ each with exactly one free first-order variable, an output map
11	$\Phi \to B^$ , and a string in $B^$ for the empty input, such that for every
12	input string and every position in it exactly one formula of $\Phi$ is true at
13	that position. The relabelling maps a nonempty input to the concatenation, over
14	its positions, of the outputs of the unique formulas true there, and the empty
15	input to the designated string. MSO relabellings define exactly the rational
16	functions (Theorem C.4.4), and first-order relabellings — all of whose
17	formulas are first-order — exactly the functions of aperiodic bimachines
18	(Theorem C.4.16).
19
20	# Formalization notes
21
22	The set of formulas is indexed by a finite type `Idx`; the free variable of every
23	formula is the variable `0`, and a formula is evaluated at a position `p` under
24	the valuation sending every variable to `p`. `Relabels R w v` is the graph of
25	the relabelling, uniqueness of the true formula being a field of the structure.
26	-/
27
28	namespace Lax314295.MSORelabellings
29
30	open Lax314295.MSOLogic
31
32	/-- An mso relabelling: a finite family of formulas with one free first-order
33	variable (the variable `0`), exactly one of which holds at each position of each
34	input, an output string for each formula, and an output for the empty input. -/
35	structure MSORelabelling (A B : Type) where
36	/-- The index set of the formulas. -/
37	Idx : Type
38	/-- Finiteness of the index set. -/
39	finIdx : Finite Idx
40	/-- The formulas, each with the one free first-order variable `x₀`. -/
41	form : Idx → MSO A
42	/-- The output string of each formula. -/
43	out : Idx → List B
44	/-- The output string for the empty input. -/
45	emptyOut : List B
46	/-- At every position of every input string exactly one formula holds. -/
47	unique : ∀ (w : List A) (p : ℕ), p < w.length →
48	∃! i : Idx, MSO.Sat w (fun _ => p) (fun _ => ∅) (form i)
49
50	namespace MSORelabelling
51
52	variable {A B : Type}
53
54	/-- The relabelling maps `w` to `v`: for a nonempty input, `v` is the concatenation
55	of the outputs of the formulas true at the positions of `w`; the empty input
56	gives the designated string. -/
57	def Relabels (R : MSORelabelling A B) (w : List A) (v : List B) : Prop :=
58	(w = [] ∧ v = R.emptyOut) ∨
59	(w ≠ [] ∧ ∃ g : ℕ → R.Idx,
60	(∀ p < w.length, MSO.Sat w (fun _ => p) (fun _ => ∅) (R.form (g p))) ∧
61	v = ((List.range w.length).map (fun p => R.out (g p))).flatten)
62
63	/-- All formulas of the relabelling are first-order. -/
64	def AllFO (R : MSORelabelling A B) : Prop := ∀ i, (R.form i).IsFO
65
66	end MSORelabelling
67
68	/-- A function defined by an mso relabelling. -/
69	def IsMSORelabelling {A B : Type} (f : List A → List B) : Prop :=
70	∃ R : MSORelabelling A B, ∀ w, R.Relabels w (f w)
71
72	/-- A function defined by a first-order relabelling. -/
73	def IsFORelabelling {A B : Type} (f : List A → List B) : Prop :=
74	∃ R : MSORelabelling A B, R.AllFO ∧ ∀ w, R.Relabels w (f w)
75
76	end Lax314295.MSORelabellings
77

Formalization notes

The set of formulas is indexed by a finite type $Idx$ ; the free variable of every formula is the variable $0$ , and a formula is evaluated at a position $p$ under the valuation sending every variable to $p$ . $Relabels R w v$ is the graph of the relabelling, uniqueness of the true formula being a field of the structure.

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