Lax194892.PebbleConfigurationEncoding

String representations of pebble configurations, and balanced runs

concepts/Lax194892/PebbleConfigurationEncoding.lean · lax-194892

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 166 of the paper of lax-157538, Transducers

Definition

Section D.2 of Transducers represents a configuration of a $k$ -pebble transducer on an input $w$ — a state and a stack of at most $k$ gaps of $w$ — as a string with one letter per gap of $w$ , the letter of a gap recording the state, the input letter that follows the gap and the set of pebbles sitting in the gap; the results on reachability speak about a pair of configurations at a time, encoded together. A run between two configurations of height $\ell$ is balanced if the pebble at height $\ell$ is never popped during it, although it may be moved.

Lean source view on GitHub

1	import Lax194892.PebbleTransducers
2
3	/-!
4	---
5	title: String representations of pebble configurations, and balanced runs
6	type: definition
7	---
8	Section D.2 of Transducers represents a configuration of a $k$ -pebble
9	transducer on an input $w$ — a state and a stack of at most $k$ gaps of $w$ — as
10	a string with one letter per gap of $w$ , the letter of a gap recording the
11	state, the input letter that follows the gap and the set of pebbles sitting in
12	the gap; the results on reachability speak about a pair of configurations at
13	a time, encoded together. A run between two configurations of height $\ell$ is
14	balanced if the pebble at height $\ell$ is never popped during it, although
15	it may be moved.
16
17	# Formalization notes
18
19	`pairEnc q₁ q₂ sts stt w` has `w.length + 1` letters, the last one being the
20	only one with no following input letter; `ann k st p` is the set of pebbles of
21	the stack `st` sitting in the gap `p`. `RestrReaches M w ℓ` is reachability
22	along runs all of whose configurations have height at least `ℓ`; with `ℓ = 0` it
23	is ordinary reachability, and for endpoints of height `ℓ` it is the book's
24	balanced run.
25	-/
26
27	namespace Lax194892.PebbleConfigurationEncoding
28
29	open Lax194892.PebbleTransducers
30
31	/-- Reachability along runs whose configurations all have height at least `ℓ`:
32	the topmost `ℓ` pebbles are never popped. -/
33	inductive RestrReaches {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (ℓ : ℕ) :
34	PebbleCfg Q → PebbleCfg Q → Prop
35	/-- The empty run. -/
36	\| refl (q : Q) (st : List ℕ) (h : ℓ ≤ st.length) :
37	RestrReaches M w ℓ (PebbleCfg.conf q st) (PebbleCfg.conf q st)
38	/-- One step from a configuration of height at least `ℓ`. -/
39	\| step {q : Q} {st : List ℕ} {c' c'' : PebbleCfg Q} {o : List B} (h : ℓ ≤ st.length)
40	(hs : M.stepCfg w (PebbleCfg.conf q st) = some (o, c'))
41	(hr : RestrReaches M w ℓ c' c'') :
42	RestrReaches M w ℓ (PebbleCfg.conf q st) c''
43
44	/-- A balanced run between two configurations of height `ℓ`: the pebble at
45	height `ℓ` is never popped. -/
46	def BalancedRun {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (ℓ : ℕ)
47	(c c' : PebbleCfg Q) : Prop :=
48	RestrReaches M w ℓ c c'
49
50	/-- The pebbles of the stack `st` sitting in the gap `p`. -/
51	def ann (k : ℕ) (st : List ℕ) (p : ℕ) : Fin k → Bool := fun i => decide (st[(i : ℕ)]? = some p)
52
53	/-- A letter of the representation of a pair of configurations: the two states, the
54	input letter following the gap, and the pebbles of each configuration in the gap. -/
55	abbrev PairLetter (A Q : Type) (k : ℕ) := Q × Q × Option A × (Fin k → Bool) × (Fin k → Bool)
56
57	/-- The string representation of the pair of configurations `(q₁, sts)` and
58	`(q₂, stt)` of the input `w`: one letter per gap. -/
59	def pairEnc {A Q : Type} {k : ℕ} (q₁ q₂ : Q) (sts stt : List ℕ) (w : List A) :
60	List (PairLetter A Q k) :=
61	(List.range (w.length + 1)).map fun p => (q₁, q₂, w[p]?, ann k sts p, ann k stt p)
62
63	end Lax194892.PebbleConfigurationEncoding
64

Formalization notes

$pairEnc q₁ q₂ sts stt w$ has $w.length + 1$ letters, the last one being the only one with no following input letter; $ann k st p$ is the set of pebbles of the stack $st$ sitting in the gap $p$ . $RestrReaches M w ℓ$ is reachability along runs all of whose configurations have height at least $ℓ$ ; with $ℓ = 0$ it is ordinary reachability, and for endpoints of height $ℓ$ it is the book's balanced run.

Builds on

Lax194892.PebbleTransducers

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