Lax194892.ChildrenOfConfiguration

A for-transducer produces the children of a configuration

concepts/Lax194892/ChildrenOfConfiguration.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.ChildrenOfConfiguration

⊢Lax194892Proofs.Results.exists_forTransducer_children

In the paper

page 169 of the paper of lax-157538, Transducers

Theorem

For every $k$ -pebble transducer there is a for-transducer which inputs the string representation of a configuration and outputs all children of that configuration, as the concatenation of their string representations in order of execution (Lemma D.2.5 of Transducers). It is the composition of Claims D.2.6 and D.2.7: from the configuration to its child configuration graph, and from the graph to the children.

Lean source view on GitHub

1	import Lax194892.ForTransducers
2	import Lax194892.ChildConfigurationGraphs
3
4	/-!
5	---
6	title: A for-transducer produces the children of a configuration
7	type: theorem
8	---
9	For every $k$ -pebble transducer there is a for-transducer which inputs the
10	string representation of a configuration and outputs all children of that
11	configuration, as the concatenation of their string representations in order
12	of execution (Lemma D.2.5 of Transducers). It is the composition of Claims
13	D.2.6 and D.2.7: from the configuration to its child configuration graph, and
14	from the graph to the children.
15
16	# Formalization notes
17
18	The book does not state the hypothesis that the stack of the input
19	configuration has fewer than `k` pebbles, but its proof begins with exactly that
20	case distinction ("if `ℓ = k` there is nothing to do"), so the statement
21	carries it; the children are given as a child sequence `ch 0, …, ch m`, and the
22	output is the concatenation of their representations. The input alphabet and
23	the state space are assumed finite.
24	-/
25
26	namespace Lax194892.ChildrenOfConfiguration
27
28	open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding
29	Lax194892.ChildConfigurationGraphs Lax194892.ForTransducers
30
31	/-- A for-transducer maps the representation of a configuration to the
32	concatenation of the representations of its children. -/
33	axiom exists_forTransducer_children {A B Q : Type} [Finite A] [Finite Q] {k : ℕ}
34	(M : Pebble A B Q k) :
35	∃ f : List (ConfLetter A Q k) → List (ConfLetter A Q k), IsForTransducer f ∧
36	∀ (q₀ : Q) (st : List ℕ) (w : List A) (ch : ℕ → Vtx Q) (m : ℕ),
37	(∀ p, p ∈ st → p ≤ w.length) → st.length < k →
38	IsChildSeq M w q₀ st ch m →
39	f (confEnc q₀ st w)
40	= ((List.range (m + 1)).map fun t => confEnc (ch t).1 (st ++ [(ch t).2]) w).flatten
41
42	end Lax194892.ChildrenOfConfiguration
43

Show Proof

Formalization notes

The book does not state the hypothesis that the stack of the input configuration has fewer than $k$ pebbles, but its proof begins with exactly that case distinction ("if $ℓ = k$ there is nothing to do"), so the statement carries it; the children are given as a child sequence $ch 0, …, ch m$ , and the output is the concatenation of their representations. The input alphabet and the state space are 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