Lax916827.SnakeLemma

The snake lemma: the output of a snake graph is a regular function

concepts/Lax916827/SnakeLemma.lean · lax-916827

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✓Lax916827.SnakeLemma

⊢Lax916827Proofs.Results.isRegularFun_snakeOut

In the paper

page 100 of the paper of lax-157538, Transducers

Theorem

Let $C$ be the alphabet representing snake graphs with states $Q$ and output alphabet $B$ . For every $k$ , the function mapping a string $w \in C^*$ to the output of the snake graph it represents, if it represents a snake graph of width at most $k$ , and to $\varepsilon$ otherwise, is regular (Lemma C.2.12 of Transducers, the book's snake lemma). The proof is an induction on the width: a snake of width $k$ visits the record-breaking columns, the ones it reaches for the first time further right than ever before; between two consecutive record-breakers the snake consists of a looping part and a progress part, both of width below $k$ , whose outputs are given by the induction hypothesis on factors cut out by rational functions, and the closure properties of Lemma C.2.10 glue them together.

Lean source view on GitHub

1	import Lax916827.RegularFunctions
2	import Lax916827.SnakeGraphs
3
4	/-!
5	---
6	title: The snake lemma: the output of a snake graph is a regular function
7	type: theorem
8	---
9	Let $C$ be the alphabet representing snake graphs with states $Q$ and output
10	alphabet $B$ . For every $k$ , the function mapping a string $w \in C^*$ to the
11	output of the snake graph it represents, if it represents a snake graph of width
12	at most $k$ , and to $\varepsilon$ otherwise, is regular (Lemma C.2.12 of
13	Transducers, the book's snake lemma). The proof is an induction on the
14	width: a snake of width $k$ visits the record-breaking columns, the ones it
15	reaches for the first time further right than ever before; between two
16	consecutive record-breakers the snake consists of a looping part and a
17	progress part, both of width below $k$ , whose outputs are given by the
18	induction hypothesis on factors cut out by rational functions, and the closure
19	properties of Lemma C.2.10 glue them together.
20
21	# Formalization notes
22
23	The function is `snakeOut k` of `SnakeGraphs`. The lemma is stated for every
24	`k`, not only for `k ∈ {1, …, \|Q\|}`, which is more general and costs nothing:
25	a column has at most `\|Q\|` vertices. The state set and the output alphabet are
26	assumed finite, so that the alphabet `C` is finite. The formal proof carries out
27	the induction for the width-`k` output function of an arbitrary two-way
28	transducer and reads the snake letters through the transducer that walks along a
29	snake graph.
30	-/
31
32	namespace Lax916827.SnakeLemma
33
34	open Lax916827.RegularFunctions Lax916827.SnakeGraphs
35
36	/-- The output of a snake graph of width at most `k`, read off its string
37	representation, is a regular function. -/
38	axiom isRegularFun_snakeOut {Q B : Type} [Finite Q] [Finite B] (k : ℕ) :
39	IsRegularFun (snakeOut (Q := Q) (B := B) k)
40
41	end Lax916827.SnakeLemma
42

Show Proof

Formalization notes

The function is $snakeOut k$ of $SnakeGraphs$ . The lemma is stated for every $k$ , not only for $k ∈ {1, …, |Q|}$ , which is more general and costs nothing: a column has at most $|Q|$ vertices. The state set and the output alphabet are assumed finite, so that the alphabet $C$ is finite. The formal proof carries out the induction for the width- $k$ output function of an arbitrary two-way transducer and reads the snake letters through the transducer that walks along a snake graph.

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