Lax314295.LogicPrecomputation

Precomputing the answers of MSO formulas by a rational function

concepts/Lax314295/LogicPrecomputation.lean · lax-314295

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax314295.LogicPrecomputation

⊢Lax314295Proofs.Results.exists_rational_precomputation

In the paper

page 128 of the paper of lax-157538, Transducers

Theorem

For a finite set of mso formulas with one or two free first-order variables there is a letter-to-letter rational function $f : A^* \to C^*$ such that each formula $\varphi(x)$ with one free variable corresponds to a set of letters $F \subseteq C$ — $w \models \varphi(x)$ exactly when the letter of $f(w)$ at position $x$ is in $F$ — and each formula $\varphi(x, y)$ with two free variables corresponds to a regular language $L \subseteq C^*$ — for $x \le y$ , $w \models \varphi(x, y)$ exactly when the infix of $f(w)$ from $x$ to $y$ belongs to $L$ (Lemma C.4.10 of Transducers). The function decorates every position with the states, on the prefix and on the suffix, of the automata of Lemma C.4.2 for the formulas.

Lean source view on GitHub

1	import Lax765601.ElementaryProperties
2	import Lax132576.RationalFunctions
3	import Lax314295.MSOLogic
4
5	/-!
6	---
7	title: Precomputing the answers of MSO formulas by a rational function
8	type: theorem
9	---
10	For a finite set of mso formulas with one or two free first-order variables
11	there is a letter-to-letter rational function $f : A^* \to C^*$ such that each
12	formula $\varphi(x)$ with one free variable corresponds to a set of letters
13	$F \subseteq C$ — $w \models \varphi(x)$ exactly when the letter of $f(w)$ at
14	position $x$ is in $F$ — and each formula $\varphi(x, y)$ with two free
15	variables corresponds to a regular language $L \subseteq C^*$ — for
16	$x \le y$ , $w \models \varphi(x, y)$ exactly when the infix of $f(w)$ from
17	$x$ to $y$ belongs to $L$ (Lemma C.4.10 of Transducers). The function
18	decorates every position with the states, on the prefix and on the suffix, of
19	the automata of Lemma C.4.2 for the formulas.
20
21	# Formalization notes
22
23	The formulas with one free variable use the variable `0`; those with two use
24	`0` and `1`, evaluated at `x ≤ y`. The infix from `x` to `y` is
25	`((f w).drop x).take (y - x + 1)`. The alphabet is assumed finite.
26	-/
27
28	namespace Lax314295.LogicPrecomputation
29
30	open Lax765601.ElementaryProperties Lax132576.RationalFunctions Lax314295.MSOLogic
31
32	/-- The answers of finitely many mso formulas with one or two free variables are
33	read off a letter-to-letter rational function: as letters, respectively as regular
34	languages of infixes. -/
35	axiom exists_rational_precomputation {A : Type} [Finite A]
36	(Φ₁ Φ₂ : Set (MSO A)) (hΦ₁ : Φ₁.Finite) (hΦ₂ : Φ₂.Finite) :
37	∃ (C : Type) (_ : Finite C) (f : List A → List C),
38	IsRationalFun f ∧ LengthPreserving f ∧
39	(∀ φ ∈ Φ₁, ∃ F : Set C, ∀ (w : List A) (x : ℕ), x < w.length →
40	(MSO.Sat w (fun _ => x) (fun _ => ∅) φ ↔ ∃ c ∈ F, (f w)[x]? = some c)) ∧
41	(∀ φ ∈ Φ₂, ∃ L : Language C, L.IsRegular ∧ ∀ (w : List A) (x y : ℕ),
42	x ≤ y → y < w.length →
43	(MSO.Sat w (fun i => if i = 0 then x else y) (fun _ => ∅) φ ↔
44	((f w).drop x).take (y - x + 1) ∈ L))
45
46	end Lax314295.LogicPrecomputation
47

Show Proof

Formalization notes

The formulas with one free variable use the variable $0$ ; those with two use $0$ and $1$ , evaluated at $x ≤ y$ . The infix from $x$ to $y$ is $((f w).drop x).take (y - x + 1)$ . The alphabet is assumed finite.

Builds on

Used by

none

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