Lax314295.KTypes

The k-type of a string

concepts/Lax314295/KTypes.lean · lax-314295

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 131 of the paper of lax-157538, Transducers

Definition

The $k$ -type of a string (Definition C.4.12 of Transducers) is defined by induction on $k$ : the $0$ -type of every string is the same, and the $(k+1)$ -type of $w$ is the set of triples

\{(\text{$k$-type of } w_1,\; a,\; \text{$k$-type of } w_2) \mid w = w_1\, a\, w_2\}

over all factorisations of $w$ around one of its letters. Two strings have the same $k$ -type if and only if they satisfy the same first-order sentences of quantifier rank at most $k$ (Lemma C.4.13); $k$ -types refine, are a congruence for concatenation and are aperiodic (Lemma C.4.15), which is what makes the first-order definable languages the aperiodic ones (Theorem C.4.11).

Lean source view on GitHub

1	import Mathlib.Data.Set.Basic
2
3	/-!
4	---
5	title: The k-type of a string
6	type: definition
7	---
8	The * $k$ -type* of a string (Definition C.4.12 of Transducers) is defined by
9	induction on $k$ : the $0$ -type of every string is the same, and the
10	$(k+1)$ -type of $w$ is the set of triples
11	$\{(\text{$k$-type of } w_1,\; a,\; \text{$k$-type of } w_2) \mid w = w_1\, a\, w_2\}$
12	over all factorisations of $w$ around one of its letters. Two strings have the
13	same $k$ -type if and only if they satisfy the same first-order sentences of
14	quantifier rank at most $k$ (Lemma C.4.13); $k$ -types refine, are a congruence
15	for concatenation and are aperiodic (Lemma C.4.15), which is what makes the
16	first-order definable languages the aperiodic ones (Theorem C.4.11).
17
18	# Formalization notes
19
20	`TpType A k` is the type of `k`-types, `Unit` for `k = 0` and sets of triples
21	for `k + 1`, and `tp k w` the `k`-type of `w`. Over a finite alphabet there are
22	finitely many `k`-types for every `k`, which is not part of the definition.
23	-/
24
25	namespace Lax314295.KTypes
26
27	/-- The type of `k`-types over the alphabet `A`. -/
28	def TpType (A : Type) : ℕ → Type
29	\| 0 => Unit
30	\| k + 1 => Set (TpType A k × A × TpType A k)
31
32	/-- The `k`-type of a string: trivial for `k = 0`, and for `k + 1` the set of
33	triples `(tp k w₁, a, tp k w₂)` over the factorisations `w = w₁ a w₂`. -/
34	def tp {A : Type} : (k : ℕ) → List A → TpType A k
35	\| 0, _ => ()
36	\| k + 1, w =>
37	{t : TpType A k × A × TpType A k \|
38	∃ (w₁ : List A) (a : A) (w₂ : List A), w = w₁ ++ a :: w₂ ∧ t = (tp k w₁, a, tp k w₂)}
39
40	end Lax314295.KTypes
41

Formalization notes

$TpType A k$ is the type of $k$ -types, $Unit$ for $k = 0$ and sets of triples for $k + 1$ , and $tp k w$ the $k$ -type of $w$ . Over a finite alphabet there are finitely many $k$ -types for every $k$ , which is not part of the definition.

Builds on

none

Used by

From Mathlib

Mathlib.Data.Set.Basic

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