Lax765601.Continuity

Continuous string-to-string functions

concepts/Lax765601/Continuity.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 5 of the paper of lax-157538, Transducers

Definition

A function $f : A^* \to B^*$ between the sets of strings over two alphabets is continuous if for every regular language $L \subseteq B^*$ over the output alphabet, the inverse image $f^{-1}(L)$ is a regular language over the input alphabet (Definition 0.1 of Transducers). Continuity is the compatibility with regular languages that every transducer model of the book is required to have: for functions with two possible outputs it is exactly regularity of a language, and composing a continuous function with a regular language, seen as a string-to-Boolean function, gives a regular language again.

The same requirement makes sense for a relation $R \subseteq A^* \times B^*$ and for a partial function: the set of input strings that are related to (respectively, mapped to) some string of $L$ has to be regular. The relational form is the one Part B proves for rational relations, and the partial form the one it proves for subsequential functions.

Lean source view on GitHub

1	import Mathlib.Computability.DFA
2
3	/-!
4	---
5	title: Continuous string-to-string functions
6	type: definition
7	---
8	A function $f : A^* \to B^*$ between the sets of strings over two alphabets is
9	continuous if for every regular language $L \subseteq B^*$ over the output
10	alphabet, the inverse image $f^{-1}(L)$ is a regular language over the input
11	alphabet (Definition 0.1 of Transducers). Continuity is the compatibility with
12	regular languages that every transducer model of the book is required to have:
13	for functions with two possible outputs it is exactly regularity of a language,
14	and composing a continuous function with a regular language, seen as a
15	string-to-Boolean function, gives a regular language again.
16
17	The same requirement makes sense for a relation $R \subseteq A^* \times B^*$ and
18	for a partial function: the set of input strings that are related to (respectively,
19	mapped to) some string of $L$ has to be regular. The relational form is the one
20	Part B proves for rational relations, and the partial form the one it proves for
21	subsequential functions.
22
23	# Formalization notes
24
25	Strings over an alphabet `A` are `List A`, languages are mathlib's `Language A`
26	(a set of strings), and regularity is mathlib's `Language.IsRegular`: recognition
27	by a deterministic finite automaton with a finite state set. This dictionary is
28	used by every concept of the book and is not repeated.
29
30	Alphabets are arbitrary types here. The finiteness of the alphabets, which the
31	book assumes throughout, is an instance hypothesis `[Finite A]` on the statements
32	that need it, so that a definition never carries a hypothesis it does not use. A
33	partial function is a function into `Option (List B)`, with `none` for
34	"undefined".
35	-/
36
37	namespace Lax765601.Continuity
38
39	/-- A string-to-string function is continuous if the inverse image of every
40	regular language over the output alphabet is a regular language. -/
41	def Continuous {A B : Type} (f : List A → List B) : Prop :=
42	∀ L : Language B, L.IsRegular → Language.IsRegular ({w : List A \| f w ∈ L} : Language A)
43
44	/-- A relation `R ⊆ A* × B*` is continuous if, for every regular language `L` over
45	the output alphabet, the set of input strings related to some string of `L` is
46	regular. -/
47	def RelContinuous {A B : Type} (R : List A → List B → Prop) : Prop :=
48	∀ L : Language B, L.IsRegular →
49	Language.IsRegular ({w : List A \| ∃ v, R w v ∧ v ∈ L} : Language A)
50
51	/-- A partial function is continuous if, for every regular language `L` over the
52	output alphabet, the set of input strings whose output is defined and belongs to
53	`L` is regular. -/
54	def PartialContinuous {A B : Type} (f : List A → Option (List B)) : Prop :=
55	∀ L : Language B, L.IsRegular →
56	Language.IsRegular ({w : List A \| ∃ v, f w = some v ∧ v ∈ L} : Language A)
57
58	end Lax765601.Continuity
59

Formalization notes

Strings over an alphabet $A$ are $List A$ , languages are mathlib's $Language A$ (a set of strings), and regularity is mathlib's $Language.IsRegular$ : recognition by a deterministic finite automaton with a finite state set. This dictionary is used by every concept of the book and is not repeated.

Alphabets are arbitrary types here. The finiteness of the alphabets, which the book assumes throughout, is an instance hypothesis $[Finite A]$ on the statements that need it, so that a definition never carries a hypothesis it does not use. A partial function is a function into $Option (List B)$ , with $none$ for "undefined".

Builds on

none

Used by

From Mathlib

Mathlib.Computability.DFA

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