Lax194892.PebbleReachability

Reachability between configurations of a pebble transducer is regular

concepts/Lax194892/PebbleReachability.lean · lax-194892

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✓Lax194892.PebbleReachability

⊢Lax194892Proofs.Results.exists_regular_reachLang

In the paper

page 166 of the paper of lax-157538, Transducers

Theorem

Reachability between two configurations of a $k$ -pebble transducer is definable: there is an mso formula $\varphi(s, t)$ over configurations which holds if some run begins in $s$ and ends in $t$ (Lemma D.2.2 of Transducers). Reachability is reduced, by induction on the height, to reachability between configurations that share their lower pebbles, which is checked by a pebble automaton with one pebble more.

Lean source view on GitHub

1	import Mathlib.Computability.DFA
2	import Lax194892.PebbleConfigurationEncoding
3
4	/-!
5	---
6	title: Reachability between configurations of a pebble transducer is regular
7	type: theorem
8	---
9	Reachability between two configurations of a $k$ -pebble transducer is
10	definable: there is an mso formula $\varphi(s, t)$ over configurations which
11	holds if some run begins in $s$ and ends in $t$ (Lemma D.2.2 of
12	Transducers). Reachability is reduced, by induction on the height, to
13	reachability between configurations that share their lower pebbles, which is
14	checked by a pebble automaton with one pebble more.
15
16	# Formalization notes
17
18	The book asks for an mso formula whose two free variables range over
19	configurations. Here the pair of configurations is encoded into the input
20	string (`pairEnc`, one letter per gap) and the conclusion is that the set of
21	encodings of reachable pairs is a regular language — equivalently, by Büchi's
22	theorem, an mso-definable one. Since a formula is only ever evaluated on a
23	genuine structure, the language is only required to be correct on genuine
24	encodings: stacks of at most `k` gaps of the input. Stated for pebble
25	transducers rather than pebble automata, which have the same configuration
26	graph.
27	-/
28
29	namespace Lax194892.PebbleReachability
30
31	open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding
32
33	/-- The encodings of pairs of configurations connected by a run form a regular
34	language. -/
35	axiom exists_regular_reachLang {A B Q : Type} {k : ℕ} [Finite A] [Finite Q] (M : Pebble A B Q k) :
36	∃ L : Language (PairLetter A Q k), L.IsRegular ∧
37	∀ (q₁ q₂ : Q) (sts stt : List ℕ) (w : List A),
38	(∀ p ∈ sts, p ≤ w.length) → (∀ p ∈ stt, p ≤ w.length) →
39	sts.length ≤ k → stt.length ≤ k →
40	(pairEnc q₁ q₂ sts stt w ∈ L ↔
41	∃ v, M.Reaches w (PebbleCfg.conf q₁ sts) v (PebbleCfg.conf q₂ stt))
42
43	end Lax194892.PebbleReachability
44

Show Proof

Formalization notes

The book asks for an mso formula whose two free variables range over configurations. Here the pair of configurations is encoded into the input string ( $pairEnc$ , one letter per gap) and the conclusion is that the set of encodings of reachable pairs is a regular language — equivalently, by Büchi's theorem, an mso-definable one. Since a formula is only ever evaluated on a genuine structure, the language is only required to be correct on genuine encodings: stacks of at most $k$ gaps of the input. Stated for pebble transducers rather than pebble automata, which have the same configuration graph.

Builds on

Lax194892.PebbleConfigurationEncoding

Used by

none

From Mathlib

Mathlib.Computability.DFA

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