Lax765601.CompositionClosure

Closure of a family of functions under composition

concepts/Lax765601/CompositionClosure.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

The transducer classes of the book are described by decomposition into primes: a class is the set of all finite compositions

A_0^* \xrightarrow{f_1} A_1^* \xrightarrow{f_2} \cdots \xrightarrow{f_n} A_n^*

of functions taken from some family of prime functions, with the intermediate alphabets finite. The book writes $P^*$ for this closure of a family $P$ under composition — the Kleene star of the family — as in $\mathrm{Mealy} = (\mathrm{Reversible} \cup \mathrm{Flip\text{-}flop})^*$ , the Krohn–Rhodes theorem (Theorem A.2.2). The same idiom defines the rational functions from their primes (Theorem B.2.6), the regular functions (Definition C.0.1) and the polyregular functions (Definition D.0.1).

Lean source view on GitHub

1	import Mathlib.Data.Finite.Defs
2
3	/-!
4	---
5	title: Closure of a family of functions under composition
6	type: definition
7	---
8	The transducer classes of the book are described by decomposition into primes:
9	a class is the set of all finite compositions
10	$A_0^* \xrightarrow{f_1} A_1^* \xrightarrow{f_2} \cdots \xrightarrow{f_n} A_n^*$
11	of functions taken from some family of prime functions, with the intermediate
12	alphabets finite. The book writes $P^*$ for this closure of a family $P$ under
13	composition — the Kleene star of the family — as in
14	$\mathrm{Mealy} = (\mathrm{Reversible} \cup \mathrm{Flip\text{-}flop})^*$ , the
15	Krohn–Rhodes theorem (Theorem A.2.2). The same idiom defines the rational
16	functions from their primes (Theorem B.2.6), the regular functions (Definition
17	C.0.1) and the polyregular functions (Definition D.0.1).
18
19	# Formalization notes
20
21	A family is a predicate on string-to-string functions indexed by the input and
22	output alphabets, `∀ (A B : Type), (List A → List B) → Prop`. The closure
23	`CompClosure P` is the least family containing `P`, the identity on every
24	alphabet, and closed under composition through a finite intermediate alphabet;
25	that finiteness is the constructor's instance argument `[Finite B]`, so that
26	"composition of primes" never passes through an infinite alphabet. Because the
27	closure is inductively defined, every statement of the form "every composition of
28	primes has property X" is proved by induction on the composition tree, and the
29	theorems of the book about a class defined this way are statements about the
30	closure, not about a syntactic list of factors.
31	-/
32
33	namespace Lax765601.CompositionClosure
34
35	/-- A family of string-to-string functions, indexed by the input and the output
36	alphabet. -/
37	abbrev Family : Type 1 := ∀ (A B : Type), (List A → List B) → Prop
38
39	/-- The closure `P*` of a family `P` under composition: the identity functions, the
40	members of `P`, and the compositions `g ∘ f` of two members of the closure through
41	a finite intermediate alphabet. -/
42	inductive CompClosure (P : Family) : Family
43	/-- A prime function belongs to the closure. -/
44	\| base {A B : Type} {f : List A → List B} : P A B f → CompClosure P A B f
45	/-- The identity on every alphabet belongs to the closure. -/
46	\| protected id (A : Type) : CompClosure P A A _root_.id
47	/-- The closure is closed under composition through a finite alphabet. -/
48	\| comp {A B C : Type} [Finite B] {f : List A → List B} {g : List B → List C} :
49	CompClosure P A B f → CompClosure P B C g → CompClosure P A C (g ∘ f)
50
51	/-- The union of two families. -/
52	def FamUnion (P Q : Family) : Family := fun A B f => P A B f ∨ Q A B f
53
54	end Lax765601.CompositionClosure
55

Formalization notes

A family is a predicate on string-to-string functions indexed by the input and output alphabets, $∀ (A B : Type), (List A → List B) → Prop$ . The closure $CompClosure P$ is the least family containing $P$ , the identity on every alphabet, and closed under composition through a finite intermediate alphabet; that finiteness is the constructor's instance argument $[Finite B]$ , so that "composition of primes" never passes through an infinite alphabet. Because the closure is inductively defined, every statement of the form "every composition of primes has property X" is proved by induction on the composition tree, and the theorems of the book about a class defined this way are statements about the closure, not about a syntactic list of factors.

Builds on

none

Used by

From Mathlib

Mathlib.Data.Finite.Defs

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

Closure of a family of functions under composition

Flags

Flag this concept