Regular terms

Lax709149.RegularTerms · concepts/Lax709149/RegularTerms.lean · lax-709149

definition

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A regular term (Definition C.5.3 of Transducers) is an expression built by applying combinators to atomic terms. The atomic terms are the identity A→AA \to A, the projections A×B→AA \times B \to A and A×B→BA \times B \to B, the co-projections A→A+BA \to A + B and B→A+BB \to A + B, distributivity A×(B+C)→(A×B)+(A×C)A \times (B + C) \to (A \times B) + (A \times C), the list constructor 1+A×A∗→A∗\mathbb{1} + A \times A^* \to A^* and deconstructor A∗→1+A×A∗A^* \to \mathbb{1} + A \times A^*, reverse A∗→A∗A^* \to A^*, concatenation A∗∗→A∗A^{**} \to A^*, split (A+B)∗→A∗×(B×A∗)∗(A + B)^* \to A^* \times (B \times A^*)^*, and group prefix multiplication G∗→G∗G^* \to G^* for a group GG whose underlying set is a finite type. The combinators are composition, pairing (f,g):A→B×C(f, g) : A \to B \times C, co-pairing either f g:A+B→C\mathsf{either}\ f\ g : A + B \to C, and map f∗:A∗→B∗f^* : A^* \to B^*. Every regular term defines a type-to-type function; Theorem C.5.4 relates the functions so defined to the regular functions under string representation.

    Concept map
    2 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    Lean source view on GitHub

    1import Mathlib.Algebra.Group.Defs
    2import Mathlib.Data.Finite.Defs
    3import Lax709149.Types
    4
    5/-!
    6---
    7title: Regular terms
    8type: definition
    9---
    10A *regular term* (Definition C.5.3 of *Transducers*) is an expression built by
    11applying combinators to atomic terms. The atomic terms are the identity
    12A→AA \to A, the projections A×B→AA \times B \to A and A×B→BA \times B \to B, the
    13co-projections A→A+BA \to A + B and B→A+BB \to A + B, distributivity
    14A×(B+C)→(A×B)+(A×C)A \times (B + C) \to (A \times B) + (A \times C), the list constructor
    151+A×A∗→A∗\mathbb{1} + A \times A^* \to A^* and deconstructor
    16A∗→1+A×A∗A^* \to \mathbb{1} + A \times A^*, reverse A∗→A∗A^* \to A^*, concatenation
    17A∗∗→A∗A^{**} \to A^*, split (A+B)∗→A∗×(B×A∗)∗(A + B)^* \to A^* \times (B \times A^*)^*, and group
    18prefix multiplication G∗→G∗G^* \to G^* for a group GG whose underlying set is a
    19finite type. The combinators are composition, pairing (f,g):A→B×C(f, g) : A \to B \times C,
    20co-pairing either f g:A+B→C\mathsf{either}\ f\ g : A + B \to C, and map f∗:A∗→B∗f^* : A^* \to B^*.
    21Every regular term defines a type-to-type function; Theorem C.5.4 relates the
    22functions so defined to the regular functions under string representation.
    23
    24# Formalization notes
    25
    26`RegTerm A B` is the syntax, indexed by the source and target types, and
    27`RegTerm.eval` the semantics. Split cuts its input at the entries from `B`, and
    28group prefix multiplication maps a list to its prefix products; its constructor
    29carries the group structure on the elements of `G` and the finiteness of that
    30type, which the book requires and which the regularity of its semantics needs.
    31`IsRegularTermFun f` says that some term evaluates to `f`.
    32-/
    33
    34namespace Lax709149.RegularTerms
    35
    36open Lax709149.Types
    37
    38/-- The prefix products of a list: the `i`-th entry of the output is the product of
    39the first `i` entries of the input. -/
    40def prefixProd {M : Type} [Monoid M] (l : List M) : List M := (l.scanl (· * ·) 1).tail
    41
    42/-- Split: the input is cut at its entries from `B`; the output is the block of
    43entries from `A` before the first cut, and the cutting entries each with the block
    44that follows it. -/
    45def splitList {A B : Type} : List (A ⊕ B) → List A × List (B × List A)
    46 | [] => ([], [])
    47 | Sum.inl a :: l => ((splitList l).1.cons a, (splitList l).2)
    48 | Sum.inr b :: l => ([], (b, (splitList l).1) :: (splitList l).2)
    49
    50/-- The syntax of regular terms: atomic terms and combinators. -/
    51inductive RegTerm : Ty → Ty → Type
    52 /-- Identity `A → A`. -/
    53 | id (A : Ty) : RegTerm A A
    54 /-- First projection `A × B → A`. -/
    55 | fst (A B : Ty) : RegTerm (.prod A B) A
    56 /-- Second projection `A × B → B`. -/
    57 | snd (A B : Ty) : RegTerm (.prod A B) B
    58 /-- Left co-projection `A → A + B`. -/
    59 | inl (A B : Ty) : RegTerm A (.sum A B)
    60 /-- Right co-projection `B → A + B`. -/
    61 | inr (A B : Ty) : RegTerm B (.sum A B)
    62 /-- Distributivity `A × (B + C) → (A × B) + (A × C)`. -/
    63 | distr (A B C : Ty) : RegTerm (.prod A (.sum B C)) (.sum (.prod A B) (.prod A C))
    64 /-- The list constructor `1 + A × A* → A*`. -/
    65 | cons (A : Ty) : RegTerm (.sum .one (.prod A (.list A))) (.list A)
    66 /-- The list deconstructor `A* → 1 + A × A*`. -/
    67 | uncons (A : Ty) : RegTerm (.list A) (.sum .one (.prod A (.list A)))
    68 /-- Reverse `A* → A*`. -/
    69 | reverse (A : Ty) : RegTerm (.list A) (.list A)
    70 /-- Concatenation `A** → A*`. -/
    71 | concat (A : Ty) : RegTerm (.list (.list A)) (.list A)
    72 /-- Split `(A + B)* → A* × (B × A*)*`. -/
    73 | split (A B : Ty) : RegTerm (.list (.sum A B)) (.prod (.list A) (.list (.prod B (.list A))))
    74 /-- Group prefix multiplication `G* → G*`, for a group on a finite type. -/
    75 | pref (G : Ty) (grp : Group G.Elt) (hfin : Finite G.Elt) : RegTerm (.list G) (.list G)
    76 /-- Composition. -/
    77 | comp {A B C : Ty} : RegTerm A B → RegTerm B C → RegTerm A C
    78 /-- Pairing. -/
    79 | pair {A B C : Ty} : RegTerm A B → RegTerm A C → RegTerm A (.prod B C)
    80 /-- Co-pairing. -/
    81 | copair {A B C : Ty} : RegTerm A C → RegTerm B C → RegTerm (.sum A B) C
    82 /-- Map. -/
    83 | map {A B : Ty} : RegTerm A B → RegTerm (.list A) (.list B)
    84
    85/-- The function defined by a regular term. -/
    86def RegTerm.eval : {A B : Ty} → RegTerm A B → A.Elt → B.Elt
    87 | _, _, .id _ => fun x => x
    88 | _, _, .fst _ _ => fun x => x.1
    89 | _, _, .snd _ _ => fun x => x.2
    90 | _, _, .inl _ _ => fun x => Sum.inl x
    91 | _, _, .inr _ _ => fun x => Sum.inr x
    92 | _, _, .distr _ _ _ => fun x =>
    93 Sum.elim (fun b => Sum.inl (x.1, b)) (fun c => Sum.inr (x.1, c)) x.2
    94 | _, _, .cons _ => fun x => Sum.elim (fun _ => []) (fun p => p.1 :: p.2) x
    95 | _, _, .uncons _ => fun l => match l with
    96 | [] => Sum.inl ()
    97 | a :: l' => Sum.inr (a, l')
    98 | _, _, .reverse _ => fun l => l.reverse
    99 | _, _, .concat _ => fun l => l.flatten
    100 | _, _, .split _ _ => fun l => splitList l
    101 | _, _, .pref _ grp _ => fun l => @prefixProd _ (@Group.toDivisionMonoid _ grp).toMonoid l
    102 | _, _, .comp s t => fun x => t.eval (s.eval x)
    103 | _, _, .pair s t => fun x => (s.eval x, t.eval x)
    104 | _, _, .copair s t => fun x => Sum.elim s.eval t.eval x
    105 | _, _, .map t => fun l => l.map t.eval
    106
    107/-- A type-to-type function is defined by a regular term. -/
    108def IsRegularTermFun {A B : Ty} (f : A.Elt → B.Elt) : Prop := ∃ t : RegTerm A B, t.eval = f
    109
    110end Lax709149.RegularTerms
    111
    Formalization notes

    RegTermABRegTerm A B is the syntax, indexed by the source and target types, and RegTerm.evalRegTerm.eval the semantics. Split cuts its input at the entries from BB, and group prefix multiplication maps a list to its prefix products; its constructor carries the group structure on the elements of GG and the finiteness of that type, which the book requires and which the regularity of its semantics needs. IsRegularTermFunfIsRegularTermFun f says that some term evaluates to ff.

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…