Rational functions

Lax149335.RationalFunctions · concepts/Lax149335/RationalFunctions.lean · lax-149335

definition

Loading review…

Natural Language Statement

Definition

A rational relation $R \subseteq A^* \times B^*$ between strings over alphabets $A$ and $B$ is a subset of the monoid $A^* \times B^*$ defined by a regular expression: the atoms are pairs of strings, and the operations are union, concatenation (componentwise) and Kleene star.

Definition 2.1 (Rational function). A function $f : A^* \to B^*$ is rational if its graph is a rational relation.

Definition 2.3 (Rational functions on types). A function $f : A \to B$ between types is rational if there is a rational function $f' : \mathbb{8}^* \to \mathbb{8}^*$ that agrees with $f$ on the string representations of elements, i.e. the string representation of $f(a)$ is $f'$ applied to the string representation of $a$ .

Concept map

2 concepts; 1 descendant hidden

100%

Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax149335.Types
2	import Mathlib.Data.Set.Defs
3
4	/-!
5	---
6	title: Rational functions
7	type: definition
8	---
9	A rational relation $R \subseteq A^* \times B^*$ between strings over alphabets $A$ and
10	$B$ is a subset of the monoid $A^* \times B^*$ defined by a regular expression: the atoms
11	are pairs of strings, and the operations are union, concatenation (componentwise) and Kleene
12	star.
13
14	Definition 2.1 (Rational function). A function $f : A^* \to B^$ is rational* if its
15	graph is a rational relation.
16
17	Definition 2.3 (Rational functions on types). A function $f : A \to B$ between types is
18	rational if there is a rational function $f' : \mathbb{8}^* \to \mathbb{8}^*$ that agrees
19	with $f$ on the string representations of elements, i.e. the string representation of
20	$f(a)$ is $f'$ applied to the string representation of $a$ .
21	-/
22
23	namespace Lax149335.RationalFunctions
24
25	open Lax149335.Types
26
27	variable {α β : Type}
28
29	/-- Regular expressions over the product monoid `α* × β*`. -/
30	inductive RatExp (α β : Type) : Type
31	\| zero : RatExp α β
32	\| atom : List α → List β → RatExp α β
33	\| plus : RatExp α β → RatExp α β → RatExp α β
34	\| cat : RatExp α β → RatExp α β → RatExp α β
35	\| star : RatExp α β → RatExp α β
36
37	/-- The submonoid of `α* × β*` generated by a set `S`: all finite products of elements of
38	`S`. -/
39	inductive StarSet (S : Set (List α × List β)) : List α × List β → Prop
40	\| nil : StarSet S ([], [])
41	\| cons {x y : List α × List β} : x ∈ S → StarSet S y → StarSet S (x.1 ++ y.1, x.2 ++ y.2)
42
43	/-- The relation defined by a regular expression. -/
44	def RatExp.lang : RatExp α β → Set (List α × List β)
45	\| .zero => ∅
46	\| .atom u v => {(u, v)}
47	\| .plus e f => e.lang ∪ f.lang
48	\| .cat e f => {p \| ∃ x ∈ e.lang, ∃ y ∈ f.lang, p = (x.1 ++ y.1, x.2 ++ y.2)}
49	\| .star e => {p \| StarSet e.lang p}
50
51	/-- A relation between strings is rational if it is defined by a regular expression. -/
52	def IsRationalRel (R : Set (List α × List β)) : Prop := ∃ e : RatExp α β, e.lang = R
53
54	/-- Definition 2.1. A function `f : α* → β*` is rational if its graph is a rational
55	relation. -/
56	def IsRationalFun (f : List α → List β) : Prop :=
57	IsRationalRel {p : List α × List β \| p.2 = f p.1}
58
59	/-- Definition 2.3. A function between types is rational if, on string representations,
60	it is computed by a rational function `𝟖* → 𝟖*`. -/
61	def IsRationalTypeFun {A B : Ty} (f : ⟦A⟧ → ⟦B⟧) : Prop :=
62	∃ f' : List Ty.Sym → List Ty.Sym,
63	IsRationalFun f' ∧ ∀ a : ⟦A⟧, Ty.repr B (f a) = f' (Ty.repr A a)
64
65	end Lax149335.RationalFunctions
66