-
def
Lax765601.Continuitypp. 5–6Continuous string-to-string functions
A function between the sets of strings over two alphabets is continuous if for every regular language over the output alphabet, the inverse image 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 and for a partial function: the set of input strings that are related to (respectively, mapped to) some string of 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.
1 import Mathlib.Computability.DFA 2 … module docstring, 33 lines 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 -
Transducers, Part A: Mealy Machines
-
def
Lax765601.PrimeMealyMachinesp. 20Prime Mealy machines: reversible and flip-flop
The prime Mealy machines are defined in terms of the state transformations of their letters (Definition A.2.1 of Transducers). There are two kinds.
- Reversible machines: the state transformation of every letter is a permutation of the state space.
- Flip-flop machines: the state transformation of every letter is either the identity or a constant, all states being mapped to the same one.
A one-state machine is both. The machine outputting on is reversible; the delay machine, which shifts the input one position to the right, is a flip-flop. Since composing permutations gives a permutation and composing constants gives a constant, nothing changes if the definition is phrased for the state transformations of input strings rather than of letters.
The Krohn–Rhodes theorem (Theorem A.2.2) says that every Mealy machine is a composition of prime Mealy machines; Theorem A.2.8 characterises the compositions of flip-flops alone.
1 import Mathlib.Logic.Function.Defs 2 import Lax765601.MealyMachine 3 import Lax765601.CompositionClosure 4 … module docstring, 32 lines 37 38 namespace Lax765601.PrimeMealyMachines 39 40 open Lax765601.MealyMachine Lax765601.CompositionClosure 41 42 /-- A Mealy machine is reversible if the state transformation of every letter is a 43 permutation of the state space. -/ 44 def Reversible {A B Q : Type} (M : Mealy A B Q) : Prop := 45 ∀ a : A, Function.Bijective (M.letterTrans a) 46 47 /-- A Mealy machine is a flip-flop if the state transformation of every letter is 48 the identity or a constant. -/ 49 def FlipFlop {A B Q : Type} (M : Mealy A B Q) : Prop := 50 ∀ a : A, M.letterTrans a = id ∨ ∃ q₀ : Q, ∀ q : Q, M.letterTrans a q = q₀ 51 52 /-- A function is computed by a reversible Mealy machine with a finite state 53 space. -/ 54 def IsReversibleMealy {A B : Type} (f : List A → List B) : Prop := 55 ∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ Reversible M 56 57 /-- A function is computed by a flip-flop Mealy machine with a finite state 58 space. -/ 59 def IsFlipFlopMealy {A B : Type} (f : List A → List B) : Prop := 60 ∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ FlipFlop M 61 62 /-- The family of prime Mealy machines: the functions computed by a reversible or 63 by a flip-flop machine. -/ 64 def PrimeMealyFam : Family := fun _ _ f => IsReversibleMealy f ∨ IsFlipFlopMealy f 65 66 /-- The family of flip-flop Mealy machines. -/ 67 def FlipFlopFam : Family := fun _ _ f => IsFlipFlopMealy f 68 69 end Lax765601.PrimeMealyMachines 70 -
thm✓
Lax765601.KrohnRhodespp. 20–21The Krohn–Rhodes decomposition theorem
Every Mealy machine admits a decomposition
in which each Mealy machine is either reversible or flip-flop (Theorem A.2.2 of Transducers, the Krohn–Rhodes theorem). No uniqueness is claimed. Since Mealy machines are closed under composition, the class of functions computed by Mealy machines is exactly the closure under composition of the prime Mealy machines,
The proof of the book has two steps: map lifting is compatible with decompositions into primes (Lemma A.2.4), and the state transformation transducer of every pre-automaton is a composition of primes (Lemma A.2.5), by an induction on the number of states and the number of letters whose state transformation is not a permutation; the output of the machine is then recovered from the state transformations of the prefixes by a delay machine and a letter-to-letter homomorphism.
1 import Lax765601.PrimeMealyMachines 2 … module docstring, 32 lines 35 36 namespace Lax765601.KrohnRhodes 37 38 open Lax765601.MealyMachine Lax765601.CompositionClosure Lax765601.PrimeMealyMachines 39 40 /-- Every function computed by a Mealy machine is a composition of reversible and 41 flip-flop Mealy machines. -/ 42 axiom compClosure_primeMealy_of_isMealy {A B : Type} [Finite A] [Finite B] 43 {f : List A → List B} (hf : IsMealy f) : CompClosure PrimeMealyFam A B f 44 45 end Lax765601.KrohnRhodes 46 -
def
Lax765601.MapLiftingp. 21Map lifting
Let be a string-to-string function. Its map lifting (Definition A.2.3 of Transducers) is the function
over the alphabets extended by a fresh separator letter , which applies to every block of the input delimited by the separator:
where the strings do not use the separator. The map lifting is the construction by which a transducer is applied to a list of input strings in parallel; it is used many times in the book, first in the proof of the Krohn–Rhodes theorem (Lemma A.2.4), and the prime regular functions of Part C are map liftings.
1 import Mathlib.Data.List.Basic 2 … module docstring, 28 lines 31 32 namespace Lax765601.MapLifting 33 34 /-- Cut a string over `A + 1` (the separator being `none`) into its maximal blocks 35 without the separator; there is always one block more than there are separators. 36 -/ 37 def splitSep {A : Type} : List (Option A) → List (List A) 38 | [] => [[]] 39 | none :: w => [] :: splitSep w 40 | some a :: w => 41 match splitSep w with 42 | [] => [[a]] 43 | u :: us => (a :: u) :: us 44 45 /-- The map lifting of `f`: apply `f` to every block delimited by the separator, 46 `w₁ # ⋯ # wₙ ↦ f w₁ # ⋯ # f wₙ`. -/ 47 def mapLift {A B : Type} (f : List A → List B) (w : List (Option A)) : List (Option B) := 48 List.intercalate [none] ((splitSep w).map (fun u => (f u).map some)) 49 50 end Lax765601.MapLifting 51 -
thm✓
Lax765601.MapLiftingDecompositionp. 21Map lifting preserves decompositions into primes
If a Mealy machine decomposes into prime Mealy machines, then so does its map lifting (Lemma A.2.4 of Transducers). Since map lifting commutes with composition, it suffices to lift a single prime. A flip-flop is lifted by resetting its state at every separator. A reversible machine needs more care, because resetting would break reversibility: the book computes, by a reversible machine, the state transformation of every prefix in the variant where the separator does nothing, stores the value at the last separator by a flip-flop delay machine, and recovers the state transformation of the current block by the cancellation law , all of which is a one-state machine's work.
1 import Lax765601.PrimeMealyMachines 2 import Lax765601.MapLifting 3 … module docstring, 23 lines 27 28 namespace Lax765601.MapLiftingDecomposition 29 30 open Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax765601.MapLifting 31 32 /-- The map lifting of a composition of prime Mealy machines is a composition of 33 prime Mealy machines. -/ 34 axiom compClosure_mapLift {A B : Type} [Finite A] {f : List A → List B} 35 (hf : CompClosure PrimeMealyFam A B f) : 36 CompClosure PrimeMealyFam (Option A) (Option B) (mapLift f) 37 38 end Lax765601.MapLiftingDecomposition 39 -
⊢
Lax765601Proofs.Results.compClosure_mapLiftpp. 21–23no assumptions
Map lifting preserves decompositions into primes (Lemma A.2.4): the source proves it for a single prime — a flip-flop is reset at the separator, a reversible machine goes through the cancellation law of the book — and extends it along the composition tree.
-
The state transformation transducer is a composition of primes
For every pre-automaton, its state transformation transducer — the Mealy machine whose -th output letter is the state transformation of the first input letters — is a composition of prime Mealy machines (Lemma A.2.5 of Transducers, the main lemma in the proof of the Krohn–Rhodes theorem).
The book proves it by induction on the number of states and, for a tie, on the number of letters whose state transformation is not a permutation. A pre-automaton all of whose letters are permutations is reversible as it stands. Otherwise one fixes a letter whose state transformation has a proper image , decomposes the input into its first -block, the middle -blocks and the -free suffix, and computes the three state transformations in five stages: the map lifting of the induction hypothesis for the alphabet without (Lemma A.2.4) handles the -free pieces, two flip-flops distribute the state transformations of the blocks, the induction hypothesis for the smaller state space handles the middle part, and a letter-to-letter homomorphism assembles the result.
1 import Lax765601.PrimeMealyMachines 2 import Lax765601.StateTransformations 3 … module docstring, 33 lines 37 38 namespace Lax765601.StateTransformationDecomposition 39 40 open Lax765601.MealyMachine Lax765601.CompositionClosure Lax765601.PrimeMealyMachines 41 Lax765601.StateTransformations 42 43 /-- The state transformation transducer of a finite pre-automaton over a finite 44 alphabet is a composition of prime Mealy machines. -/ 45 axiom compClosure_stateTransTransducer {A Q : Type} [Finite A] [Finite Q] (δ : Q → A → Q) : 46 CompClosure PrimeMealyFam A (Q → Q) (stateTransTransducer δ).eval 47 48 end Lax765601.StateTransformationDecomposition 49 -
thm✓
Lax765601.ReversibleCompositionp. 27Reversible Mealy machines are closed under composition
The composition of two functions computed by reversible Mealy machines is computed by a reversible Mealy machine (Lemma A.2.6 of Transducers). Hence the class of compositions of reversible machines is just the class of reversible machines: the product machine of the composition (Theorem A.1.3) is reversible, since the state transformation of a letter in it is a permutation in each coordinate.
1 import Lax765601.PrimeMealyMachines 2 … module docstring, 17 lines 20 21 namespace Lax765601.ReversibleComposition 22 23 open Lax765601.PrimeMealyMachines 24 25 /-- The composition of two reversible Mealy machines is a reversible Mealy 26 machine. -/ 27 axiom isReversibleMealy_comp {A B C : Type} [Finite B] 28 {f : List A → List B} {g : List B → List C} 29 (hf : IsReversibleMealy f) (hg : IsReversibleMealy g) : IsReversibleMealy (g ∘ f) 30 31 end Lax765601.ReversibleComposition 32 -
def
Lax765601.Aperiodicityp. 27Aperiodic string-to-string functions
A length preserving string-to-string function is aperiodic (Definition A.2.7 of Transducers) if for all input strings the last letter of
is the same for all sufficiently large . Aperiodicity says that the function cannot have periodic behaviour: the function on whose last output letter says whether the input has length at least two is aperiodic, while the one whose last letter gives the parity of the length is not. By the arbitrary choice of , the last output letters are eventually fixed as well, for every . Theorem A.2.8 shows that the aperiodic functions computed by Mealy machines are exactly the compositions of flip-flop machines.
1 import Mathlib.Data.List.Basic 2 … module docstring, 29 lines 32 33 namespace Lax765601.Aperiodicity 34 35 /-- The `n`-fold concatenation `vⁿ` of a string with itself. -/ 36 def npow {A : Type} (v : List A) : ℕ → List A 37 | 0 => [] 38 | n + 1 => v ++ npow v n 39 40 /-- A string-to-string function is aperiodic if for all input strings `u, v, w` the 41 last letter of `f (u vⁿ w)` — as an element of `Option B`, so that "no letter" is 42 an admissible value — is the same for all sufficiently large `n`. -/ 43 def Aperiodic {A B : Type} (f : List A → List B) : Prop := 44 ∀ u v w : List A, ∃ o : Option B, ∃ N : ℕ, ∀ n ≥ N, (f (u ++ npow v n ++ w)).getLast? = o 45 46 end Lax765601.Aperiodicity 47 -
thm✓
Lax765601.AperiodicMealyp. 28Aperiodic Mealy machines are exactly the compositions of flip-flops
A function computed by a Mealy machine is aperiodic if and only if it is computed by a composition of flip-flop Mealy machines (Theorem A.2.8 of Transducers). This answers the question what the class of compositions of one kind of prime is; for the other kind, is the class of reversible machines (Lemma A.2.6).
The two implications are separate results, each with its own proof: (a composition of flip-flops is aperiodic) and (an aperiodic Mealy function decomposes into flip-flops); this statement is their conjunction.
1 import Lax765601.PrimeMealyMachines 2 import Lax765601.Aperiodicity 3 … module docstring, 26 lines 30 31 namespace Lax765601.AperiodicMealy 32 33 open Lax765601.MealyMachine Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax765601.Aperiodicity 34 35 /-- A function computed by a Mealy machine is aperiodic if and only if it is a 36 composition of flip-flop Mealy machines. -/ 37 axiom aperiodic_iff_compClosure_flipFlop {A B : Type} [Finite A] [Finite B] 38 {f : List A → List B} (hf : IsMealy f) : 39 Aperiodic f ↔ CompClosure FlipFlopFam A B f 40 41 end Lax765601.AperiodicMealy 42 -
thm✓
Lax765601.FlipFlopsOfAperiodicp. 28Aperiodic Mealy machines are compositions of flip-flops
Every aperiodic function computed by a Mealy machine is computed by a composition of flip-flop Mealy machines: the implication "aperiodic composition of flip-flops" of Theorem A.2.8 of Transducers, the hard half. By Lemma A.2.11 the function is computed by a machine whose state transformations satisfy the stabilisation condition (); the proof of the Krohn–Rhodes theorem is then run for this machine, and every machine arising in the induction inherits (), since it only uses state transformations of the original one, so that no reversible machine with more than one state ever appears and every prime in the decomposition is a flip-flop.
1 import Lax765601.PrimeMealyMachines 2 import Lax765601.Aperiodicity 3 … module docstring, 21 lines 25 26 namespace Lax765601.FlipFlopsOfAperiodic 27 28 open Lax765601.MealyMachine Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax765601.Aperiodicity 29 30 /-- An aperiodic function computed by a Mealy machine is a composition of flip-flop 31 Mealy machines. -/ 32 axiom compClosure_flipFlop_of_aperiodic {A B : Type} [Finite A] [Finite B] 33 {f : List A → List B} (hf : IsMealy f) (ha : Aperiodic f) : 34 CompClosure FlipFlopFam A B f 35 36 end Lax765601.FlipFlopsOfAperiodic 37 -
thm✓
Lax765601.AperiodicOfFlipFlopsp. 28Compositions of flip-flop machines are aperiodic
Every composition of flip-flop Mealy machines computes an aperiodic function: the implication "composition of flip-flops aperiodic" of Theorem A.2.8 of Transducers. A single flip-flop is aperiodic, because the last letter of depends only on the last letter read and on the last letter of whose state transformation is a constant, neither of which depends on ; and aperiodicity is preserved by composition, by the pumping form of aperiodicity (Claim A.2.9), in which the shifts of the two functions add up.
1 import Lax765601.PrimeMealyMachines 2 import Lax765601.Aperiodicity 3 … module docstring, 20 lines 24 25 namespace Lax765601.AperiodicOfFlipFlops 26 27 open Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax765601.Aperiodicity 28 29 /-- A composition of flip-flop Mealy machines is aperiodic. -/ 30 axiom aperiodic_of_compClosure_flipFlop {A B : Type} {f : List A → List B} 31 (hf : CompClosure FlipFlopFam A B f) : Aperiodic f 32 33 end Lax765601.AperiodicOfFlipFlops 34 -
Theorem A.2.8 as a biconditional, glued from its two halves: the statements and are its assumptions.
-
thm✓
Lax765601.AperiodicPumpingp. 28Aperiodicity as a pumping property
A function computed by a Mealy machine is aperiodic if and only if for all input strings there are output strings and a number such that
(Claim A.2.9 of Transducers). The right-to-left direction is immediate, since the last letter of does not depend on . For the other direction, aperiodicity fixes the last letters of for large , so that from some point on the output ends with repetitions of a fixed string of length , and fixes the last letters of , which gives . The pumping form is what makes aperiodicity compatible with composition: the shift of is the sum of the shifts of and .
1 import Lax765601.MealyMachine 2 import Lax765601.Aperiodicity 3 … module docstring, 23 lines 27 28 namespace Lax765601.AperiodicPumping 29 30 open Lax765601.MealyMachine Lax765601.Aperiodicity 31 32 /-- A Mealy function is aperiodic if and only if it has the pumping property: for 33 all `u, v, w` there are `x, y, z` and `k` with `f (u v^(n+k) w) = x yⁿ z` for all 34 `n > 0`. -/ 35 axiom aperiodic_iff_pumping {A B : Type} {f : List A → List B} (hf : IsMealy f) : 36 Aperiodic f ↔ 37 ∀ u v w : List A, ∃ (x y z : List B) (k : ℕ), ∀ n > 0, 38 f (u ++ npow v (n + k) ++ w) = x ++ npow y n ++ z 39 40 end Lax765601.AperiodicPumping 41 -
no assumptions
Aperiodicity of a Mealy function is the pumping property of Claim A.2.9. The source proves the pumping property from the stabilisation condition of Lemma A.2.11 () and the converse directly.
-
thm✓
Lax765601.MealyDerivativesp. 29Myhill–Nerode for Mealy machines
A string-to-string function is computed by a Mealy machine if and only if (1) it has finitely many derivatives, (2) it is letter-to-letter, and (3) its -th output letter depends only on the first input letters (Lemma A.2.10 of Transducers). From a machine, the derivative is determined by the state reached after reading , so there are finitely many. Conversely, the minimal machine of has the derivatives as its states, the derivative of the empty string as initial state, and the transitions
which are well defined because the output letter and the target depend only on the derivative and not on .
1 import Mathlib.Data.Set.Finite.Basic 2 import Lax765601.MealyMachine 3 import Lax765601.ElementaryProperties 4 import Lax765601.Derivatives 5 … module docstring, 25 lines 31 32 namespace Lax765601.MealyDerivatives 33 34 open Lax765601.MealyMachine Lax765601.ElementaryProperties Lax765601.Derivatives 35 36 /-- A function is computed by a Mealy machine if and only if it has finitely many 37 derivatives, is letter-to-letter, and its first `n` output letters depend only on 38 its first `n` input letters. -/ 39 axiom isMealy_iff {A B : Type} (f : List A → List B) : 40 IsMealy f ↔ (Set.range (deriv f)).Finite ∧ LengthPreserving f ∧ PrefixDetermined f 41 42 end Lax765601.MealyDerivatives 43 -
def
Lax765601.Derivativesp. 29Derivatives of a string-to-string function
A derivative of a length preserving string-to-string function is a function of the form
for some input string (Section A.2.3 of Transducers). The derivative is the output that still produces after having read ; for a function computed by a Mealy machine it is determined by the state reached after reading , which is the observation behind the Myhill–Nerode lemma for Mealy machines (Lemma A.2.10): a function is computed by a Mealy machine if and only if it is letter-to-letter, its -th output letter depends only on the first input letters, and it has finitely many derivatives. The minimal Mealy machine of such a function has the derivatives as its states.
1 import Mathlib.Data.List.Basic 2 … module docstring, 26 lines 29 30 namespace Lax765601.Derivatives 31 32 /-- The derivative `f(w_)` of `f`: the output `f` produces after having read `w`, 33 namely `v ↦ f (w v)` with the first `|w|` letters of the output removed. -/ 34 def deriv {A B : Type} (f : List A → List B) (w : List A) : List A → List B := 35 fun v => (f (w ++ v)).drop w.length 36 37 end Lax765601.Derivatives 38 -
no assumptions
The Myhill–Nerode lemma for Mealy machines (Lemma A.2.10). From a machine, the derivative after is the run from the state reached after ; conversely the source builds the minimal machine on the finitely many derivatives, its transition from on outputting the first letter of and moving to .
-
thm✓
Lax765601.AperiodicityMinimalMachinep. 29Aperiodicity through the state transformations of the minimal machine
A function computed by a Mealy machine is aperiodic if and only if its minimal Mealy machine satisfies the stabilisation condition (): for every state transformation that arises from some input string, the sequence eventually stabilises on a single state transformation (Lemma A.2.11 of Transducers). If any machine computing satisfies (), then is aperiodic; conversely, if the minimal machine violates (*) for the state transformation of a string , then two powers recur infinitely often, and minimality yields strings for which the last letters of and differ, contradicting aperiodicity. This lemma is what the book's decision procedure for aperiodicity rests on.
1 import Lax765601.MealyMachine 2 import Lax765601.StateTransformations 3 import Lax765601.Aperiodicity 4 … module docstring, 26 lines 31 32 namespace Lax765601.AperiodicityMinimalMachine 33 34 open Lax765601.MealyMachine Lax765601.StateTransformations Lax765601.Aperiodicity 35 36 /-- A Mealy function is aperiodic if and only if some Mealy machine computing it 37 satisfies the stabilisation condition (*) on its state transformations. -/ 38 axiom aperiodic_iff_transAperiodic {A B : Type} {f : List A → List B} (hf : IsMealy f) : 39 Aperiodic f ↔ 40 ∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f ∧ TransAperiodic M.transFun 41 42 end Lax765601.AperiodicityMinimalMachine 43 -
no assumptions
A Mealy function is aperiodic if and only if some machine computing it satisfies the stabilisation condition () (Lemma A.2.11). The source constructs the minimal machine on the derivatives and shows that aperiodicity makes its state transformations stabilise; conversely () gives the pumping property.
-
def
Lax765601.MealyMachinep. 13Mealy machines
A Mealy machine is a deterministic finite automaton whose transitions are labelled by output letters, and which has no accepting states, since its purpose is to produce an output string rather than to accept or reject. Formally (Definition A.1.1 of Transducers), it consists of an input alphabet , an output alphabet , a state space , an initial state and a transition function
Its semantics is the function obtained by running the underlying automaton on the input string and labelling each position by the output letter of the corresponding transition; it is a letter-to-letter function, the output having the same length as the input. A function is computed by a Mealy machine if it is the semantics of a Mealy machine with a finite state space.
The state transformation of an input letter is the map describing how reading updates the state, the output being ignored; the underlying pre-automaton of the machine is the family of these maps, i.e. a deterministic automaton without initial and accepting states (Section A.2).
1 import Mathlib.Data.Finite.Defs 2 … module docstring, 38 lines 41 42 namespace Lax765601.MealyMachine 43 44 /-- A Mealy machine with input alphabet `A`, output alphabet `B` and state space 45 `Q`: an initial state and a transition function `Q × A → Q × B`. -/ 46 structure Mealy (A B Q : Type) where 47 /-- The initial state. -/ 48 init : Q 49 /-- The transition function: a source state and an input letter determine a 50 target state and an output letter. -/ 51 step : Q → A → Q × B 52 53 namespace Mealy 54 55 variable {A B Q : Type} 56 57 /-- The output produced by the machine on an input string, when started in a 58 given state. -/ 59 def run (M : Mealy A B Q) : Q → List A → List B 60 | _, [] => [] 61 | q, a :: w => (M.step q a).2 :: M.run (M.step q a).1 w 62 63 /-- The semantics of a Mealy machine: the output produced from the initial state. 64 -/ 65 def eval (M : Mealy A B Q) (w : List A) : List B := M.run M.init w 66 67 /-- The state transformation of an input letter: how reading the letter updates 68 the state. -/ 69 def letterTrans (M : Mealy A B Q) (a : A) : Q → Q := fun q => (M.step q a).1 70 71 /-- The underlying pre-automaton: the transition function with the output letters 72 forgotten. -/ 73 def transFun (M : Mealy A B Q) : Q → A → Q := fun q a => (M.step q a).1 74 75 end Mealy 76 77 /-- A string-to-string function is computed by a Mealy machine if it is the 78 semantics of a Mealy machine with a finite state space. -/ 79 def IsMealy {A B : Type} (f : List A → List B) : Prop := 80 ∃ (Q : Type) (_ : Finite Q) (M : Mealy A B Q), M.eval = f 81 82 end Lax765601.MealyMachine 83 -
thm✓
Lax765601.MealyEquivalenceBoundp. 14Decidable equivalence of Mealy machines
The equivalence problem for Mealy machines — do two given machines compute the same function? — is decidable (Theorem A.1.2 of Transducers). The book reduces it to the equivalence of regular languages: a letter-to-letter function is determined by the languages "the last output letter is ", one for each output letter , and each of them is recognised by the automaton underlying the machine. In the form stated here, two Mealy machines with and states are equivalent if and only if they agree on all input strings of length at most — a finite check, since the alphabet is finite.
1 import Mathlib.SetTheory.Cardinal.Finite 2 import Lax765601.MealyMachine 3 … module docstring, 24 lines 28 29 namespace Lax765601.MealyEquivalenceBound 30 31 open Lax765601.MealyMachine 32 33 /-- Two Mealy machines are equivalent if and only if they agree on every input 34 string of length at most the product of their numbers of states. -/ 35 axiom eval_eq_iff_short {A B Q₁ Q₂ : Type} [Finite Q₁] [Finite Q₂] 36 (M : Mealy A B Q₁) (N : Mealy A B Q₂) : 37 M.eval = N.eval ↔ 38 ∀ w : List A, w.length ≤ Nat.card Q₁ * Nat.card Q₂ → M.eval w = N.eval w 39 40 end Lax765601.MealyEquivalenceBound 41 -
⊢
Lax765601Proofs.Results.eval_eq_iff_shortpp. 14–15no assumptions
Two Mealy machines are equivalent if and only if they agree on all inputs of length at most the product of their numbers of states (Theorem A.1.2).
-
thm✓
Lax765601.MealyCompositionp. 15Mealy machines are closed under composition
If and are computed by Mealy machines, then so is their composition (Theorem A.1.3 of Transducers). The proof is a product construction: the composed machine runs both machines in lockstep, feeding each output letter of the first to the second, so its state space is the product of the two state spaces.
1 import Lax765601.MealyMachine 2 … module docstring, 18 lines 21 22 namespace Lax765601.MealyComposition 23 24 open Lax765601.MealyMachine 25 26 /-- The composition of two functions computed by Mealy machines is computed by a 27 Mealy machine. -/ 28 axiom isMealy_comp {A B C : Type} [Finite B] {f : List A → List B} {g : List B → List C} 29 (hf : IsMealy f) (hg : IsMealy g) : IsMealy (g ∘ f) 30 31 end Lax765601.MealyComposition 32 -
⊢
Lax765601Proofs.Results.isMealy_comppp. 15–16no assumptions
Mealy machines are closed under composition (Theorem A.1.3), by the product construction of the source, transported through .
-
thm✓
Lax765601.MealyContinuityp. 16Mealy machines are continuous
Every function computed by a Mealy machine is continuous: the inverse image of a regular language under it is regular (Theorem A.1.4 of Transducers). The book derives this from closure under composition through the letter-to-letter lifting of a language, which labels every position of a string by whether the prefix ending there belongs to the language; a direct product construction works just as well, and is the one formalised.
1 import Lax765601.Continuity 2 import Lax765601.MealyMachine 3 … module docstring, 18 lines 22 23 namespace Lax765601.MealyContinuity 24 25 open Lax765601.Continuity Lax765601.MealyMachine 26 27 /-- A function computed by a Mealy machine is continuous. -/ 28 axiom continuous_of_isMealy {A B : Type} [Finite A] [Finite B] {f : List A → List B} 29 (hf : IsMealy f) : Continuous f 30 31 end Lax765601.MealyContinuity 32 -
no assumptions
Mealy machines are continuous (Theorem A.1.4): the product of the machine with a deterministic automaton for the output language recognises the inverse image ( in the source).
-
Transducers, Part B: Rational Functions
-
thm✓
Lax132576.MealyMachineIndependentp. 66Machine-independent characterisation of Mealy machines
A function is computed by a Mealy machine if and only if it is (a) continuous, (b) prefix preserving, and (c) length preserving (Theorem B.4.1 of Transducers). A Mealy machine clearly has the three properties; conversely, for every output letter the language of inputs whose output ends with is regular by continuity, each input position contributes exactly one output letter by prefix and length preservation, and the product of the automata of these languages is the state space of a Mealy machine computing .
1 import Lax765601.Continuity 2 import Lax765601.ElementaryProperties 3 import Lax765601.MealyMachine 4 … module docstring, 20 lines 25 26 namespace Lax132576.MealyMachineIndependent 27 28 open Lax765601.Continuity Lax765601.ElementaryProperties Lax765601.MealyMachine 29 30 /-- A function is computed by a Mealy machine if and only if it is continuous, 31 prefix preserving and length preserving. -/ 32 axiom isMealy_iff {A B : Type} [Finite A] [Finite B] (f : List A → List B) : 33 IsMealy f ↔ Continuous f ∧ PrefixPreserving f ∧ LengthPreserving f 34 35 end Lax132576.MealyMachineIndependent 36 -
def
Lax765601.ElementaryPropertiesp. 66Prefix preservation and length preservation
Three elementary properties of a string-to-string function that the characterisation theorems of the book are stated with.
- is prefix preserving if implies , where is the prefix order on strings.
- is length preserving, or letter-to-letter, if for every input string .
- is prefix determined if the first output letters depend only on the first input letters: input strings that agree on their first letters have outputs that agree on their first letters.
For a letter-to-letter function, being prefix determined says exactly that the -th output letter depends only on the first input letters, which is condition (3) of the Myhill–Nerode lemma for Mealy machines (Lemma A.2.10), and it is the determinism condition of Theorem B.2.7; prefix preservation and length preservation together are the shape of the machine-independent characterisation of Mealy machines (Theorem B.4.1).
1 import Mathlib.Data.List.Infix 2 … module docstring, 28 lines 31 32 namespace Lax765601.ElementaryProperties 33 34 /-- `f` is prefix preserving: `w ⊑ v` implies `f w ⊑ f v`. -/ 35 def PrefixPreserving {A B : Type} (f : List A → List B) : Prop := 36 ∀ w v : List A, w <+: v → f w <+: f v 37 38 /-- `f` is length preserving, i.e. letter-to-letter: the output has the length of 39 the input. -/ 40 def LengthPreserving {A B : Type} (f : List A → List B) : Prop := 41 ∀ w : List A, (f w).length = w.length 42 43 /-- `f` is prefix determined: the first `n` output letters depend only on the 44 first `n` input letters. -/ 45 def PrefixDetermined {A B : Type} (f : List A → List B) : Prop := 46 ∀ (w v : List A) (n : ℕ), w.take n = v.take n → (f w).take n = (f v).take n 47 48 end Lax765601.ElementaryProperties 49 -
no assumptions
The machine-independent characterisation of Mealy machines (Theorem B.4.1), of the source, through Part A's bridge for .
-
thm✓
Lax132576.MealyDecidablep. 66Deciding whether a rational function is a Mealy machine
One can decide whether a given rational function is computed by a Mealy machine (Theorem B.4.2 of Transducers). By Theorem B.4.1 it suffices to check the three properties of a Mealy function: continuity is automatic for a rational function, length preservation is decided by Lemma B.4.3, and after Lemma B.4.5 has put the automaton in a form where every transition reads and writes one letter, prefix preservation fails exactly when two transitions with the same input letter and different output letters start in states reachable by a common input string.
1 import Lax765601.MealyMachine 2 import Lax132576.TransducerCodes 3 … module docstring, 24 lines 28 29 namespace Lax132576.MealyDecidable 30 31 open Lax765601.MealyMachine Lax132576.TransducerCodes 32 33 /-- Whether a coded rational function is computed by a Mealy machine is decidable. 34 -/ 35 axiom decidable_isMealy : 36 DecidableUnderPromise CodeFunctional 37 (fun c => ∃ f : List ℕ → List ℕ, 38 (∀ w, CodeWord c w → ∀ v, (codeRel c w v ↔ v = f w)) ∧ IsMealy f) 39 40 end Lax132576.MealyDecidable 41 -
⊢
Lax132576Proofs.Results.decidable_isMealypp. 66–69no assumptions
Deciding whether a rational function is a Mealy machine (Theorem B.4.2): prefix preservation is reduced to the equality of two rational functions (), decided by Theorem B.3.4 ().
-
thm✓
Lax132576.LengthPreservingDecidablep. 66Deciding length preservation of a rational function
One can decide whether a given rational function is length preserving (Lemma B.4.3 of Transducers). The book's direct argument computes the unique candidate typing of the automaton — the difference between output and input length of the runs reaching each state — and checks that every transition respects it and that accepting states have type zero (Claim B.4.4).
1 import Lax132576.TransducerCodes 2 … module docstring, 22 lines 25 26 namespace Lax132576.LengthPreservingDecidable 27 28 open Lax132576.TransducerCodes 29 30 /-- Length preservation of a coded rational function is decidable. -/ 31 axiom decidable_lengthPreserving : 32 DecidableUnderPromise CodeFunctional 33 (fun c => ∀ w v, codeRel c w v → v.length = w.length) 34 35 end Lax132576.LengthPreservingDecidable 36 -
no assumptions
Deciding length preservation (Lemma B.4.3): the bounded enumeration of runs of ().
-
thm✓
Lax132576.LengthPreservingTypingp. 67Length preservation through a typing of the states
Fix an automaton with output computing a function , all of whose states are productive. A typing is a function such that every run from an initial state to a state satisfies
The function is length preserving if and only if a typing exists and maps every accepting state to zero (Claim B.4.4 of Transducers). If no typing exists, two runs reach the same state with different length differences and the function cannot be length preserving; if a typing exists but some accepting state has nonzero type, a run reaching it witnesses the same.
1 import Lax765601.ElementaryProperties 2 import Lax132576.RationalRelations 3 … module docstring, 22 lines 26 27 namespace Lax132576.LengthPreservingTyping 28 29 open Lax765601.ElementaryProperties Lax132576.LabelledAutomata Lax132576.RationalRelations 30 31 /-- A function computed by an automaton with output with productive states is length 32 preserving if and only if the automaton has a typing vanishing on the accepting 33 states. -/ 34 axiom lengthPreserving_iff_typing {A B Q : Type} (M : NFAO A B Q) 35 (hprod : ∀ q, M.Productive q) {f : List A → List B} (hM : ∀ w v, M.rel w v ↔ v = f w) : 36 LengthPreserving f ↔ 37 ∃ τ : Q → ℤ, 38 (∀ q ∈ M.init, ∀ ts p, M.Path q ts p → 39 ((NFAO.outputOf ts).length : ℤ) = (LabAut.inputOf ts).length + τ p) ∧ 40 ∀ p ∈ M.final, τ p = 0 41 42 end Lax132576.LengthPreservingTyping 43 -
no assumptions
Length preservation through a typing (Claim B.4.4), of the source.
-
thm✓
Lax132576.LengthPreservingNormalFormp. 67Length preserving rational functions have length preserving automata
If a rational function is length preserving, then it is computed by an automaton with output in which the input and the output string of every transition have the same length (Lemma B.4.5 of Transducers). The book's proof takes the typing of Claim B.4.4 and works in the free group over the output alphabet: the new states are pairs of a state and a reduced string of length , possibly negative, and a transition of the original automaton becomes the transition , whose lengths agree.
1 import Lax765601.ElementaryProperties 2 import Lax132576.RationalFunctions 3 … module docstring, 20 lines 24 25 namespace Lax132576.LengthPreservingNormalForm 26 27 open Lax765601.ElementaryProperties Lax132576.RationalRelations Lax132576.RationalFunctions 28 29 /-- A length preserving rational function is computed by an automaton with output 30 whose every transition reads and writes strings of the same length. -/ 31 axiom exists_nfao_length_eq {A B : Type} [Finite A] [Finite B] 32 {f : List A → List B} (hf : IsRationalFun f) (hlen : LengthPreserving f) : 33 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), 34 (∀ t ∈ M.δ, t.2.1.length = t.2.2.1.length) ∧ ∀ w v, M.rel w v ↔ v = f w 35 36 end Lax132576.LengthPreservingNormalForm 37 -
no assumptions
Length preserving rational functions have length preserving automata (Lemma B.4.5), the free-group construction of the source ().
-
thm✓
Lax132576.SequentialCharacterisationp. 69Machine-independent characterisation of sequential functions
A function is sequential if and only if it (a) is continuous, (b) is prefix preserving, (c) outputs on the input , and (d) has the bounded increase property: the increase of output length caused by extending the input by one letter,
is finite (Theorem B.4.6 of Transducers, Ginsburg and Rose). The derivative , well defined by prefix preservation and of finite image by bounded increase, is shown to be computed by a finite automaton — its length by continuity modulo a large enough number, and then its value by continuity again.
1 import Lax765601.Continuity 2 import Lax765601.ElementaryProperties 3 import Lax132576.SequentialTransducers 4 … module docstring, 24 lines 29 30 namespace Lax132576.SequentialCharacterisation 31 32 open Lax765601.Continuity Lax765601.ElementaryProperties Lax132576.SequentialTransducers 33 34 /-- A function is sequential if and only if it maps `ε` to `ε`, is continuous, 35 prefix preserving, and has bounded increase. -/ 36 axiom isSequential_iff {A B : Type} [Finite A] [Finite B] (f : List A → List B) : 37 IsSequential f ↔ 38 f [] = [] ∧ Continuous f ∧ PrefixPreserving f ∧ 39 ∃ K : ℕ, ∀ (w : List A) (a : A), (f (w ++ [a])).length ≤ (f w).length + K 40 41 end Lax132576.SequentialCharacterisation 42 -
def
Lax132576.SequentialTransducersp. 69Sequential transducers
A sequential transducer (Section B.4.2 of Transducers) is defined like a Mealy machine, except that its transition function has type
so that a transition may produce an output string of any length, including the empty one, instead of exactly one letter. The functions computed by sequential transducers, the sequential functions, lie strictly between the Mealy machines and the rational functions; Theorem B.4.6 characterises them without reference to a machine.
1 import Mathlib.Data.Finite.Defs 2 … module docstring, 20 lines 23 24 namespace Lax132576.SequentialTransducers 25 26 /-- A sequential transducer: a Mealy machine whose transitions produce output 27 strings of variable length. -/ 28 structure Sequential (A B Q : Type) where 29 /-- The initial state. -/ 30 init : Q 31 /-- The transition function: a target state and an output string. -/ 32 step : Q → A → Q × List B 33 34 namespace Sequential 35 36 variable {A B Q : Type} 37 38 /-- The output produced from a given state on an input string. -/ 39 def run (T : Sequential A B Q) : Q → List A → List B 40 | _, [] => [] 41 | q, a :: w => (T.step q a).2 ++ T.run (T.step q a).1 w 42 43 /-- The semantics of a sequential transducer. -/ 44 def eval (T : Sequential A B Q) (w : List A) : List B := T.run T.init w 45 46 /-- The transition function of the underlying automaton. -/ 47 def transFun (T : Sequential A B Q) : Q → A → Q := fun q a => (T.step q a).1 48 49 end Sequential 50 51 /-- A function computed by a sequential transducer with a finite state space. -/ 52 def IsSequential {A B : Type} (f : List A → List B) : Prop := 53 ∃ (Q : Type) (_ : Finite Q) (T : Sequential A B Q), T.eval = f 54 55 end Lax132576.SequentialTransducers 56 -
⊢
Lax132576Proofs.Results.isSequential_iffpp. 69–70no assumptions
The characterisation of sequential functions (Theorem B.4.6), of the source through of the bridge.
-
def
Lax132576.LeftDistancep. 71Left distance and bounded variation
The left distance of two strings (Definition B.4.7 of Transducers) is the smallest such that the strings decompose as
i.e. the larger of the two lengths that remain after the longest common prefix has been removed. It measures how far apart two outputs of a transducer can be allowed to be after reading the same input. A partial function has bounded variation if for all the left distances are bounded, ranging over the strings for which both values are defined (Theorem B.4.8); for a total function, the relation
is an equivalence relation on input strings, and its index is what characterises the rational functions (Theorem B.4.13).
1 import Mathlib.Order.ConditionallyCompleteLattice.Basic 2 import Mathlib.Data.Nat.Lattice 3 … module docstring, 25 lines 29 30 namespace Lax132576.LeftDistance 31 32 /-- The left distance `‖w₁, w₂‖`: the least `k` such that `w₁ = v v₁` and 33 `w₂ = v v₂` with `|v₁|, |v₂| ≤ k`. -/ 34 noncomputable def leftDist {B : Type} (w₁ w₂ : List B) : ℕ := 35 sInf {k : ℕ | ∃ v v₁ v₂ : List B, 36 w₁ = v ++ v₁ ∧ w₂ = v ++ v₂ ∧ v₁.length ≤ k ∧ v₂.length ≤ k} 37 38 /-- The relation `w₁ ∼ w₂` of Theorem B.4.13: the left distances 39 `‖f (w w₁), f (w w₂)‖` are bounded uniformly in `w`. -/ 40 def BoundedVarRel {A B : Type} (f : List A → List B) (w₁ w₂ : List A) : Prop := 41 ∃ K : ℕ, ∀ w : List A, leftDist (f (w ++ w₁)) (f (w ++ w₂)) ≤ K 42 43 /-- A partial function has bounded variation if for all `w₁, w₂` the left distances 44 `‖f (w w₁), f (w w₂)‖` are bounded, over the `w` for which both are defined. -/ 45 def BoundedVariation {A B : Type} (f : List A → Option (List B)) : Prop := 46 ∀ w₁ w₂ : List A, ∃ K : ℕ, ∀ (w : List A) (v₁ v₂ : List B), 47 f (w ++ w₁) = some v₁ → f (w ++ w₂) = some v₂ → leftDist v₁ v₂ ≤ K 48 49 end Lax132576.LeftDistance 50 -
thm✓
Lax132576.SubsequentialCharacterisationpp. 71–72Machine-independent characterisation of subsequential functions
A partial function is subsequential if and only if it is continuous and has bounded variation: for all ,
ranging over the strings for which both values are defined (Theorem B.4.8 of Transducers, Choffrut). The construction of the transducer splits the output after a prefix into a branching part, which depends on the future, and a non-branching part, both of which are shown regular; the book's Claims B.4.9–B.4.12 are the steps of that construction.
1 import Lax765601.Continuity 2 import Lax132576.SubsequentialTransducers 3 import Lax132576.LeftDistance 4 … module docstring, 20 lines 25 26 namespace Lax132576.SubsequentialCharacterisation 27 28 open Lax765601.Continuity Lax132576.SubsequentialTransducers Lax132576.LeftDistance 29 30 /-- A partial function is subsequential if and only if it is continuous and has 31 bounded variation. -/ 32 axiom isSubsequential_iff {A B : Type} [Finite A] [Finite B] (f : List A → Option (List B)) : 33 IsSubsequential f ↔ PartialContinuous f ∧ BoundedVariation f 34 35 end Lax132576.SubsequentialCharacterisation 36 -
def
Lax132576.SubsequentialTransducerspp. 71–72Subsequential transducers
A subsequential transducer (Section B.4.3 of Transducers) is a sequential transducer equipped with a partial end-of-input function, which is applied to the state reached after the whole input has been read: its value, if defined, is appended to the output, and if it is undefined the transducer has no output. Subsequential transducers therefore compute partial functions; they can, for instance, append a letter to their input, which a sequential transducer cannot, and a function that is undefined on some inputs can be computed. Theorem B.4.8 characterises the subsequential functions.
1 import Lax765601.StateTransformations 2 import Lax132576.SequentialTransducers 3 … module docstring, 21 lines 25 26 namespace Lax132576.SubsequentialTransducers 27 28 open Lax765601.StateTransformations Lax132576.SequentialTransducers 29 30 /-- A subsequential transducer: a sequential transducer with a partial end-of-input 31 function applied to the last state of the run. -/ 32 structure Subsequential (A B Q : Type) extends Sequential A B Q where 33 /-- The partial end-of-input function. -/ 34 endOfInput : Q → Option (List B) 35 36 namespace Subsequential 37 38 variable {A B Q : Type} 39 40 /-- The semantics of a subsequential transducer: the output of the sequential 41 part followed by the end-of-input value, when defined. -/ 42 def eval (T : Subsequential A B Q) (w : List A) : Option (List B) := 43 (T.endOfInput (strTrans T.toSequential.transFun w T.toSequential.init)).map 44 (fun u => T.toSequential.eval w ++ u) 45 46 end Subsequential 47 48 /-- A partial function computed by a subsequential transducer with a finite state 49 space. -/ 50 def IsSubsequential {A B : Type} (f : List A → Option (List B)) : Prop := 51 ∃ (Q : Type) (_ : Finite Q) (T : Subsequential A B Q), T.eval = f 52 53 end Lax132576.SubsequentialTransducers 54 -
⊢
Lax132576Proofs.Results.isSubsequential_iffpp. 72–75no assumptions
The characterisation of subsequential functions (Theorem B.4.8), of the source.
-
thm✓
Lax132576.RationalMachineIndependentp. 76Machine-independent characterisation of rational functions
A function is rational if and only if it is continuous and the equivalence relation
on input strings has finite index (Theorem B.4.13 of Transducers, Reutenauer and Schützenberger). For a rational function computed by a bimachine, two strings with the same state of the suffix automaton are equivalent, so the index is finite; conversely the finitely many classes are used as the states of a suffix automaton, and the output after a prefix is computed by a subsequential transducer for each class. String reversal is not rational: all its input strings are pairwise inequivalent.
1 import Mathlib.Data.Set.Finite.Basic 2 import Lax765601.Continuity 3 import Lax132576.RationalFunctions 4 import Lax132576.LeftDistance 5 … module docstring, 22 lines 28 29 namespace Lax132576.RationalMachineIndependent 30 31 open Lax765601.Continuity Lax132576.RationalFunctions Lax132576.LeftDistance 32 33 /-- A function is rational if and only if it is continuous and the relation of 34 bounded variation has finitely many classes. -/ 35 axiom isRationalFun_iff {A B : Type} [Finite A] [Finite B] (f : List A → List B) : 36 IsRationalFun f ↔ 37 Continuous f ∧ {C : Set (List A) | ∃ w₁, C = {w₂ | BoundedVarRel f w₁ w₂}}.Finite 38 39 end Lax132576.RationalMachineIndependent 40 -
⊢
Lax132576Proofs.Results.isRationalFun_iffpp. 76–77no assumptions
The machine-independent characterisation of rational functions (Theorem B.4.13), of the source.
-
def
Lax132576.RationalFunctionsp. 44Rational functions
A rational function (Definition B.2.1 of Transducers) is the special case of a rational relation in which each input string is related to exactly one output string. The definition is semantic: the underlying automaton is nondeterministic and merely happens to have a unique output for every input, possibly through several runs; Theorem B.2.3 gives the deterministic model, the bimachine, that computes exactly these functions. Rational functions inherit closure under composition and continuity from rational relations, and every Mealy machine is a rational function.
1 import Lax132576.RationalRelations 2 … module docstring, 21 lines 24 25 namespace Lax132576.RationalFunctions 26 27 open Lax132576.RationalRelations 28 29 /-- A string-to-string function is rational if its graph is a rational relation. 30 -/ 31 def IsRationalFun {A B : Type} (f : List A → List B) : Prop := 32 IsRationalRel (fun w v => v = f w) 33 34 end Lax132576.RationalFunctions 35 -
def
Lax132576.Bimachinespp. 44–45Bimachines
A bimachine (Definition B.2.2 of Transducers) is a deterministic model for the rational functions. It consists of input and output alphabets and , two deterministic automata over without accepting states — the prefix automaton and the suffix automaton — and an output function
On an input it considers, for every , the factorisation into the prefix and the suffix , runs the prefix automaton on the prefix and the suffix automaton on the reverse of the suffix, applies the output function to the resulting pair of states, and concatenates the pieces in increasing order of . Bimachines compute exactly the rational functions (Theorem B.2.3). A bimachine is aperiodic if both its automata are aperiodic, i.e. satisfy the stabilisation condition on state transformations; aperiodic bimachines compute exactly the first-order relabellings (Theorem C.4.16).
1 import Lax765601.StateTransformations 2 … module docstring, 27 lines 30 31 namespace Lax132576.Bimachines 32 33 open Lax765601.StateTransformations 34 35 /-- A bimachine: a deterministic prefix automaton, a deterministic suffix automaton 36 (run on the reverse of the suffix) and an output function on pairs of states. -/ 37 structure Bimachine (A B P S : Type) where 38 /-- Initial state of the prefix automaton. -/ 39 prefixInit : P 40 /-- Transition function of the prefix automaton. -/ 41 prefixStep : P → A → P 42 /-- Initial state of the suffix automaton. -/ 43 suffixInit : S 44 /-- Transition function of the suffix automaton. -/ 45 suffixStep : S → A → S 46 /-- The output function. -/ 47 out : P → S → List B 48 49 namespace Bimachine 50 51 variable {A B P S : Type} 52 53 /-- The semantics of a bimachine: for every gap `i` of the input, the prefix 54 automaton is run on the first `i` letters and the suffix automaton on the reverse 55 of the rest, and the pieces of output are concatenated. -/ 56 def eval (M : Bimachine A B P S) (w : List A) : List B := 57 ((List.range (w.length + 1)).map (fun i => 58 M.out (strTrans M.prefixStep (w.take i) M.prefixInit) 59 (strTrans M.suffixStep (w.drop i).reverse M.suffixInit))).flatten 60 61 end Bimachine 62 63 /-- A function computed by a bimachine with finite state spaces. -/ 64 def IsBimachine {A B : Type} (f : List A → List B) : Prop := 65 ∃ (P S : Type) (_ : Finite P) (_ : Finite S) (M : Bimachine A B P S), M.eval = f 66 67 /-- A function computed by an aperiodic bimachine: both automata satisfy the 68 stabilisation condition on their state transformations. -/ 69 def IsAperiodicBimachine {A B : Type} (f : List A → List B) : Prop := 70 ∃ (P S : Type) (_ : Finite P) (_ : Finite S) (M : Bimachine A B P S), 71 M.eval = f ∧ TransAperiodic M.prefixStep ∧ TransAperiodic M.suffixStep 72 73 end Lax132576.Bimachines 74 -
thm✓
Lax132576.RationalUnambiguousBimachinep. 45Eilenberg's theorem: rational functions, unambiguous automata and bimachines
For a string-to-string function the following are equivalent (Theorem B.2.3 of Transducers, Eilenberg): (1) it is a rational relation which happens to be functional; (2) it is computed by an unambiguous nondeterministic automaton with output; (3) it is computed by a bimachine. The book proves (3) ⇒ (1) ⇒ (2) ⇒ (3); here the three implications with content are separate statements — , and — and this statement is their conjunction, the implication (2) ⇒ (1) being immediate since an unambiguous automaton is an automaton.
1 import Mathlib.Data.List.TFAE 2 import Lax132576.RationalFunctions 3 import Lax132576.Bimachines 4 … module docstring, 20 lines 25 26 namespace Lax132576.RationalUnambiguousBimachine 27 28 open Lax132576.RationalRelations Lax132576.RationalFunctions Lax132576.Bimachines 29 30 /-- Eilenberg's theorem: a function is rational, computed by an unambiguous 31 automaton with output, or computed by a bimachine, equivalently. -/ 32 axiom tfae_rational_unambiguous_bimachine {A B : Type} [Finite A] [Finite B] 33 (f : List A → List B) : 34 [IsRationalFun f, IsUnambiguousRel (fun w v => v = f w), IsBimachine f].TFAE 35 36 end Lax132576.RationalUnambiguousBimachine 37 -
thm✓
Lax132576.UnambiguousOfRationalp. 45Rational functions are computed by unambiguous automata
Every rational function is computed by an unambiguous nondeterministic automaton with output, one with exactly one accepting run per input string: the implication (1) ⇒ (2) of Theorem B.2.3 of Transducers (Eilenberg). It is a consequence of the uniformisation lemma (Lemma B.2.5): the graph of a function is a total rational relation, so it contains an unambiguous rational relation, which must be the graph itself.
1 import Lax132576.RationalFunctions 2 … module docstring, 17 lines 20 21 namespace Lax132576.UnambiguousOfRational 22 23 open Lax132576.RationalRelations Lax132576.RationalFunctions 24 25 /-- The graph of a rational function is computed by an unambiguous automaton with 26 output. -/ 27 axiom isUnambiguousRel_of_isRationalFun {A B : Type} [Finite A] [Finite B] 28 {f : List A → List B} (hf : IsRationalFun f) : IsUnambiguousRel (fun w v => v = f w) 29 30 end Lax132576.UnambiguousOfRational 31 -
thm✓
Lax132576.BimachineOfRationalp. 45Rational functions are computed by bimachines
Every rational function is computed by a bimachine: the implication (1) ⇒ (3) of Theorem B.2.3 of Transducers (Eilenberg), through the unambiguous automaton of (2). Given an unambiguous automaton whose accepting runs end with a single empty-input transition, the bimachine's prefix automaton computes the states reachable from an initial state on the prefix, its suffix automaton computes the first letter of the suffix and the states that can reach acceptance on the rest, and the output function reads off the output of the unique transition consuming the letter at the gap — or of the final empty-input transition at the last gap.
1 import Lax132576.RationalFunctions 2 import Lax132576.Bimachines 3 … module docstring, 20 lines 24 25 namespace Lax132576.BimachineOfRational 26 27 open Lax132576.RationalFunctions Lax132576.Bimachines 28 29 /-- A rational function is computed by a bimachine. -/ 30 axiom isBimachine_of_isRationalFun {A B : Type} [Finite A] [Finite B] 31 {f : List A → List B} (hf : IsRationalFun f) : IsBimachine f 32 33 end Lax132576.BimachineOfRational 34 -
thm✓
Lax132576.RationalOfBimachinep. 45Bimachines compute rational functions
Every function computed by a bimachine is rational: the implication (3) ⇒ (1) of Theorem B.2.3 of Transducers, the easiest one. The nondeterministic automaton guesses the runs of both the prefix and the suffix automaton, its states being pairs of their states plus one extra final state; a transition on the letter from to requires in the prefix automaton and in the suffix automaton and outputs the piece of the gap to the left of , and an empty transition into the final state outputs the piece of the last gap.
1 import Lax132576.RationalFunctions 2 import Lax132576.Bimachines 3 … module docstring, 19 lines 23 24 namespace Lax132576.RationalOfBimachine 25 26 open Lax132576.RationalFunctions Lax132576.Bimachines 27 28 /-- A function computed by a bimachine is rational. -/ 29 axiom isRationalFun_of_isBimachine {A B : Type} [Finite A] [Finite B] 30 {f : List A → List B} (hf : IsBimachine f) : IsRationalFun f 31 32 end Lax132576.RationalOfBimachine 33 -
Eilenberg's theorem as a , glued from the three implications with content, taken as assumptions, and the trivial (2) ⇒ (1).
-
thm✓
Lax132576.EpsilonEliminationExtendedp. 46Elimination of ε-transitions, with extended transitions
Every rational relation is computed by an automaton with output and extended transitions in which every accepting run is in ε-free normal form: if the input string is nonempty, each transition reads exactly one letter, and if the input is empty, the run has exactly one transition (Lemma B.2.4 of Transducers, first sentence). After arranging that no state is both initial and final and that every transition reads at most one letter, the usual elimination replaces, for every letter and states , the runs from to reading and any number of empty-input transitions by one transition labelled with the regular language of their outputs; a fresh initial and a fresh final state with one transition between them, labelled with the outputs on the empty input, take care of the empty string.
1 import Lax132576.EpsilonFreeAutomata 2 … module docstring, 23 lines 26 27 namespace Lax132576.EpsilonEliminationExtended 28 29 open Lax132576.LabelledAutomata Lax132576.RationalRelations Lax132576.EpsilonFreeAutomata 30 31 /-- Every rational relation is computed by an ε-free automaton with extended 32 transitions. -/ 33 axiom exists_extended_epsilonFree {A B : Type} [Finite A] [Finite B] 34 {R : List A → List B → Prop} (hR : IsRationalRel R) : 35 ∃ (Q : Type) (_ : Finite Q) (M : LabAut A (Language B) Q), 36 IsExtendedNFAO M ∧ EpsilonFree M ∧ ∀ w v, R w v ↔ extRel M w v 37 38 end Lax132576.EpsilonEliminationExtended 39 -
thm✓
Lax132576.EpsilonEliminationFinitep. 46Elimination of ε-transitions for finitely valued relations
If a rational relation is such that every input string has finitely many outputs, then it is computed by an ordinary automaton with output in ε-free normal form: extended transitions are not needed (Lemma B.2.4 of Transducers, second sentence). In the elimination construction, the regular languages labelling the new transitions are then finite, and each such transition is replaced by finitely many transitions with one output string each.
1 import Lax132576.EpsilonFreeAutomata 2 … module docstring, 19 lines 22 23 namespace Lax132576.EpsilonEliminationFinite 24 25 open Lax132576.RationalRelations Lax132576.EpsilonFreeAutomata 26 27 /-- A finitely valued rational relation is computed by an ε-free automaton with 28 output. -/ 29 axiom exists_nfao_epsilonFree {A B : Type} [Finite A] [Finite B] 30 {R : List A → List B → Prop} (hR : IsRationalRel R) (hfin : ∀ w, {v | R w v}.Finite) : 31 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), EpsilonFree M ∧ ∀ w v, R w v ↔ M.rel w v 32 33 end Lax132576.EpsilonEliminationFinite 34 -
def
Lax132576.EpsilonFreeAutomatap. 46Extended transitions and the elimination of ε-transitions
Transitions with empty input (-transitions) are essential to automata with output in two roles: producing an output for the empty input, and producing infinitely many outputs for one input. Lemma B.2.4 of Transducers shows that, up to these two caveats, they can be eliminated. An automaton with extended transitions carries, instead of an output string, a regular language of output strings on every transition; the relation it computes takes as outputs all strings in the concatenation of the languages along an accepting run. An automaton (with ordinary or extended transitions) is in the ε-free normal form of the lemma if in every accepting run, either the input is nonempty and each transition reads exactly one letter, or the input is empty and the run consists of exactly one transition.
1 import Mathlib.Computability.DFA 2 import Lax132576.RationalRelations 3 … module docstring, 25 lines 29 30 namespace Lax132576.EpsilonFreeAutomata 31 32 open Lax132576.LabelledAutomata 33 34 /-- An automaton with extended transitions: transitions are labelled by an input 35 string and a regular language of output strings. -/ 36 def IsExtendedNFAO {A B Q : Type} (M : LabAut A (Language B) Q) : Prop := 37 ∀ t ∈ M.δ, Language.IsRegular t.2.2.1 38 39 /-- The relation computed by an automaton with extended transitions: the output 40 is any string in the concatenation of the languages along an accepting run. -/ 41 def extRel {A B Q : Type} (M : LabAut A (Language B) Q) (w : List A) (v : List B) : Prop := 42 ∃ ts, M.Accepting ts ∧ LabAut.inputOf ts = w ∧ v ∈ (LabAut.labelsOf ts).prod 43 44 /-- The normal form of Lemma B.2.4: in every accepting run, either the input is 45 nonempty and each transition reads exactly one letter, or the input is empty and 46 the run has exactly one transition. -/ 47 def EpsilonFree {A L Q : Type} (M : LabAut A L Q) : Prop := 48 ∀ ts, M.Accepting ts → 49 (LabAut.inputOf ts ≠ [] → ∀ t ∈ ts, t.2.1.length = 1) ∧ 50 (LabAut.inputOf ts = [] → ts.length = 1) 51 52 end Lax132576.EpsilonFreeAutomata 53 -
no assumptions
Elimination of ε-transitions with extended transitions (Lemma B.2.4, first sentence), the first conjunct of the source's .
-
thm✓
Lax132576.Uniformisationp. 47Uniformisation of total rational relations
If a rational relation is total — every input string has at least one output — then it contains an unambiguous rational relation (Lemma B.2.5 of Transducers). After eliminating ε-transitions, the unambiguous automaton follows the run of the original automaton that is lexicographically minimal for a chosen linear order on the states: its states are pairs of the set of states that can still reach acceptance, chosen deterministically from right to left, and the minimal state reachable so far, chosen deterministically from left to right; the output of a transition is one chosen output of the original automaton between its two states on its letter.
1 import Lax132576.RationalRelations 2 … module docstring, 20 lines 23 24 namespace Lax132576.Uniformisation 25 26 open Lax132576.RationalRelations 27 28 /-- A total rational relation contains an unambiguous rational relation. -/ 29 axiom exists_isUnambiguousRel_le {A B : Type} [Finite A] [Finite B] 30 {R : List A → List B → Prop} (hR : IsRationalRel R) (htotal : ∀ w, ∃ v, R w v) : 31 ∃ S : List A → List B → Prop, (∀ w v, S w v → R w v) ∧ IsUnambiguousRel S 32 33 end Lax132576.Uniformisation 34 -
no assumptions
Uniformisation of total rational relations (Lemma B.2.5): the lexicographically minimal run of the source's construction.
-
thm✓
Lax132576.RationalPrimesp. 49The rational functions are the compositions of prime rational functions
A string-to-string function is rational if and only if it is a composition of prime rational functions: prime Mealy machines, their right-to-left variants, string homomorphisms and the separator function (Theorem B.2.6 of Transducers). This is the Krohn–Rhodes theorem one step up the transducer ladder. The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax132576.RationalFunctions 2 import Lax132576.PrimeRationalFunctions 3 … module docstring, 16 lines 20 21 namespace Lax132576.RationalPrimes 22 23 open Lax765601.CompositionClosure Lax132576.RationalFunctions Lax132576.PrimeRationalFunctions 24 25 /-- A function is rational if and only if it is a composition of prime rational 26 functions. -/ 27 axiom isRationalFun_iff_compClosure_primeRational {A B : Type} [Finite A] [Finite B] 28 (f : List A → List B) : IsRationalFun f ↔ CompClosure PrimeRationalFam A B f 29 30 end Lax132576.RationalPrimes 31 -
thm✓
Lax132576.PrimesOfRationalp. 49Rational functions decompose into prime rational functions
Every rational function is a composition of prime rational functions — prime Mealy machines, their right-to-left variants, string homomorphisms and the separator function (Theorem B.2.6 of Transducers, the implication ⇒). By Eilenberg's theorem the function is computed by a bimachine; one appends the separator, labels every position with the state of the prefix automaton (a Mealy machine, decomposed by the Krohn–Rhodes theorem) and with the state of the suffix automaton (a right-to-left Mealy machine, the state being stored one position to the right, which is what the separator is for), and a homomorphism produces the output of every gap.
1 import Lax132576.RationalFunctions 2 import Lax132576.PrimeRationalFunctions 3 … module docstring, 21 lines 25 26 namespace Lax132576.PrimesOfRational 27 28 open Lax765601.CompositionClosure Lax132576.RationalFunctions Lax132576.PrimeRationalFunctions 29 30 /-- A rational function is a composition of prime rational functions. -/ 31 axiom compClosure_primeRational_of_isRationalFun {A B : Type} [Finite A] [Finite B] 32 {f : List A → List B} (hf : IsRationalFun f) : CompClosure PrimeRationalFam A B f 33 34 end Lax132576.PrimesOfRational 35 -
thm✓
Lax132576.RationalOfPrimesp. 49Compositions of prime rational functions are rational
Every composition of prime rational functions is rational (Theorem B.2.6 of Transducers, the implication ⇐): each prime is rational — a Mealy machine and a homomorphism are read directly as automata with output, the separator function needs one empty-input transition, and a right-to-left Mealy machine is a bimachine with a trivial prefix automaton — and rational functions are closed under composition (Theorem B.1.4).
1 import Lax132576.RationalFunctions 2 import Lax132576.PrimeRationalFunctions 3 … module docstring, 17 lines 21 22 namespace Lax132576.RationalOfPrimes 23 24 open Lax765601.CompositionClosure Lax132576.RationalFunctions Lax132576.PrimeRationalFunctions 25 26 /-- A composition of prime rational functions is rational. -/ 27 axiom isRationalFun_of_compClosure_primeRational {A B : Type} [Finite A] [Finite B] 28 {f : List A → List B} (hf : CompClosure PrimeRationalFam A B f) : IsRationalFun f 29 30 end Lax132576.RationalOfPrimes 31 -
def
Lax132576.PrimeRationalFunctionsp. 49The prime rational functions
The prime rational functions of Theorem B.2.6 of Transducers are the following four kinds of functions:
- the prime Mealy machines, i.e. the reversible and the flip-flop Mealy machines;
- their right-to-left variants — Mealy machines that process the input from right to left, the initial state being used after the rightmost position;
- the string homomorphisms;
- the function which appends a fresh separator symbol to the input string.
Theorem B.2.6 says that the rational functions are exactly the compositions of prime rational functions, the analogue of the Krohn–Rhodes theorem one step up the transducer ladder.
1 import Lax765601.PrimeMealyMachines 2 import Lax132576.StringHomomorphisms 3 … module docstring, 30 lines 34 35 namespace Lax132576.PrimeRationalFunctions 36 37 open Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax132576.StringHomomorphisms 38 39 /-- The family of prime rational functions: prime Mealy machines, their 40 right-to-left variants, string homomorphisms, and the separator function 41 `w ↦ w #`. -/ 42 def PrimeRationalFam : Family := fun A B f => 43 PrimeMealyFam A B f ∨ 44 PrimeMealyFam A B (fun w => (f w.reverse).reverse) ∨ 45 (∃ φ : A → List B, f = homOf φ) ∨ 46 (∃ e : Option A ≃ B, f = fun w => w.map (fun a => e (some a)) ++ [e none]) 47 48 end Lax132576.PrimeRationalFunctions 49 -
Theorem B.2.6 as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax132576.RationalMealyCharacterisationp. 50Which rational functions are Mealy machines
A rational function is computed by a Mealy machine if and only if it is letter-to-letter — the output has the length of the input — and deterministic: input strings that agree on their first letters have outputs that agree on their first letters (Theorem B.2.7 of Transducers). Mealy machines are the special case of the rational functions that the theorem pins down; the proof goes through the machine-independent characterisation of Theorem B.4.1, since a rational function is continuous.
1 import Lax765601.MealyMachine 2 import Lax765601.ElementaryProperties 3 import Lax132576.RationalFunctions 4 … module docstring, 19 lines 24 25 namespace Lax132576.RationalMealyCharacterisation 26 27 open Lax765601.MealyMachine Lax765601.ElementaryProperties Lax132576.RationalFunctions 28 29 /-- A rational function is computed by a Mealy machine if and only if it is 30 letter-to-letter and prefix determined. -/ 31 axiom isMealy_iff_of_isRationalFun {A B : Type} [Finite A] [Finite B] {f : List A → List B} 32 (hf : IsRationalFun f) : IsMealy f ↔ LengthPreserving f ∧ PrefixDetermined f 33 34 end Lax132576.RationalMealyCharacterisation 35 -
def
Lax132576.RationalRelationsp. 36Nondeterministic automata with output and rational relations
A nondeterministic automaton with output (Definition B.1.1 of Transducers) consists of input and output alphabets and , a finite set of states , initial and final subsets , and a finite transition relation
It is a directed graph whose edges are labelled by pairs of an input string and an output string; a run is a path from an initial to a final state, and its input and output strings are the concatenations of the labels along it. The semantics of the automaton is the relation of the pairs (input string, output string) of its accepting runs, and a relation is rational (Definition B.1.2) if it is the semantics of such an automaton. Rational relations are input/output symmetric, and a single input may have infinitely many outputs, through transitions with empty input.
An automaton with output is unambiguous if every input string has exactly one accepting run; the relations computed by unambiguous automata are the second item of Theorem B.2.3. A state is productive if it occurs in some accepting run (Claim B.4.4).
1 import Lax132576.LabelledAutomata 2 … module docstring, 32 lines 35 36 namespace Lax132576.RationalRelations 37 38 open Lax132576.LabelledAutomata 39 40 /-- A nondeterministic automaton with output: a labelled automaton whose labels 41 are output strings. -/ 42 abbrev NFAO (A B Q : Type) := LabAut A (List B) Q 43 44 namespace NFAO 45 46 variable {A B Q : Type} 47 48 /-- The output string of a path: the concatenation of the outputs of its 49 transitions. -/ 50 def outputOf (ts : List (Q × List A × List B × Q)) : List B := (LabAut.labelsOf ts).flatten 51 52 /-- The relation computed by an automaton with output: `w` is related to `v` if 53 some accepting run reads `w` and writes `v`. -/ 54 def rel (M : NFAO A B Q) (w : List A) (v : List B) : Prop := 55 ∃ ts, M.Accepting ts ∧ LabAut.inputOf ts = w ∧ outputOf ts = v 56 57 /-- An automaton with output is unambiguous if every input string has exactly one 58 accepting run. -/ 59 def Unambiguous (M : NFAO A B Q) : Prop := 60 ∀ w : List A, ∃! ts, M.Accepting ts ∧ LabAut.inputOf ts = w 61 62 /-- A state is productive if it occurs in some accepting run. -/ 63 def Productive (M : NFAO A B Q) (q : Q) : Prop := 64 ∃ q₀ ∈ M.init, ∃ p ∈ M.final, ∃ ts₁ ts₂, M.Path q₀ ts₁ q ∧ M.Path q ts₂ p 65 66 end NFAO 67 68 /-- A relation is rational if it is computed by a nondeterministic automaton with 69 output with a finite state space. -/ 70 def IsRationalRel {A B : Type} (R : List A → List B → Prop) : Prop := 71 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), ∀ w v, R w v ↔ M.rel w v 72 73 /-- A relation computed by an unambiguous automaton with output. -/ 74 def IsUnambiguousRel {A B : Type} (R : List A → List B → Prop) : Prop := 75 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), M.Unambiguous ∧ ∀ w v, R w v ↔ M.rel w v 76 77 end Lax132576.RationalRelations 78 -
def
Lax132576.LabelledAutomatap. 36Automata with labelled transitions
The two nondeterministic models of Part B of Transducers — nondeterministic automata with output (Definition B.1.1) and weighted automata (Definition B.3.2) — are automata whose finitely many transitions are labelled by an input string together with a label from some set: an output string in the first case, an element of a semiring in the second. This concept is their common basis: a finite set of transitions
each a directed edge from a state to a state carrying an input string and a label, together with initial and final subsets of the state space. A run is a path that begins in an initial state and ends in a final state; its input string is the concatenation of the input strings of its transitions, and its labels are read off in the order in which the transitions are taken.
1 import Mathlib.Data.Set.Finite.Basic 2 … module docstring, 30 lines 33 34 namespace Lax132576.LabelledAutomata 35 36 /-- An automaton whose finitely many transitions are labelled by an input string and 37 a label from `L`, with distinguished sets of initial and final states. -/ 38 structure LabAut (A L Q : Type) where 39 /-- The set of initial states. -/ 40 init : Set Q 41 /-- The set of final states. -/ 42 final : Set Q 43 /-- The transition relation. -/ 44 δ : Set (Q × List A × L × Q) 45 /-- There are only finitely many transitions. -/ 46 δ_finite : δ.Finite 47 48 namespace LabAut 49 50 variable {A L Q : Type} 51 52 /-- A path in the automaton, given as the list of the transitions it uses. -/ 53 inductive Path (M : LabAut A L Q) : Q → List (Q × List A × L × Q) → Q → Prop 54 | nil (q : Q) : Path M q [] q 55 | cons {q : Q} {u : List A} {l : L} {q' : Q} {ts : List (Q × List A × L × Q)} {p : Q} : 56 (q, u, l, q') ∈ M.δ → Path M q' ts p → Path M q ((q, u, l, q') :: ts) p 57 58 /-- The input string of a path: the concatenation of the input strings of its 59 transitions. -/ 60 def inputOf (ts : List (Q × List A × L × Q)) : List A := (ts.map (fun t => t.2.1)).flatten 61 62 /-- The labels along a path, in the order of the transitions. -/ 63 def labelsOf (ts : List (Q × List A × L × Q)) : List L := ts.map (fun t => t.2.2.1) 64 65 /-- A path is accepting if it starts in an initial state and ends in a final state. 66 -/ 67 def Accepting (M : LabAut A L Q) (ts : List (Q × List A × L × Q)) : Prop := 68 ∃ q ∈ M.init, ∃ p ∈ M.final, M.Path q ts p 69 70 /-- The accepting paths with a given input string. -/ 71 def acceptingOn (M : LabAut A L Q) (w : List A) : Set (List (Q × List A × L × Q)) := 72 {ts | M.Accepting ts ∧ inputOf ts = w} 73 74 end LabAut 75 76 end Lax132576.LabelledAutomata 77 -
def
Lax132576.RationalRelationsp. 36Nondeterministic automata with output and rational relations
A nondeterministic automaton with output (Definition B.1.1 of Transducers) consists of input and output alphabets and , a finite set of states , initial and final subsets , and a finite transition relation
It is a directed graph whose edges are labelled by pairs of an input string and an output string; a run is a path from an initial to a final state, and its input and output strings are the concatenations of the labels along it. The semantics of the automaton is the relation of the pairs (input string, output string) of its accepting runs, and a relation is rational (Definition B.1.2) if it is the semantics of such an automaton. Rational relations are input/output symmetric, and a single input may have infinitely many outputs, through transitions with empty input.
An automaton with output is unambiguous if every input string has exactly one accepting run; the relations computed by unambiguous automata are the second item of Theorem B.2.3. A state is productive if it occurs in some accepting run (Claim B.4.4).
1 import Lax132576.LabelledAutomata 2 … module docstring, 32 lines 35 36 namespace Lax132576.RationalRelations 37 38 open Lax132576.LabelledAutomata 39 40 /-- A nondeterministic automaton with output: a labelled automaton whose labels 41 are output strings. -/ 42 abbrev NFAO (A B Q : Type) := LabAut A (List B) Q 43 44 namespace NFAO 45 46 variable {A B Q : Type} 47 48 /-- The output string of a path: the concatenation of the outputs of its 49 transitions. -/ 50 def outputOf (ts : List (Q × List A × List B × Q)) : List B := (LabAut.labelsOf ts).flatten 51 52 /-- The relation computed by an automaton with output: `w` is related to `v` if 53 some accepting run reads `w` and writes `v`. -/ 54 def rel (M : NFAO A B Q) (w : List A) (v : List B) : Prop := 55 ∃ ts, M.Accepting ts ∧ LabAut.inputOf ts = w ∧ outputOf ts = v 56 57 /-- An automaton with output is unambiguous if every input string has exactly one 58 accepting run. -/ 59 def Unambiguous (M : NFAO A B Q) : Prop := 60 ∀ w : List A, ∃! ts, M.Accepting ts ∧ LabAut.inputOf ts = w 61 62 /-- A state is productive if it occurs in some accepting run. -/ 63 def Productive (M : NFAO A B Q) (q : Q) : Prop := 64 ∃ q₀ ∈ M.init, ∃ p ∈ M.final, ∃ ts₁ ts₂, M.Path q₀ ts₁ q ∧ M.Path q ts₂ p 65 66 end NFAO 67 68 /-- A relation is rational if it is computed by a nondeterministic automaton with 69 output with a finite state space. -/ 70 def IsRationalRel {A B : Type} (R : List A → List B → Prop) : Prop := 71 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), ∀ w v, R w v ↔ M.rel w v 72 73 /-- A relation computed by an unambiguous automaton with output. -/ 74 def IsUnambiguousRel {A B : Type} (R : List A → List B → Prop) : Prop := 75 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), M.Unambiguous ∧ ∀ w v, R w v ↔ M.rel w v 76 77 end Lax132576.RationalRelations 78 -
thm✓
Lax132576.RationalCompositionp. 38Rational relations are closed under composition
If and are rational relations, then so is their relational composition
(Theorem B.1.4 of Transducers). The proof is the product construction of Theorem A.1.3, after splitting transitions so that each produces at most one letter of input or output and adding empty transitions around every state, so that the two runs can be synchronised on the intermediate string.
1 import Lax132576.RationalRelations 2 … module docstring, 18 lines 21 22 namespace Lax132576.RationalComposition 23 24 open Lax132576.RationalRelations 25 26 /-- The composition of two rational relations is rational. -/ 27 axiom isRationalRel_comp {A B C : Type} 28 {R : List A → List B → Prop} {S : List B → List C → Prop} 29 (hR : IsRationalRel R) (hS : IsRationalRel S) : 30 IsRationalRel (fun w v => ∃ u, R w u ∧ S u v) 31 32 end Lax132576.RationalComposition 33 -
⊢
Lax132576Proofs.Results.isRationalRel_comppp. 38–39no assumptions
Rational relations are closed under composition (Theorem B.1.4): the product construction on ε-normalised automata ().
-
thm✓
Lax132576.RationalContinuityp. 39Rational relations are continuous
If is a rational relation and is a regular language, then the inverse image
is a regular language (Theorem B.1.5 of Transducers). The book deduces it from closure under composition: rational relations with an empty output alphabet are the regular languages over the input alphabet, and the inverse image is the composition of with the relation . Since rational relations are input/output symmetric, forward images of regular languages are regular too.
1 import Lax765601.Continuity 2 import Lax132576.RationalRelations 3 … module docstring, 20 lines 24 25 namespace Lax132576.RationalContinuity 26 27 open Lax765601.Continuity Lax132576.RationalRelations 28 29 /-- A rational relation is continuous: inverse images of regular languages are 30 regular. -/ 31 axiom relContinuous_of_isRationalRel {A B : Type} {R : List A → List B → Prop} 32 (hR : IsRationalRel R) : RelContinuous R 33 34 end Lax132576.RationalContinuity 35 -
thm✓
Lax132576.RationalEquivalenceUndecidablepp. 39–40Equivalence of rational relations is undecidable
The equivalence problem is undecidable for rational relations (Theorem B.1.6 of Transducers, Griffiths). The book reduces the Post correspondence problem to the universality problem: for two homomorphisms , the instance has no solution exactly when the union of the complements of and — a rational relation by Claim B.1.7 and closure under union — is the full relation .
1 import Lax132576.TransducerCodes 2 … module docstring, 21 lines 24 25 namespace Lax132576.RationalEquivalenceUndecidable 26 27 open Lax132576.TransducerCodes 28 29 /-- No algorithm decides whether two coded rational relations are equal. -/ 30 axiom not_computablePred_codeRel_eq : 31 ¬ ComputablePred (fun p : RelCode × RelCode => codeRel p.1 = codeRel p.2) 32 33 end Lax132576.RationalEquivalenceUndecidable 34 -
Equivalence of rational relations is undecidable (Theorem B.1.6).
-
thm✓
Lax132576.HomomorphismComplementp. 40The complement of a homomorphism is rational
If is a string homomorphism, then its complement
is a rational relation (Claim B.1.7 of Transducers). The automaton guesses a prefix of the input on which the homomorphism is applied correctly, then insists on an error at the next letter: it outputs a proper prefix of the image of that letter and nothing more, or a string incomparable with it and then anything. This is the observation behind the undecidability of equivalence (Theorem B.1.6).
1 import Lax132576.RationalRelations 2 import Lax132576.StringHomomorphisms 3 … module docstring, 19 lines 23 24 namespace Lax132576.HomomorphismComplement 25 26 open Lax132576.RationalRelations Lax132576.StringHomomorphisms 27 28 /-- The complement of the graph of a string homomorphism is a rational relation. -/ 29 axiom isRationalRel_ne_homOf {A B : Type} [Finite A] [Finite B] (φ : A → List B) : 30 IsRationalRel (fun (w : List A) (v : List B) => v ≠ homOf φ w) 31 32 end Lax132576.HomomorphismComplement 33 -
no assumptions
The complement of a homomorphism is rational (Claim B.1.7).
-
def
Lax132576.WeightedAutomatapp. 59–60Weighted automata
A weighted automaton over a semiring (Definition B.3.2 of Transducers) is defined like a nondeterministic automaton with output, except that the transitions carry elements of instead of output strings, and that every input string is required to have only finitely many accepting runs. Its semantics is the function mapping an input string to
the sum over the accepting runs over of the product of the weights of the transitions of , taken in the order of the run — which matters when the multiplication of is not commutative. The finiteness requirement is what makes the sum well defined. Over the Boolean semiring weighted automata are nondeterministic automata; over the semiring of regular languages they are the rational relations; over they have decidable equivalence (Theorem B.3.3).
1 import Mathlib.Algebra.BigOperators.Finprod 2 import Lax132576.LabelledAutomata 3 … module docstring, 30 lines 34 35 namespace Lax132576.WeightedAutomata 36 37 open Lax132576.LabelledAutomata 38 39 variable {A S Q : Type} [Semiring S] 40 41 /-- The weight of a path: the product of the weights of its transitions, in the 42 order in which they are taken. -/ 43 def weightOf (ts : List (Q × List A × S × Q)) : S := (LabAut.labelsOf ts).prod 44 45 /-- The semantics of a weighted automaton: the sum of the weights of the accepting 46 runs over the input. -/ 47 noncomputable def wEval (M : LabAut A S Q) (w : List A) : S := 48 ∑ᶠ ts ∈ M.acceptingOn w, weightOf ts 49 50 /-- The requirement of Definition B.3.2: every input string has only finitely 51 many accepting runs. -/ 52 def FinitelyManyRuns (M : LabAut A S Q) : Prop := ∀ w : List A, (M.acceptingOn w).Finite 53 54 /-- A function `A* → S` computed by a weighted automaton over the semiring `S` 55 with a finite state space. -/ 56 def IsWeighted {A S : Type} [Semiring S] (f : List A → S) : Prop := 57 ∃ (Q : Type) (_ : Finite Q) (M : LabAut A S Q), FinitelyManyRuns M ∧ wEval M = f 58 59 end Lax132576.WeightedAutomata 60 -
thm✓
Lax132576.WeightedEquivalenceDecidablepp. 61–62Decidable equivalence of weighted automata over the rationals
Given two weighted automata over the field of rationals, it is decidable whether they compute the same function (Theorem B.3.3 of Transducers, Schützenberger). The book proves it through linear representations: the difference of the two automata is a weighted automaton, and by Schützenberger's rank argument it is zero on all inputs as soon as it is zero on the inputs of length less than its dimension, a finite check. The same proof works for any field whose elements are finitely representable and whose operations are computable.
1 import Lax132576.TransducerCodes 2 import Lax132576.WeightedCodes 3 … module docstring, 23 lines 27 28 namespace Lax132576.WeightedEquivalenceDecidable 29 30 open Lax132576.TransducerCodes Lax132576.WeightedCodes 31 32 /-- Equivalence of two valid coded weighted automata over `ℚ` is decidable. -/ 33 axiom decidable_wcodeEval_eq : 34 DecidableUnderPromise (fun p : WCode × WCode => WCodeValid p.1 ∧ WCodeValid p.2) 35 (fun p => wcodeEval p.1 = wcodeEval p.2) 36 37 end Lax132576.WeightedEquivalenceDecidable 38 -
def
Lax132576.WeightedCodespp. 61–62Codes of weighted automata over the rationals
The decision problems of Section B.3 of Transducers — equivalence and zeroness of weighted automata over the field of rationals — are about algorithms whose inputs are weighted automata. A weighted automaton over with states and letters in is described by a finite code: its transitions , from to , reading , with weight given by an integer and a natural number, and its lists of initial and final states. A code is valid if the automaton it describes is a genuine weighted automaton, i.e. every input string has finitely many accepting runs; validity is the promise under which the decision procedures of Theorems B.3.3 and B.3.7 are correct.
1 import Mathlib.Computability.Halting 2 import Mathlib.Data.Rat.Defs 3 import Lax132576.WeightedAutomata 4 … module docstring, 23 lines 28 29 namespace Lax132576.WeightedCodes 30 31 open Lax132576.LabelledAutomata Lax132576.WeightedAutomata 32 33 /-- A code of a weighted automaton over `ℚ`: transitions `(p, u, (a, b), q)` from 34 `p` to `q` reading `u` with weight `a / b`, and the initial and final states. -/ 35 structure WCode where 36 /-- The transitions `(p, u, (a, b), q)`. -/ 37 transitions : List (ℕ × List ℕ × (ℤ × ℕ) × ℕ) 38 /-- The initial states. -/ 39 init : List ℕ 40 /-- The final states. -/ 41 final : List ℕ 42 43 /-- A code is the tuple of its three lists. -/ 44 def wcodeEquiv : WCode ≃ List (ℕ × List ℕ × (ℤ × ℕ) × ℕ) × List ℕ × List ℕ where 45 toFun c := (c.transitions, c.init, c.final) 46 invFun x := ⟨x.1, x.2.1, x.2.2⟩ 47 left_inv := by rintro ⟨t, i, f⟩; rfl 48 right_inv := by rintro ⟨t, i, f⟩; rfl 49 50 instance : Primcodable WCode := Primcodable.ofEquiv _ wcodeEquiv 51 52 /-- The weighted automaton over `ℚ` described by a code. -/ 53 def wcodeAut (c : WCode) : LabAut ℕ ℚ ℕ where 54 init := {q | q ∈ c.init} 55 final := {q | q ∈ c.final} 56 δ := {t | ∃ s ∈ c.transitions, t = (s.1, s.2.1, (s.2.2.1.1 : ℚ) / (s.2.2.1.2 : ℚ), s.2.2.2)} 57 δ_finite := Set.Finite.ofFinset 58 (c.transitions.toFinset.image 59 (fun s => (s.1, s.2.1, (s.2.2.1.1 : ℚ) / (s.2.2.1.2 : ℚ), s.2.2.2))) 60 (by intro t; simp [eq_comm]) 61 62 /-- The function computed by the weighted automaton described by a code. -/ 63 noncomputable def wcodeEval (c : WCode) : List ℕ → ℚ := wEval (wcodeAut c) 64 65 /-- A code is valid if it describes a genuine weighted automaton: every input has 66 finitely many accepting runs. -/ 67 def WCodeValid (c : WCode) : Prop := FinitelyManyRuns (wcodeAut c) 68 69 end Lax132576.WeightedCodes 70 -
thm✓
Lax132576.RationalEquivalenceDecidablep. 62Decidable equivalence of rational functions
The equivalence problem is decidable for rational functions (Theorem B.3.4 of Transducers). The book reduces it to equivalence of weighted automata over the rationals (Theorem B.3.3): output strings are represented injectively by rational numbers through a weighted automaton , weighted automata are closed under pre-composition with rational functions (Lemma B.3.5), and exactly when .
1 import Lax132576.TransducerCodes 2 … module docstring, 21 lines 24 25 namespace Lax132576.RationalEquivalenceDecidable 26 27 open Lax132576.TransducerCodes 28 29 /-- Equivalence of two coded rational functions is decidable. -/ 30 axiom decidable_codeRel_eq : 31 DecidableUnderPromise (fun p : RelCode × RelCode => CodeFunctional p.1 ∧ CodeFunctional p.2) 32 (fun p => codeRel p.1 = codeRel p.2) 33 34 end Lax132576.RationalEquivalenceDecidable 35 -
def
Lax132576.TransducerCodesp. 62Codes of automata with output, and decidability under a promise
The decidability statements of the book are about algorithms whose inputs are automata. An automaton with output whose states and letters are natural numbers is described by a finite code: the list of its transitions — from state to state , reading and writing — and the lists of its initial and final states. A code mentions only finitely many letters, its alphabet; a string over that alphabet is a code word. A code is functional if the relation it describes is a total function on the code words: every code word has exactly one output.
A problem "given an automaton satisfying a promise, decide whether it has a property" is decidable if there is a computable Boolean-valued function on codes that answers correctly on every code satisfying the promise. This is the form of Theorems B.3.4, B.4.2 and Lemma B.4.3 (and of Theorem C.1.4 in Part C).
1 import Mathlib.Computability.Halting 2 import Lax132576.RationalRelations 3 … module docstring, 31 lines 35 36 namespace Lax132576.TransducerCodes 37 38 open Lax132576.LabelledAutomata Lax132576.RationalRelations 39 40 /-- A code of an automaton with output over the alphabet `ℕ` with states in `ℕ`: 41 its transitions `(p, u, v, q)` and its initial and final states. -/ 42 structure RelCode where 43 /-- The transitions `(p, u, v, q)`: from `p` to `q`, reading `u`, writing `v`. -/ 44 transitions : List (ℕ × List ℕ × List ℕ × ℕ) 45 /-- The initial states. -/ 46 init : List ℕ 47 /-- The final states. -/ 48 final : List ℕ 49 50 /-- A code is the tuple of its three lists. -/ 51 def relCodeEquiv : RelCode ≃ List (ℕ × List ℕ × List ℕ × ℕ) × List ℕ × List ℕ where 52 toFun c := (c.transitions, c.init, c.final) 53 invFun x := ⟨x.1, x.2.1, x.2.2⟩ 54 left_inv := by rintro ⟨t, i, f⟩; rfl 55 right_inv := by rintro ⟨t, i, f⟩; rfl 56 57 instance : Primcodable RelCode := Primcodable.ofEquiv _ relCodeEquiv 58 59 /-- The automaton with output described by a code. -/ 60 def codeAut (c : RelCode) : NFAO ℕ ℕ ℕ where 61 init := {q | q ∈ c.init} 62 final := {q | q ∈ c.final} 63 δ := {t | t ∈ c.transitions} 64 δ_finite := c.transitions.finite_toSet 65 66 /-- The rational relation described by a code. -/ 67 def codeRel (c : RelCode) : List ℕ → List ℕ → Prop := (codeAut c).rel 68 69 /-- The alphabet of a code: the letters occurring in the input strings of its 70 transitions. -/ 71 def codeAlphabet (c : RelCode) : List ℕ := c.transitions.flatMap (fun t => t.2.1) 72 73 /-- A string over the alphabet of the code. -/ 74 def CodeWord (c : RelCode) (w : List ℕ) : Prop := ∀ x ∈ w, x ∈ codeAlphabet c 75 76 /-- The relation described by the code is a total function on the code words. -/ 77 def CodeFunctional (c : RelCode) : Prop := ∀ w, CodeWord c w → ∃! v, codeRel c w v 78 79 /-- A property `P` is decidable under a promise if a computable Boolean-valued 80 function answers `P` correctly on every input satisfying the promise. -/ 81 def DecidableUnderPromise {α : Type} [Primcodable α] (promise P : α → Prop) : Prop := 82 ∃ D : α → Bool, Computable D ∧ ∀ a, promise a → (D a = true ↔ P a) 83 84 end Lax132576.TransducerCodes 85 -
⊢
Lax132576Proofs.Results.decidable_codeRel_eqpp. 62–63no assumptions
Decidable equivalence of rational functions (Theorem B.3.4), by the book's reduction to Theorem B.3.3 ().
-
thm✓
Lax132576.WeightedPrecompositionp. 62Weighted automata are closed under pre-composition with rational functions
For every semiring , the composition
of a rational function with a function computed by a weighted automaton is computed by a weighted automaton (Lemma B.3.5 of Transducers). The automaton for is first made unambiguous and ε-free (Lemmas B.2.4 and B.2.5), so that its unique run aligns with the runs of the automaton for in a product construction whose transitions carry, as weight, the sum of the weights of the runs of over the output of one transition of .
1 import Lax132576.RationalFunctions 2 import Lax132576.WeightedAutomata 3 … module docstring, 19 lines 23 24 namespace Lax132576.WeightedPrecomposition 25 26 open Lax132576.RationalFunctions Lax132576.WeightedAutomata 27 28 /-- Pre-composing a weighted function with a rational function gives a weighted 29 function. -/ 30 axiom isWeighted_comp_of_isRationalFun {A B S : Type} [Finite A] [Finite B] [Semiring S] 31 {f : List A → List B} {h : List B → S} (hf : IsRationalFun f) (hh : IsWeighted h) : 32 IsWeighted (h ∘ f) 33 34 end Lax132576.WeightedPrecomposition 35 -
no assumptions
Weighted automata are closed under pre-composition with rational functions (Lemma B.3.5), by the product with an unambiguous ε-free automaton ().
-
thm✓
Lax132576.RationalViaWeightedp. 63Rational functions characterised by weighted automata
A string-to-string function is rational if and only if weighted automata, over every semiring, are closed under pre-composition with it (Theorem B.3.6 of Transducers). The implication ⇒ is Lemma B.3.5 () and the implication ⇐ is ; this statement is their conjunction.
1 import Lax132576.RationalFunctions 2 import Lax132576.WeightedAutomata 3 … module docstring, 15 lines 19 20 namespace Lax132576.RationalViaWeighted 21 22 open Lax132576.RationalFunctions Lax132576.WeightedAutomata 23 24 /-- A function is rational if and only if every weighted automaton can be 25 pre-composed with it. -/ 26 axiom isRationalFun_iff_weighted_precomp {A B : Type} [Finite A] [Finite B] 27 (f : List A → List B) : 28 IsRationalFun f ↔ 29 ∀ (S : Type) (_ : Semiring S) (h : List B → S), IsWeighted h → IsWeighted (h ∘ f) 30 31 end Lax132576.RationalViaWeighted 32 -
Functions that weighted automata can be pre-composed with are rational
If pre-composition with a function preserves computability by weighted automata over every semiring, then is rational: the implication ⇐ of Theorem B.3.6 of Transducers, its content. The book applies the hypothesis to the weighted automaton over the semiring of regular languages that maps a string to the singleton language of itself — the rational relations are the weighted automata over that semiring — and reads a rational relation computing the graph of off the resulting automaton.
1 import Lax132576.RationalFunctions 2 import Lax132576.WeightedAutomata 3 … module docstring, 19 lines 23 24 namespace Lax132576.RationalOfWeightedPrecomposition 25 26 open Lax132576.RationalFunctions Lax132576.WeightedAutomata 27 28 /-- A function with which every weighted automaton can be pre-composed is 29 rational. -/ 30 axiom isRationalFun_of_weighted_precomp {A B : Type} [Finite A] [Finite B] 31 (f : List A → List B) 32 (h : ∀ (S : Type) (_ : Semiring S) (h : List B → S), IsWeighted h → IsWeighted (h ∘ f)) : 33 IsRationalFun f 34 35 end Lax132576.RationalOfWeightedPrecomposition 36 -
Theorem B.3.6 as a biconditional, glued from Lemma B.3.5 and its converse taken as assumptions.
-
thm✓
Lax132576.WeightedZeronessDecidablep. 64Decidable zeroness of weighted automata over the rationals
The zeroness problem — does a given weighted automaton over the field of rationals compute the constant function ? — is decidable (Theorem B.3.7 of Transducers). It is the special case of equivalence (Theorem B.3.3) in which the second automaton is empty, and conversely equivalence reduces to zeroness of the difference; the book proves the zeroness criterion, Schützenberger's bound on the length of a witness, and derives both.
1 import Lax132576.TransducerCodes 2 import Lax132576.WeightedCodes 3 … module docstring, 17 lines 21 22 namespace Lax132576.WeightedZeronessDecidable 23 24 open Lax132576.TransducerCodes Lax132576.WeightedCodes 25 26 /-- Zeroness of a valid coded weighted automaton over `ℚ` is decidable. -/ 27 axiom decidable_wcodeEval_eq_zero : 28 DecidableUnderPromise WCodeValid (fun c => wcodeEval c = 0) 29 30 end Lax132576.WeightedZeronessDecidable 31 -
no assumptions
Decidable zeroness of weighted automata over (Theorem B.3.7), the special case of equivalence with the empty automaton ().
-
def
Lax916827.TwoWayTransducerspp. 91–92Two-way transducers
A two-way transducer (Definition C.2.1 of Transducers) consists of a finite input alphabet , a finite output alphabet , a finite set of states with an initial state, and a transition function
which, on the letter to the left of the head, the current state and the letter to the right of the head (each possibly missing, at the ends of the input), either produces an output string and halts, or produces an output string, changes state and moves the head left or right. The head sits in a gap between two positions of the input; the run starts in the leftmost gap in the initial state, and the transducer computes on if the run started there halts with the concatenation of the produced outputs equal to . Since the transducer is deterministic, it computes at most one output on every input; a function is computed by a two-way transducer if its graph is.
1 import Mathlib.Data.Finite.Defs 2 … module docstring, 32 lines 35 36 namespace Lax916827.TwoWayTransducers 37 38 /-- A two-way transducer: on the letters adjacent to the head and the state, it 39 either produces an output string and halts (`Sum.inl`), or produces an output 40 string, changes state and moves the head left (`false`) or right (`true`). -/ 41 structure TwoWay (A B Q : Type) where 42 /-- The initial state. -/ 43 init : Q 44 /-- The transition function. -/ 45 step : Option A → Q → Option A → List B ⊕ (Q × List B × Bool) 46 47 /-- A configuration: the input to the left of the head, the state, and the input 48 to the right of the head; or the halting vertex. -/ 49 inductive Cfg (A Q : Type) : Type 50 | conf : List A → Q → List A → Cfg A Q 51 | halt : Cfg A Q 52 53 namespace TwoWay 54 55 variable {A B Q : Type} 56 57 /-- One step of the computation: the produced output and the next configuration, 58 if the head does not fall off the input. -/ 59 def stepCfg (M : TwoWay A B Q) : Cfg A Q → Option (List B × Cfg A Q) 60 | Cfg.halt => none 61 | Cfg.conf u q v => 62 match M.step u.getLast? q v.head? with 63 | Sum.inl o => some (o, Cfg.halt) 64 | Sum.inr (q', o, true) => 65 match v with 66 | [] => none 67 | a :: v' => some (o, Cfg.conf (u ++ [a]) q' v') 68 | Sum.inr (q', o, false) => 69 match u.getLast? with 70 | none => none 71 | some a => some (o, Cfg.conf u.dropLast q' (a :: v)) 72 73 /-- Reachability in the configuration graph, recording the produced output. -/ 74 inductive Reaches (M : TwoWay A B Q) : Cfg A Q → List B → Cfg A Q → Prop 75 | refl (c : Cfg A Q) : Reaches M c [] c 76 | step {c c' c'' : Cfg A Q} {o o' : List B} : 77 M.stepCfg c = some (o, c') → Reaches M c' o' c'' → Reaches M c (o ++ o') c'' 78 79 /-- The transducer produces the output `v` on the input `w`: the run from the 80 initial configuration reaches the halting vertex with output `v`. -/ 81 def Computes (M : TwoWay A B Q) (w : List A) (v : List B) : Prop := 82 M.Reaches (Cfg.conf [] M.init w) v Cfg.halt 83 84 /-- The configuration of the run on `w` after `n` steps; `none` once the run has 85 halted or got stuck. -/ 86 def cfgAt (M : TwoWay A B Q) (w : List A) : ℕ → Option (Cfg A Q) 87 | 0 => some (Cfg.conf [] M.init w) 88 | n + 1 => (cfgAt M w n).bind fun c => (M.stepCfg c).map Prod.snd 89 90 /-- A configuration lies on the run of `M` on `w`. -/ 91 def Visits (M : TwoWay A B Q) (w : List A) (c : Cfg A Q) : Prop := ∃ n, cfgAt M w n = some c 92 93 end TwoWay 94 95 /-- A function computed by a two-way transducer with a finite state space. -/ 96 def IsTwoWay {A B : Type} (f : List A → List B) : Prop := 97 ∃ (Q : Type) (_ : Finite Q) (M : TwoWay A B Q), ∀ w, M.Computes w (f w) 98 99 end Lax916827.TwoWayTransducers 100 -
thm✓
Lax916827.TwoWayContinuityp. 92Two-way transducers are continuous
Every function computed by a two-way transducer is continuous (Theorem C.2.2 of Transducers, Rabin–Scott and Shepherdson). The book computes the reachable configuration graph by a rational function (Lemma C.2.3) and checks membership of the output in a regular language on the representation (Lemma C.2.4); a direct proof runs a deterministic automaton for the output language inside the transducer, turning it into a two-way automaton, whose language is regular by Shepherdson's theorem.
1 import Lax765601.Continuity 2 import Lax916827.TwoWayTransducers 3 … module docstring, 17 lines 21 22 namespace Lax916827.TwoWayContinuity 23 24 open Lax765601.Continuity Lax916827.TwoWayTransducers 25 26 /-- A function computed by a two-way transducer is continuous. -/ 27 axiom continuous_of_isTwoWay {A B : Type} [Finite A] [Finite B] {f : List A → List B} 28 (hf : IsTwoWay f) : Continuous f 29 30 end Lax916827.TwoWayContinuity 31 -
no assumptions
Two-way transducers are continuous (Theorem C.2.2): the source runs a deterministic automaton for the output language inside the transducer and appeals to Shepherdson's theorem ().
-
thm✓
Lax916827.ConfigurationGraphRationalp. 94Computing the reachable configuration graph is rational
The function which maps an input string to the string representation of its reachable configuration graph is rational (Lemma C.2.3 of Transducers). The main observation is that the representations of reachable configuration graphs form a regular language — reachability is checked locally, slice by slice — so that an automaton with output can guess the representation and verify it.
1 import Lax132576.RationalFunctions 2 import Lax916827.ConfigurationGraphs 3 … module docstring, 17 lines 21 22 namespace Lax916827.ConfigurationGraphRational 23 24 open Lax132576.RationalFunctions Lax916827.TwoWayTransducers Lax916827.ConfigurationGraphs 25 26 /-- The string representation of the reachable configuration graph is a rational 27 function of the input. -/ 28 axiom isRationalFun_enc {A B Q : Type} [Finite A] [Finite Q] (M : TwoWay A B Q) : 29 IsRationalFun (TwoWay.enc M) 30 31 end Lax916827.ConfigurationGraphRational 32 -
def
Lax916827.ConfigurationGraphsp. 94The string representation of the reachable configuration graph
The proof of Theorem C.2.2 of Transducers represents the reachable configuration graph of a two-way transducer on a fixed input — the configurations on its run, with the transition between consecutive ones — as a string over a finite alphabet . The graph is sliced along the letters of the input: the slice at a letter is a bipartite graph whose vertices are two copies of the state space , one for the gap to the left of the letter and one for the gap to its right, with a directed edge, labelled by an output string, for every transition of the run that crosses the letter; each vertex has at most one outgoing edge, and it goes to the other copy of . The alphabet consists of these slices, and is finite because only the finitely many output strings occurring in the transition function label edges. A special letter represents the graph of the empty input, which has no letter to slice at.
Lemma C.2.3 says that the map from an input to the representation of its reachable configuration graph is rational; Lemma C.2.4 that the representations whose output string lies in a regular language form a regular language. The output string of a representation is read by a two-way transducer over that walks along the represented path and prints the labels it meets.
1 import Mathlib.Data.Set.Finite.Basic 2 import Lax916827.TwoWayTransducers 3 … module docstring, 39 lines 43 44 namespace Lax916827.ConfigurationGraphs 45 46 open Lax916827.TwoWayTransducers 47 48 /-- The outgoing edge of a vertex inside one slice: none, an edge to the state `q'` 49 of the other copy labelled `l`, or the halting vertex with the output `l`. -/ 50 inductive VOut (Q L : Type) where 51 /-- No outgoing edge inside this slice. -/ 52 | nil : VOut Q L 53 /-- An edge to the state `q'` of the other copy, labelled `l`. -/ 54 | move (q' : Q) (l : L) : VOut Q L 55 /-- The transducer halts here, producing `l`. -/ 56 | halt (l : L) : VOut Q L 57 58 /-- A slice of the configuration graph at a letter: the outgoing edge of every 59 vertex, `(false, q)` being the state `q` at the gap to the left of the letter and 60 `(true, q)` at the gap to its right. -/ 61 abbrev Slice (Q L : Type) := Bool × Q → VOut Q L 62 63 /-- The alphabet `C`: the slices, and the special letter for the empty input, 64 carrying the output of the halting transition on the empty input if the run 65 halts there. -/ 66 abbrev CLet (Q L : Type) := Slice Q L ⊕ Option L 67 68 namespace TwoWay 69 70 variable {A B Q : Type} 71 72 /-- The output string produced by a transition. -/ 73 def transOut (M : TwoWay A B Q) (l : Option A) (q : Q) (r : Option A) : List B := 74 match M.step l q r with 75 | Sum.inl o => o 76 | Sum.inr (_, o, _) => o 77 78 /-- The output strings occurring in the transition function. -/ 79 def OutLabels (M : TwoWay A B Q) : Set (List B) := 80 Set.range (fun p : Option A × Q × Option A => transOut M p.1 p.2.1 p.2.2) 81 82 /-- The finite set of edge labels: the output strings of the transitions. -/ 83 abbrev Lab (M : TwoWay A B Q) : Type := {o : List B // o ∈ OutLabels M} 84 85 /-- The label of the edge produced by a transition. -/ 86 def labOf (M : TwoWay A B Q) (l : Option A) (q : Q) (r : Option A) : Lab M := 87 ⟨transOut M l q r, ⟨(l, q, r), rfl⟩⟩ 88 89 /-- The outgoing edge recorded, in the direction `d`, for the state `q` at a gap 90 with adjacent letters `l` and `r`: the left copy of a slice records the 91 transitions moving right, the right copy those moving left, and a halting 92 transition is recorded on both copies of its gap. -/ 93 def edgeOf (M : TwoWay A B Q) (l : Option A) (q : Q) (r : Option A) (d : Bool) : VOut Q (Lab M) := 94 match M.step l q r with 95 | Sum.inl _ => VOut.halt (labOf M l q r) 96 | Sum.inr (q', _, dir) => if dir = d then VOut.move q' (labOf M l q r) else VOut.nil 97 98 /-- The letter to the left of the gap `j` of `w`, if any. -/ 99 def prevAt (w : List A) (j : ℕ) : Option A := if j = 0 then none else w[j - 1]? 100 101 open scoped Classical in 102 /-- The outgoing edge, in the direction `d`, of the state `q` at the gap `j` of 103 `w`, for the *reachable* configurations only: a configuration the run does not 104 visit has no edge. -/ 105 noncomputable def cutV (M : TwoWay A B Q) (w : List A) (j : ℕ) (q : Q) (d : Bool) : 106 VOut Q (Lab M) := 107 if M.Visits w (Cfg.conf (w.take j) q (w.drop j)) then edgeOf M (prevAt w j) q w[j]? d 108 else VOut.nil 109 110 /-- The slice of the reachable configuration graph of `M` on `w` at the letter of 111 position `i`. -/ 112 noncomputable def encSlice (M : TwoWay A B Q) (w : List A) (i : ℕ) : Slice Q (Lab M) := 113 fun v => cutV M w (if v.1 then i + 1 else i) v.2 (!v.1) 114 115 /-- The special letter for the empty input: the output of the halting transition on 116 the empty input, if the run on the empty input halts at once. -/ 117 def emptyOut (M : TwoWay A B Q) : Option (Lab M) := 118 match M.step none M.init none with 119 | Sum.inl _ => some (labOf M none M.init none) 120 | Sum.inr _ => none 121 122 /-- The string representation of the reachable configuration graph of `M` on `w`: 123 one slice per input letter, and the special letter for the empty input. -/ 124 noncomputable def enc (M : TwoWay A B Q) (w : List A) : List (CLet Q (Lab M)) := 125 if w.isEmpty then [Sum.inr (emptyOut M)] 126 else (List.range w.length).map (fun i => Sum.inl (encSlice M w i)) 127 128 variable {L : Type} 129 130 /-- The outgoing edge at the current gap recorded by the letter to the right of 131 the head. -/ 132 def readR (r : Option (CLet Q L)) (q : Q) : VOut Q L := 133 match r with 134 | some (Sum.inl s) => s (false, q) 135 | some (Sum.inr (some lab)) => VOut.halt lab 136 | _ => VOut.nil 137 138 /-- The outgoing edge at the current gap recorded by the letter to the left of the 139 head. -/ 140 def readL (l : Option (CLet Q L)) (q : Q) : VOut Q L := 141 match l with 142 | some (Sum.inl s) => s (true, q) 143 | _ => VOut.nil 144 145 /-- The two-way transducer over `C` that walks along the path of a represented 146 configuration graph, printing the labels of the edges it follows; on a string 147 that represents nothing it halts with empty output. -/ 148 def pathTrans (M : TwoWay A B Q) : TwoWay (CLet Q (Lab M)) B Q where 149 init := M.init 150 step := fun l q r => 151 match readR r q with 152 | VOut.move q' lab => Sum.inr (q', lab.val, true) 153 | VOut.halt lab => Sum.inl lab.val 154 | VOut.nil => 155 match readL l q with 156 | VOut.move q' lab => Sum.inr (q', lab.val, false) 157 | VOut.halt lab => Sum.inl lab.val 158 | VOut.nil => Sum.inl [] 159 160 end TwoWay 161 162 end Lax916827.ConfigurationGraphs 163 -
⊢
Lax916827Proofs.Results.isRationalFun_encpp. 94–95no assumptions
The string representation of the reachable configuration graph is a rational function of the input (Lemma C.2.3), .
-
thm✓
Lax916827.ConfigurationGraphOutputp. 95Checking the output of a configuration graph against a regular language
For a regular language over the output alphabet, the set of strings over that represent a reachable configuration graph whose output string belongs to is a regular language (Lemma C.2.4 of Transducers). An automaton checks that the string is a representation and guesses a labelling of the edges of the represented path by transitions of an automaton for .
1 import Mathlib.Computability.DFA 2 import Lax916827.ConfigurationGraphs 3 … module docstring, 19 lines 23 24 namespace Lax916827.ConfigurationGraphOutput 25 26 open Lax916827.TwoWayTransducers Lax916827.ConfigurationGraphs 27 28 /-- The representations of reachable configuration graphs whose output lies in a 29 regular language form a regular language. -/ 30 axiom isRegular_encOutputLang {A B Q : Type} [Finite A] [Finite Q] (M : TwoWay A B Q) 31 {f : List A → List B} (hM : ∀ w, M.Computes w (f w)) {L : Language B} (hL : L.IsRegular) : 32 Language.IsRegular {u : List (CLet Q (TwoWay.Lab M)) | 33 (∃ w, u = TwoWay.enc M w) ∧ ∃ v, (TwoWay.pathTrans M).Computes u v ∧ v ∈ L} 34 35 end Lax916827.ConfigurationGraphOutput 36 -
no assumptions
The representations whose output lies in a regular language form a regular language (Lemma C.2.4), .
-
thm✓
Lax916827.TwoWayCompositionp. 95Two-way transducers are closed under composition
Functions computed by two-way transducers are closed under composition (Theorem C.2.5 of Transducers, Chytil and Jákl). The composed transducer computes the reachable configuration graph of the first transducer by a rational function (Lemma C.2.3), which two-way transducers can be pre-composed with (Corollary C.2.7), and then simulates the second transducer on the represented path, walking backwards along the path — which is possible because the run of a deterministic transducer never revisits a configuration — when the second transducer moves left.
1 import Lax916827.TwoWayTransducers 2 … module docstring, 18 lines 21 22 namespace Lax916827.TwoWayComposition 23 24 open Lax916827.TwoWayTransducers 25 26 /-- The composition of two functions computed by two-way transducers is computed by 27 a two-way transducer. -/ 28 axiom isTwoWay_comp {A B C : Type} [Finite A] [Finite B] [Finite C] 29 {f : List A → List B} {g : List B → List C} (hf : IsTwoWay f) (hg : IsTwoWay g) : 30 IsTwoWay (g ∘ f) 31 32 end Lax916827.TwoWayComposition 33 -
⊢
Lax916827Proofs.Results.isTwoWay_comppp. 95–97no assumptions
Two-way transducers are closed under composition (Theorem C.2.5), : the second transducer is simulated on the run of the first, walking backwards along the run when it moves left.
-
thm✓
Lax916827.TwoWayMealyPrecompositionp. 96Two-way transducers are closed under pre-composition with Mealy machines
Functions computed by two-way transducers are closed under pre-composition with Mealy machines (Lemma C.2.6 of Transducers). By the Krohn–Rhodes theorem it suffices to pre-compose with a reversible and with a flip-flop machine: a reversible machine can be run backwards, so its state at the head can be maintained when the head moves left; a flip-flop machine's state at a position is determined by the last resetting letter before it, which the two-way transducer finds by a detour to the left.
1 import Lax765601.MealyMachine 2 import Lax916827.TwoWayTransducers 3 … module docstring, 17 lines 21 22 namespace Lax916827.TwoWayMealyPrecomposition 23 24 open Lax765601.MealyMachine Lax916827.TwoWayTransducers 25 26 /-- Pre-composing a two-way transducer with a Mealy machine gives a two-way 27 transducer. -/ 28 axiom isTwoWay_comp_isMealy {A B C : Type} [Finite A] [Finite B] [Finite C] 29 {f : List A → List B} {g : List B → List C} (hf : IsMealy f) (hg : IsTwoWay g) : 30 IsTwoWay (g ∘ f) 31 32 end Lax916827.TwoWayMealyPrecomposition 33 -
no assumptions
Two-way transducers are closed under pre-composition with Mealy machines (Lemma C.2.6): the Krohn–Rhodes decomposition of Part A reduces to reversible and flip-flop machines (); Part A's bridge transports .
-
thm✓
Lax916827.TwoWayRationalPrecompositionpp. 96–97Two-way transducers are closed under pre-composition with rational functions
Functions computed by two-way transducers are closed under pre-composition with rational functions (Corollary C.2.7 of Transducers). By Theorem B.2.6 a rational function is a composition of prime Mealy machines, their right-to-left variants, homomorphisms and the separator function; Lemma C.2.6 handles the Mealy machines, a right-to-left machine is handled symmetrically, and a homomorphism is handled by simulating the head inside the image of a letter.
1 import Lax132576.RationalFunctions 2 import Lax916827.TwoWayTransducers 3 … module docstring, 16 lines 20 21 namespace Lax916827.TwoWayRationalPrecomposition 22 23 open Lax132576.RationalFunctions Lax916827.TwoWayTransducers 24 25 /-- Pre-composing a two-way transducer with a rational function gives a two-way 26 transducer. -/ 27 axiom isTwoWay_comp_isRationalFun {A B C : Type} [Finite A] [Finite B] [Finite C] 28 {f : List A → List B} {g : List B → List C} (hf : IsRationalFun f) (hg : IsTwoWay g) : 29 IsTwoWay (g ∘ f) 30 31 end Lax916827.TwoWayRationalPrecomposition 32 -
no assumptions
Two-way transducers are closed under pre-composition with rational functions (Corollary C.2.7), through the prime decomposition of Theorem B.2.6 (); Part B's bridge transports .
-
thm✓
Lax916827.TwoWayOfRegularp. 97Every regular function is computed by a two-way transducer
Every regular function is computed by a two-way transducer (Corollary C.2.8 of Transducers). Two-way transducers are closed under composition (Theorem C.2.5) and contain the rational functions (Corollary C.2.7), and map reverse and map duplicate are computed by explicit two-way transducers that sweep each block backwards, respectively twice.
1 import Lax916827.RegularFunctions 2 import Lax916827.TwoWayTransducers 3 … module docstring, 16 lines 20 21 namespace Lax916827.TwoWayOfRegular 22 23 open Lax916827.RegularFunctions Lax916827.TwoWayTransducers 24 25 /-- A regular function is computed by a two-way transducer. -/ 26 axiom isTwoWay_of_isRegularFun {A B : Type} [Finite A] [Finite B] {f : List A → List B} 27 (hf : IsRegularFun f) : IsTwoWay f 28 29 end Lax916827.TwoWayOfRegular 30 -
no assumptions
Every regular function is computed by a two-way transducer (Corollary C.2.8): induction on the composition tree with Theorem C.2.5 and Corollary C.2.7, and explicit two-way transducers for map reverse and map duplicate ().
-
thm✓
Lax916827.TwoWayIffRegularp. 98Two-way transducers compute exactly the regular functions
A string-to-string function is computed by a two-way transducer if and only if it is regular (Theorem C.2.9 of Transducers). The two implications are the separate statements (Corollary C.2.8) and (the decomposition into primes through the snake lemma); this statement is their conjunction.
1 import Lax916827.RegularFunctions 2 import Lax916827.TwoWayTransducers 3 … module docstring, 15 lines 19 20 namespace Lax916827.TwoWayIffRegular 21 22 open Lax916827.RegularFunctions Lax916827.TwoWayTransducers 23 24 /-- A function is computed by a two-way transducer if and only if it is regular. -/ 25 axiom isTwoWay_iff_isRegularFun {A B : Type} [Finite A] [Finite B] (f : List A → List B) : 26 IsTwoWay f ↔ IsRegularFun f 27 28 end Lax916827.TwoWayIffRegular 29 -
thm✓
Lax916827.RegularOfTwoWayp. 98Every two-way transducer computes a regular function
Every function computed by a two-way transducer is regular, i.e. decomposes into rational functions, map reverse and map duplicate (Theorem C.2.9 of Transducers, the hard implication). The run of the transducer is described by its snake graph, computed by a rational function, and the output of a snake graph of width at most is a regular function of its representation (the snake lemma, Lemma C.2.12), by induction on the width: a snake of width is cut, at the record-breaking columns, into looping and progressing parts of smaller width, whose outputs are computed by the induction hypothesis on factors cut out by rational functions and glued back by the closure properties of Lemma C.2.10. A run that halts visits every column at most times, so the transducer's function is its own width- snake output.
1 import Lax916827.RegularFunctions 2 import Lax916827.TwoWayTransducers 3 … module docstring, 21 lines 25 26 namespace Lax916827.RegularOfTwoWay 27 28 open Lax916827.RegularFunctions Lax916827.TwoWayTransducers 29 30 /-- A function computed by a two-way transducer is regular. -/ 31 axiom isRegularFun_of_isTwoWay {A B : Type} [Finite A] [Finite B] {f : List A → List B} 32 (hf : IsTwoWay f) : IsRegularFun f 33 34 end Lax916827.RegularOfTwoWay 35 -
Theorem C.2.9 as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax916827.RegularMapLiftingpp. 98–99Regular functions are closed under map lifting
The map lifting of a regular function is regular (Lemma C.2.10 of Transducers, first item). Map lifting commutes with composition, so it suffices to lift the primes: the map lifting of a rational function is rational, and the map liftings of map reverse and map duplicate are regular.
1 import Lax765601.MapLifting 2 import Lax916827.RegularFunctions 3 … module docstring, 14 lines 18 19 namespace Lax916827.RegularMapLifting 20 21 open Lax765601.MapLifting Lax916827.RegularFunctions 22 23 /-- The map lifting of a regular function is regular. -/ 24 axiom isRegularFun_mapLift {A B : Type} [Finite A] [Finite B] {f : List A → List B} 25 (hf : IsRegularFun f) : IsRegularFun (mapLift f) 26 27 end Lax916827.RegularMapLifting 28 -
thm✓
Lax916827.RegularConcatenationpp. 98–99Regular functions are closed under concatenation
If are regular, then so is their concatenation (Lemma C.2.10 of Transducers, second item): map duplicate produces two copies of the input, and the map liftings of and of are applied to the two copies, selected by a rational marking.
1 import Lax916827.RegularFunctions 2 … module docstring, 14 lines 17 18 namespace Lax916827.RegularConcatenation 19 20 open Lax916827.RegularFunctions 21 22 /-- The concatenation of two regular functions is regular. -/ 23 axiom isRegularFun_concat {A B : Type} [Finite A] [Finite B] {f g : List A → List B} 24 (hf : IsRegularFun f) (hg : IsRegularFun g) : IsRegularFun (fun w => f w ++ g w) 25 26 end Lax916827.RegularConcatenation 27 -
thm✓
Lax916827.RegularConditionalpp. 98–99Regular functions are closed under conditionals over regular languages
If are regular and is regular, then the conditional function
is regular (Lemma C.2.10 of Transducers, third item): a rational function marks the input with its membership in , and the marked sum of Claim C.2.11 applies or according to the mark.
1 import Mathlib.Computability.DFA 2 import Lax916827.RegularFunctions 3 … module docstring, 18 lines 22 23 namespace Lax916827.RegularConditional 24 25 open Lax916827.RegularFunctions 26 27 open scoped Classical in 28 /-- The conditional of two regular functions over a regular language is regular. -/ 29 axiom isRegularFun_ite {A B : Type} [Finite A] [Finite B] {f g : List A → List B} 30 (hf : IsRegularFun f) (hg : IsRegularFun g) (L : Language A) (hL : L.IsRegular) : 31 IsRegularFun (fun w => if w ∈ L then f w else g w) 32 33 end Lax916827.RegularConditional 34 -
⊢
Lax916827Proofs.Results.isRegularFun_mapLiftpp. 99–100no assumptions
Regular functions are closed under map lifting (Lemma C.2.10, first item): map lifting commutes with composition and the primes lift (, first conjunct), through Part A's .
-
thm✓
Lax916827.RegularSump. 99The sum of two regular functions on disjoint alphabets
For regular functions and with disjoint input and output alphabets, the function on is regular (Claim C.2.11 of Transducers): it applies to the inputs using only letters of , to those using only letters of , and returns a fixed string using both output alphabets otherwise. The claim is what the closure properties of Lemma C.2.10 rest on.
1 import Lax916827.RegularFunctions 2 … module docstring, 23 lines 26 27 namespace Lax916827.RegularSum 28 29 open Lax916827.RegularFunctions 30 31 /-- The sum `f₁ + f₂` of two regular functions on disjoint alphabets is regular, 32 with a bottom value on mixed inputs (and the two clauses required on nonempty 33 inputs). -/ 34 axiom exists_isRegularFun_sum {A₁ A₂ B₁ B₂ : Type} [Finite A₁] [Finite A₂] [Finite B₁] [Finite B₂] 35 [Nonempty B₁] [Nonempty B₂] {f₁ : List A₁ → List B₁} {f₂ : List A₂ → List B₂} 36 (hf₁ : IsRegularFun f₁) (hf₂ : IsRegularFun f₂) : 37 ∃ (bot : List (B₁ ⊕ B₂)) (F : List (A₁ ⊕ A₂) → List (B₁ ⊕ B₂)), 38 (∃ b₁, Sum.inl b₁ ∈ bot) ∧ (∃ b₂, Sum.inr b₂ ∈ bot) ∧ 39 IsRegularFun F ∧ 40 (∀ u : List A₁, u ≠ [] → F (u.map Sum.inl) = (f₁ u).map Sum.inl) ∧ 41 (∀ u : List A₂, u ≠ [] → F (u.map Sum.inr) = (f₂ u).map Sum.inr) ∧ 42 (∀ w, (¬ ∃ u : List A₁, w = u.map Sum.inl) → (¬ ∃ u : List A₂, w = u.map Sum.inr) → 43 F w = bot) 44 45 end Lax916827.RegularSum 46 -
no assumptions
The sum of two regular functions on disjoint alphabets is regular (Claim C.2.11, corrected on the empty input), .
-
thm✓
Lax916827.SnakeLemmapp. 100–101The snake lemma: the output of a snake graph is a regular function
Let be the alphabet representing snake graphs with states and output alphabet . For every , the function mapping a string to the output of the snake graph it represents, if it represents a snake graph of width at most , and to otherwise, is regular (Lemma C.2.12 of Transducers, the book's snake lemma). The proof is an induction on the width: a snake of width visits the record-breaking columns, the ones it reaches for the first time further right than ever before; between two consecutive record-breakers the snake consists of a looping part and a progress part, both of width below , whose outputs are given by the induction hypothesis on factors cut out by rational functions, and the closure properties of Lemma C.2.10 glue them together.
1 import Lax916827.RegularFunctions 2 import Lax916827.SnakeGraphs 3 … module docstring, 27 lines 31 32 namespace Lax916827.SnakeLemma 33 34 open Lax916827.RegularFunctions Lax916827.SnakeGraphs 35 36 /-- The output of a snake graph of width at most `k`, read off its string 37 representation, is a regular function. -/ 38 axiom isRegularFun_snakeOut {Q B : Type} [Finite Q] [Finite B] (k : ℕ) : 39 IsRegularFun (snakeOut (Q := Q) (B := B) k) 40 41 end Lax916827.SnakeLemma 42 -
def
Lax916827.SnakeGraphspp. 100–101Snake graphs and their outputs
A snake graph with states , length and output alphabet (Section C.2.4 of Transducers) is a directed graph with edges labelled by whose vertices are pairs of a row and a column , in which edges only go between adjacent columns and all edges lie on a single directed path. The output of a snake graph is the concatenation of the labels along that path, the extra label of contributing nothing; its width is the largest number of times the path visits one column. Like configuration graphs, snake graphs are represented as strings over a finite alphabet once the state set is fixed: a letter is a bipartite graph on two copies of describing the edges between two adjacent columns. The book's snake lemma (Lemma C.2.12) says that for every the function mapping a string over to the output of the snake graph it represents, if it represents one of width at most , and to otherwise, is regular; this is the induction on the width by which two-way transducers are decomposed into primes.
1 import Mathlib.Data.Set.Card 2 … module docstring, 35 lines 38 39 namespace Lax916827.SnakeGraphs 40 41 /-- The alphabet `C` of snake letters for the state set `Q` and output alphabet `B`: 42 a letter gives, for every vertex of the two copies of `Q`, its outgoing edge to 43 the other copy with a label in `B + 1`, if any. -/ 44 abbrev SnakeLetter (Q B : Type) := Bool × Q → Option (Q × Option B) 45 46 /-- A vertex of a snake graph: a row `q` and a column `i`. -/ 47 abbrev Vtx (Q : Type) := Q × ℕ 48 49 /-- The edge relation of the graph represented by `w`: an edge from `v` to `v'` 50 labelled `o` is recorded by the letter between their columns, read from the left 51 copy when `v'` is in the next column and from the right copy when it is in the 52 previous one. -/ 53 def Edge {Q B : Type} (w : List (SnakeLetter Q B)) (v v' : Vtx Q) (o : Option B) : Prop := 54 (v'.2 = v.2 + 1 ∧ ∃ c, w[v.2]? = some c ∧ c (false, v.1) = some (v'.1, o)) ∨ 55 (v.2 = v'.2 + 1 ∧ ∃ c, w[v'.2]? = some c ∧ c (true, v.1) = some (v'.1, o)) 56 57 /-- The vertex `v` carries an edge, incoming or outgoing. -/ 58 def Incident {Q B : Type} (w : List (SnakeLetter Q B)) (v : Vtx Q) : Prop := 59 (∃ v' o, Edge w v v' o) ∨ (∃ u o, Edge w u v o) 60 61 /-- All edges of the graph represented by `w` lie on the single directed path 62 `p 0, …, p m` with pairwise distinct vertices and edge labels `lab`: this is 63 what makes the graph a snake graph. -/ 64 structure IsSnakePath {Q B : Type} (w : List (SnakeLetter Q B)) (m : ℕ) (p : ℕ → Vtx Q) 65 (lab : ℕ → Option B) : Prop where 66 /-- Consecutive vertices of the path are joined by an edge with the recorded 67 label. -/ 68 edge : ∀ t < m, Edge w (p t) (p (t + 1)) (lab t) 69 /-- The vertices of the path are pairwise distinct. -/ 70 inj : ∀ s ≤ m, ∀ t ≤ m, p s = p t → s = t 71 /-- Every edge of the graph is an edge of the path. -/ 72 covers : ∀ v v' o, Edge w v v' o → ∃ t < m, p t = v ∧ p (t + 1) = v' ∧ lab t = o 73 74 /-- The output along a path: the concatenation of the labels of its edges, the 75 label `none` contributing nothing. -/ 76 def pathOut {B : Type} (lab : ℕ → Option B) (m : ℕ) : List B := 77 ((List.range m).map (fun t => (lab t).toList)).flatten 78 79 /-- `v` is the output of the snake graph represented by `w`. -/ 80 def SnakeOutIs {Q B : Type} (w : List (SnakeLetter Q B)) (v : List B) : Prop := 81 ∃ m p lab, IsSnakePath w m p lab ∧ v = pathOut lab m 82 83 /-- The number of times the snake visits the column `i`: the number of vertices of 84 that column carrying an edge. -/ 85 noncomputable def colVisits {Q B : Type} (w : List (SnakeLetter Q B)) (i : ℕ) : ℕ := 86 {q : Q | Incident w (q, i)}.ncard 87 88 /-- The width of the represented graph is at most `k`. -/ 89 def SnakeWidthLe {Q B : Type} (w : List (SnakeLetter Q B)) (k : ℕ) : Prop := 90 ∀ i, colVisits w i ≤ k 91 92 open Classical in 93 /-- The function of the snake lemma: the output of the snake graph represented by 94 `w`, if `w` represents one of width at most `k`, and the empty string otherwise. 95 -/ 96 noncomputable def snakeOut {Q B : Type} (k : ℕ) (w : List (SnakeLetter Q B)) : List B := 97 if h : SnakeWidthLe w k ∧ ∃ v, SnakeOutIs w v then h.2.choose else [] 98 99 end Lax916827.SnakeGraphs 100 -
⊢
Lax916827Proofs.Results.isRegularFun_snakeOutpp. 101–103no assumptions
The snake lemma (Lemma C.2.12): the output of a snake graph of width at most , read off its string representation, is a regular function ().
-
def
Lax709149.Typesp. 138Types and their string representation
The types of Section C.5 of Transducers (Definition C.5.1) are the expressions built from the unit type , which has the unique element , by the product , the co-product and the list type . Every element of a type has a string representation over a fixed alphabet with eight letters
defined by induction on the type: the unique element of is , an element of is or , a pair is , and a list is . Through this representation, type-to-type functions can be computed by string-to-string transducers (Definition C.5.2).
1 import Mathlib.Data.Fintype.Basic 2 import Mathlib.Tactic.DeriveFintype 3 … module docstring, 23 lines 27 28 namespace Lax709149.Types 29 30 /-- A type: built from the unit type by product, co-product and list. -/ 31 inductive Ty : Type 32 | one : Ty 33 | prod : Ty → Ty → Ty 34 | sum : Ty → Ty → Ty 35 | list : Ty → Ty 36 deriving DecidableEq 37 38 /-- The set of elements of a type. -/ 39 def Ty.Elt : Ty → Type 40 | .one => Unit 41 | .prod A B => A.Elt × B.Elt 42 | .sum A B => A.Elt ⊕ B.Elt 43 | .list A => List A.Elt 44 45 /-- The alphabet with eight letters `(`, `)`, `[`, `]`, `,`, `1`, `L`, `R`. -/ 46 inductive Sym8 : Type 47 | lpar | rpar | lbrack | rbrack | comma | one | left | right 48 deriving DecidableEq, Fintype 49 50 /-- The entries of a list representation, separated by commas. -/ 51 def joinSep : List (List Sym8) → List Sym8 52 | [] => [] 53 | [x] => x 54 | x :: xs => x ++ Sym8.comma :: joinSep xs 55 56 /-- The string representation of an element: `1` for the unit, `L a` and `R b` for 57 the co-product, `(a,b)` for a pair, `[a₁,…,aₙ]` for a list. -/ 58 def Ty.repr : (t : Ty) → t.Elt → List Sym8 59 | .one, _ => [Sym8.one] 60 | .prod A B, x => Sym8.lpar :: (A.repr x.1 ++ Sym8.comma :: (B.repr x.2 ++ [Sym8.rpar])) 61 | .sum A B, x => Sum.elim (fun a => Sym8.left :: A.repr a) (fun b => Sym8.right :: B.repr b) x 62 | .list A, l => Sym8.lbrack :: (joinSep (l.map A.repr) ++ [Sym8.rbrack]) 63 64 end Lax709149.Types 65 -
def
Lax709149.RegularUnderRepresentationp. 139Regular functions on types under string representation
A type-to-type function is regular under string representation (Definition C.5.2 of Transducers) if there is a regular string-to-string function over the eight-letter alphabet making the square commute: maps the representation of to the representation of , for every . Rational functions between types are defined in the same way. Nothing is required of on the strings that represent no element.
1 import Lax132576.RationalFunctions 2 import Lax916827.RegularFunctions 3 import Lax709149.Types 4 … module docstring, 18 lines 23 24 namespace Lax709149.RegularUnderRepresentation 25 26 open Lax132576.RationalFunctions Lax916827.RegularFunctions Lax709149.Types 27 28 /-- A type-to-type function is regular under string representation if a regular 29 string-to-string function maps the representation of `a` to the representation 30 of `f a`. -/ 31 def IsRegularUnderRepr {A B : Ty} (f : A.Elt → B.Elt) : Prop := 32 ∃ f' : List Sym8 → List Sym8, IsRegularFun f' ∧ ∀ a : A.Elt, f' (A.repr a) = B.repr (f a) 33 34 /-- A type-to-type function is rational under string representation. -/ 35 def IsRationalUnderRepr {A B : Ty} (f : A.Elt → B.Elt) : Prop := 36 ∃ f' : List Sym8 → List Sym8, IsRationalFun f' ∧ ∀ a : A.Elt, f' (A.repr a) = B.repr (f a) 37 38 end Lax709149.RegularUnderRepresentation 39 -
def
Lax709149.RegularTermspp. 140–141Regular terms
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 , the projections and , the co-projections and , distributivity , the list constructor and deconstructor , reverse , concatenation , split , and group prefix multiplication for a group whose underlying set is a finite type. The combinators are composition, pairing , co-pairing , and map . 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.
1 import Mathlib.Algebra.Group.Defs 2 import Mathlib.Data.Finite.Defs 3 import Lax709149.Types 4 … module docstring, 28 lines 33 34 namespace Lax709149.RegularTerms 35 36 open Lax709149.Types 37 38 /-- The prefix products of a list: the `i`-th entry of the output is the product of 39 the first `i` entries of the input. -/ 40 def 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 43 entries from `A` before the first cut, and the cutting entries each with the block 44 that follows it. -/ 45 def 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. -/ 51 inductive 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. -/ 86 def 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. -/ 108 def IsRegularTermFun {A B : Ty} (f : A.Elt → B.Elt) : Prop := ∃ t : RegTerm A B, t.eval = f 109 110 end Lax709149.RegularTerms 111 -
thm✓
Lax709149.RegularOfTermp. 141Regular terms define regular functions
Every type-to-type function defined by a regular term is regular under string representation (Theorem C.5.4 of Transducers, the implication from terms to regular functions). The proof is an induction on the term: every atomic term is computed, on representations, by a rational or a regular string-to-string function — reading a representation with a bracket counter capped at the height of the type — and the four combinators preserve regularity under representation, composition by Theorem C.1.1, pairing and co-pairing through the closure properties of Lemma C.2.10, and map through map lifting.
1 import Lax709149.RegularUnderRepresentation 2 import Lax709149.RegularTerms 3 … module docstring, 20 lines 24 25 namespace Lax709149.RegularOfTerm 26 27 open Lax709149.Types Lax709149.RegularUnderRepresentation Lax709149.RegularTerms 28 29 /-- A function defined by a regular term is regular under string representation. -/ 30 axiom isRegularUnderRepr_of_isRegularTermFun {A B : Ty} {f : A.Elt → B.Elt} 31 (hf : IsRegularTermFun f) : IsRegularUnderRepr f 32 33 end Lax709149.RegularOfTerm 34 -
Transducers, Part C: Regular Functions, Two-Way Transducers and Streaming String Transducers
-
def
Lax916827.RegularFunctionsp. 84Regular functions
The map reverse function is the map lifting of string reversal, applied blockwise between separators, and the map duplicate function is the map lifting of string duplication :
Neither is rational. A string-to-string function is regular (Definition C.0.1 of Transducers) if it can be obtained as a finite composition of functions each of which is a rational function, a map reverse function or a map duplicate function. The regular functions are the third step of the transducer ladder; Part C shows that they are the functions of two-way transducers, of streaming string transducers, of string-to-string mso transductions and of regular terms.
1 import Lax765601.MapLifting 2 import Lax765601.CompositionClosure 3 import Lax132576.RationalFunctions 4 … module docstring, 26 lines 31 32 namespace Lax916827.RegularFunctions 33 34 open Lax765601.MapLifting Lax765601.CompositionClosure Lax132576.RationalFunctions 35 36 /-- The map reverse function `w₁ # ⋯ # wₙ ↦ reverse w₁ # ⋯ # reverse wₙ`. -/ 37 def mapReverse (A : Type) : List (Option A) → List (Option A) := mapLift List.reverse 38 39 /-- The map duplicate function `w₁ # ⋯ # wₙ ↦ w₁w₁ # ⋯ # wₙwₙ`. -/ 40 def mapDuplicate (A : Type) : List (Option A) → List (Option A) := mapLift (fun w => w ++ w) 41 42 /-- The family of prime regular functions: rational functions, and the map reverse 43 and map duplicate functions, up to a renaming of the alphabets. -/ 44 def RegularFam : Family := fun A B f => 45 IsRationalFun f ∨ 46 (∃ (A₀ : Type) (e : A ≃ Option A₀) (e' : B ≃ Option A₀), 47 ∀ w, f w = (mapReverse A₀ (w.map e)).map e'.symm) ∨ 48 (∃ (A₀ : Type) (e : A ≃ Option A₀) (e' : B ≃ Option A₀), 49 ∀ w, f w = (mapDuplicate A₀ (w.map e)).map e'.symm) 50 51 /-- A string-to-string function is regular if it is a finite composition of 52 rational functions, map reverse and map duplicate. -/ 53 def IsRegularFun {A B : Type} (f : List A → List B) : Prop := CompClosure RegularFam A B f 54 55 end Lax916827.RegularFunctions 56 -
thm✓
Lax314295.BuchiTheoremp. 118Büchi's theorem: regular languages are the MSO-definable ones
A language is regular if and only if it is definable in monadic second-order logic (Theorem C.4.1 of Transducers, Büchi, Elgot and Trakhtenbrot). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax314295.MSOLogic 2 … module docstring, 15 lines 18 19 namespace Lax314295.BuchiTheorem 20 21 open Lax314295.MSOLogic 22 23 /-- A language is regular if and only if it is mso-definable. -/ 24 axiom isRegular_iff_msoDefinable {A : Type} [Finite A] (L : Language A) : 25 L.IsRegular ↔ MSODefinable L 26 27 end Lax314295.BuchiTheorem 28 -
thm✓
Lax314295.MSODefinableOfRegularp. 118Regular languages are MSO-definable
Every regular language is definable in monadic second-order logic (Theorem C.4.1 of Transducers, Büchi–Elgot–Trakhtenbrot, the implication from regular to definable). The formula guesses the run of a deterministic automaton on the input as one set variable per state, and checks that the sets partition the positions, that the first position carries the initial state's successor, that consecutive positions follow the transition function, and that the last position leads to an accepting state.
1 import Lax314295.MSOLogic 2 … module docstring, 17 lines 20 21 namespace Lax314295.MSODefinableOfRegular 22 23 open Lax314295.MSOLogic 24 25 /-- A regular language is definable in mso. -/ 26 axiom msoDefinable_of_isRegular {A : Type} [Finite A] {L : Language A} (hL : L.IsRegular) : 27 MSODefinable L 28 29 end Lax314295.MSODefinableOfRegular 30 -
thm✓
Lax314295.RegularOfMSODefinablep. 118MSO-definable languages are regular
Every language definable in monadic second-order logic is regular (Theorem C.4.1 of Transducers, Büchi–Elgot–Trakhtenbrot, the implication from definable to regular). It follows from Lemma C.4.2 on formulas with free variables, by induction on the formula: the annotated strings satisfying a formula form a regular language, Boolean connectives are Boolean operations on languages, and a quantifier is a projection of the annotation.
1 import Lax314295.MSOLogic 2 … module docstring, 16 lines 19 20 namespace Lax314295.RegularOfMSODefinable 21 22 open Lax314295.MSOLogic 23 24 /-- An mso-definable language is regular. -/ 25 axiom isRegular_of_msoDefinable {A : Type} [Finite A] {L : Language A} (hL : MSODefinable L) : 26 L.IsRegular 27 28 end Lax314295.RegularOfMSODefinable 29 -
def
Lax314295.MSOLogicp. 118Monadic second-order logic on strings
A string is a structure whose universe is the set of positions of , with the order on positions and, for every letter , the unary predicate "position carries the letter ". Monadic second-order logic (mso) has first-order variables ranging over positions and second-order variables ranging over sets of positions, the atomic formulas , and , Boolean connectives, and existential quantification over both kinds of variables (Section C.4.1 of Transducers). A sentence — a formula without free variables — defines the language of the strings that satisfy it; the first-order fragment is the set of formulas that use neither set variables nor membership. A formula with free variables is evaluated on a string together with a valuation, which the book represents by annotating the string: the string over the alphabet carries at every position the bits saying which of the variables point to it.
1 import Mathlib.Computability.DFA 2 import Mathlib.Data.Fintype.Basic 3 … module docstring, 35 lines 39 40 namespace Lax314295.MSOLogic 41 42 /-- Formulas of monadic second-order logic over strings with letters in `A`; 43 first-order and second-order variables are named by natural numbers. -/ 44 inductive MSO (A : Type) : Type 45 /-- The order test `x_i ≤ x_j`. -/ 46 | le : ℕ → ℕ → MSO A 47 /-- The label test `a (x_i)`. -/ 48 | lab : A → ℕ → MSO A 49 /-- The membership test `x_i ∈ X_j`. -/ 50 | mem : ℕ → ℕ → MSO A 51 /-- Negation. -/ 52 | not : MSO A → MSO A 53 /-- Conjunction. -/ 54 | and : MSO A → MSO A → MSO A 55 /-- Disjunction. -/ 56 | or : MSO A → MSO A → MSO A 57 /-- First-order existential quantification `∃ x_i`. -/ 58 | exFO : ℕ → MSO A → MSO A 59 /-- Second-order existential quantification `∃ X_i`. -/ 60 | exSO : ℕ → MSO A → MSO A 61 62 namespace MSO 63 64 variable {A : Type} 65 66 /-- Satisfaction of a formula in a string under a valuation of the first-order 67 variables by positions and of the second-order variables by sets of positions. -/ 68 def Sat (w : List A) : (ℕ → ℕ) → (ℕ → Set ℕ) → MSO A → Prop 69 | fo, _, le i j => fo i ≤ fo j 70 | fo, _, lab a i => w[fo i]? = some a 71 | fo, so, mem i j => fo i ∈ so j 72 | fo, so, not φ => ¬ Sat w fo so φ 73 | fo, so, and φ ψ => Sat w fo so φ ∧ Sat w fo so ψ 74 | fo, so, or φ ψ => Sat w fo so φ ∨ Sat w fo so ψ 75 | fo, so, exFO i φ => ∃ p < w.length, Sat w (Function.update fo i p) so φ 76 | fo, so, exSO i φ => ∃ S ⊆ {p | p < w.length}, Sat w fo (Function.update so i S) φ 77 78 /-- A formula is first-order if it uses neither set quantification nor membership. 79 -/ 80 def IsFO : MSO A → Prop 81 | le _ _ => True 82 | lab _ _ => True 83 | mem _ _ => False 84 | not φ => IsFO φ 85 | and φ ψ => IsFO φ ∧ IsFO ψ 86 | or φ ψ => IsFO φ ∧ IsFO ψ 87 | exFO _ φ => IsFO φ 88 | exSO _ _ => False 89 90 /-- The quantifier rank: the maximal number of nested quantifiers. -/ 91 def qrank : MSO A → ℕ 92 | le _ _ => 0 93 | lab _ _ => 0 94 | mem _ _ => 0 95 | not φ => qrank φ 96 | and φ ψ => max (qrank φ) (qrank ψ) 97 | or φ ψ => max (qrank φ) (qrank ψ) 98 | exFO _ φ => qrank φ + 1 99 | exSO _ φ => qrank φ + 1 100 101 /-- The free first-order variables of a formula. -/ 102 def freeFO : MSO A → Set ℕ 103 | le i j => {i, j} 104 | lab _ i => {i} 105 | mem i _ => {i} 106 | not φ => freeFO φ 107 | and φ ψ => freeFO φ ∪ freeFO ψ 108 | or φ ψ => freeFO φ ∪ freeFO ψ 109 | exFO i φ => freeFO φ \ {i} 110 | exSO _ φ => freeFO φ 111 112 /-- The free second-order variables of a formula. -/ 113 def freeSO : MSO A → Set ℕ 114 | le _ _ => ∅ 115 | lab _ _ => ∅ 116 | mem _ j => {j} 117 | not φ => freeSO φ 118 | and φ ψ => freeSO φ ∪ freeSO ψ 119 | or φ ψ => freeSO φ ∪ freeSO ψ 120 | exFO _ φ => freeSO φ 121 | exSO i φ => freeSO φ \ {i} 122 123 end MSO 124 125 /-- A language is definable in monadic second-order logic. -/ 126 def MSODefinable {A : Type} (L : Language A) : Prop := 127 ∃ φ : MSO A, ∀ (w : List A) (fo : ℕ → ℕ) (so : ℕ → Set ℕ), MSO.Sat w fo so φ ↔ w ∈ L 128 129 /-- A language is definable in first-order logic. -/ 130 def FODefinable {A : Type} (L : Language A) : Prop := 131 ∃ φ : MSO A, φ.IsFO ∧ 132 ∀ (w : List A) (fo : ℕ → ℕ) (so : ℕ → Set ℕ), MSO.Sat w fo so φ ↔ w ∈ L 133 134 open scoped Classical in 135 /-- The annotation `w ⊗ {x₁} ⊗ ⋯ ⊗ {x_k} ⊗ X₁ ⊗ ⋯ ⊗ X_l` of a string by the values 136 of `k` first-order and `l` second-order variables. -/ 137 noncomputable def annotate {A : Type} (k l : ℕ) (w : List A) 138 (fo : Fin k → ℕ) (so : Fin l → Set ℕ) : List (A × (Fin k → Bool) × (Fin l → Bool)) := 139 w.zipIdx.map (fun z => (z.1, fun i => decide (fo i = z.2), fun j => decide (z.2 ∈ so j))) 140 141 /-- Extend a valuation of the first-order variables `0, …, k-1` to all variables. -/ 142 def extFO (k : ℕ) (fo : Fin k → ℕ) : ℕ → ℕ := 143 fun i => if h : i < k then fo ⟨i, h⟩ else 0 144 145 /-- Extend a valuation of the set variables `0, …, l-1` to all variables. -/ 146 def extSO (l : ℕ) (so : Fin l → Set ℕ) : ℕ → Set ℕ := 147 fun j => if h : j < l then so ⟨j, h⟩ else ∅ 148 149 end Lax314295.MSOLogic 150 -
⊢
Lax314295Proofs.Results.isRegular_iff_msoDefinablepp. 118–120Büchi's theorem (Theorem C.4.1) as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax314295.MSOFreeVariablesp. 119Formulas with free variables define regular languages of annotated strings
Let be an mso formula over whose free variables are among the first-order variables and the set variables . Then the language over of the annotated strings such that is regular (Lemma C.4.2 of Transducers). The proof is an induction on the formula, with a nondeterministic automaton guessing the value of a quantified variable.
1 import Lax314295.MSOLogic 2 … module docstring, 21 lines 24 25 namespace Lax314295.MSOFreeVariables 26 27 open Lax314295.MSOLogic 28 29 /-- The annotated strings satisfying a formula form a regular language. -/ 30 axiom isRegular_annotated {A : Type} [Finite A] (φ : MSO A) (k l : ℕ) 31 (hfo : φ.freeFO ⊆ {i | i < k}) (hso : φ.freeSO ⊆ {j | j < l}) : 32 Language.IsRegular 33 {u : List (A × (Fin k → Bool) × (Fin l → Bool)) | 34 ∃ (w : List A) (fo : Fin k → ℕ) (so : Fin l → Set ℕ), 35 (∀ i, fo i < w.length) ∧ (∀ j, so j ⊆ {p | p < w.length}) ∧ 36 u = annotate k l w fo so ∧ MSO.Sat w (extFO k fo) (extSO l so) φ} 37 38 end Lax314295.MSOFreeVariables 39 -
⊢
Lax314295Proofs.Results.isRegular_annotatedpp. 119–120no assumptions
The annotated strings satisfying a formula with free variables form a regular language (Lemma C.4.2): induction on the formula, with projection for the quantifiers ().
-
def
Lax314295.MSORelabellingspp. 120–121MSO relabellings
An mso relabelling (Definition C.4.3 of Transducers) consists of an input alphabet , an output alphabet , a finite set of mso formulas over each with exactly one free first-order variable, an output map , and a string in for the empty input, such that for every input string and every position in it exactly one formula of is true at that position. The relabelling maps a nonempty input to the concatenation, over its positions, of the outputs of the unique formulas true there, and the empty input to the designated string. MSO relabellings define exactly the rational functions (Theorem C.4.4), and first-order relabellings — all of whose formulas are first-order — exactly the functions of aperiodic bimachines (Theorem C.4.16).
1 import Lax314295.MSOLogic 2 … module docstring, 24 lines 27 28 namespace Lax314295.MSORelabellings 29 30 open Lax314295.MSOLogic 31 32 /-- An mso relabelling: a finite family of formulas with one free first-order 33 variable (the variable `0`), exactly one of which holds at each position of each 34 input, an output string for each formula, and an output for the empty input. -/ 35 structure MSORelabelling (A B : Type) where 36 /-- The index set of the formulas. -/ 37 Idx : Type 38 /-- Finiteness of the index set. -/ 39 finIdx : Finite Idx 40 /-- The formulas, each with the one free first-order variable `x₀`. -/ 41 form : Idx → MSO A 42 /-- The output string of each formula. -/ 43 out : Idx → List B 44 /-- The output string for the empty input. -/ 45 emptyOut : List B 46 /-- At every position of every input string exactly one formula holds. -/ 47 unique : ∀ (w : List A) (p : ℕ), p < w.length → 48 ∃! i : Idx, MSO.Sat w (fun _ => p) (fun _ => ∅) (form i) 49 50 namespace MSORelabelling 51 52 variable {A B : Type} 53 54 /-- The relabelling maps `w` to `v`: for a nonempty input, `v` is the concatenation 55 of the outputs of the formulas true at the positions of `w`; the empty input 56 gives the designated string. -/ 57 def Relabels (R : MSORelabelling A B) (w : List A) (v : List B) : Prop := 58 (w = [] ∧ v = R.emptyOut) ∨ 59 (w ≠ [] ∧ ∃ g : ℕ → R.Idx, 60 (∀ p < w.length, MSO.Sat w (fun _ => p) (fun _ => ∅) (R.form (g p))) ∧ 61 v = ((List.range w.length).map (fun p => R.out (g p))).flatten) 62 63 /-- All formulas of the relabelling are first-order. -/ 64 def AllFO (R : MSORelabelling A B) : Prop := ∀ i, (R.form i).IsFO 65 66 end MSORelabelling 67 68 /-- A function defined by an mso relabelling. -/ 69 def IsMSORelabelling {A B : Type} (f : List A → List B) : Prop := 70 ∃ R : MSORelabelling A B, ∀ w, R.Relabels w (f w) 71 72 /-- A function defined by a first-order relabelling. -/ 73 def IsFORelabelling {A B : Type} (f : List A → List B) : Prop := 74 ∃ R : MSORelabelling A B, R.AllFO ∧ ∀ w, R.Relabels w (f w) 75 76 end Lax314295.MSORelabellings 77 -
thm✓
Lax314295.RationalIffRelabellingp. 121Rational functions are exactly the MSO relabellings
A string-to-string function is rational if and only if it is definable by an mso relabelling (Theorem C.4.4 of Transducers, Bloem and Engelfriet). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax132576.RationalFunctions 2 import Lax314295.MSORelabellings 3 … module docstring, 14 lines 18 19 namespace Lax314295.RationalIffRelabelling 20 21 open Lax132576.RationalFunctions Lax314295.MSORelabellings 22 23 /-- A function is rational if and only if it is an mso relabelling. -/ 24 axiom isRationalFun_iff_isMSORelabelling {A B : Type} [Finite A] [Finite B] 25 (f : List A → List B) : IsRationalFun f ↔ IsMSORelabelling f 26 27 end Lax314295.RationalIffRelabelling 28 -
thm✓
Lax314295.RelabellingOfRationalp. 121Rational functions are MSO relabellings
Every rational function is definable by an mso relabelling (Theorem C.4.4 of Transducers, Bloem–Engelfriet, the implication from rational to relabelling). A rational function is computed by a bimachine; for each pair of a state of the prefix automaton and a state of the suffix automaton there is an mso formula selecting the positions at which the bimachine is in that pair of states (Claim C.4.5, stated for the index of a bimachine), and the output map is the output function of the bimachine.
1 import Lax132576.RationalFunctions 2 import Lax314295.MSORelabellings 3 … module docstring, 17 lines 21 22 namespace Lax314295.RelabellingOfRational 23 24 open Lax132576.RationalFunctions Lax314295.MSORelabellings 25 26 /-- A rational function is definable by an mso relabelling. -/ 27 axiom isMSORelabelling_of_isRationalFun {A B : Type} [Finite A] [Finite B] 28 {f : List A → List B} (hf : IsRationalFun f) : IsMSORelabelling f 29 30 end Lax314295.RelabellingOfRational 31 -
thm✓
Lax314295.RationalOfRelabellingp. 121MSO relabellings are rational
Every function definable by an mso relabelling is rational (Theorem C.4.4 of Transducers, Bloem–Engelfriet, the implication from relabelling to rational). By Claim C.4.6 the strings annotated at every position with the formula true there form a regular language, so an automaton with output guesses the annotation, checks it, and outputs the output map of the guessed formulas.
1 import Lax132576.RationalFunctions 2 import Lax314295.MSORelabellings 3 … module docstring, 15 lines 19 20 namespace Lax314295.RationalOfRelabelling 21 22 open Lax132576.RationalFunctions Lax314295.MSORelabellings 23 24 /-- A function definable by an mso relabelling is rational. -/ 25 axiom isRationalFun_of_isMSORelabelling {A B : Type} [Finite A] [Finite B] 26 {f : List A → List B} (hf : IsMSORelabelling f) : IsRationalFun f 27 28 end Lax314295.RationalOfRelabelling 29 -
Theorem C.4.4 as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax314295.MSOAnnotationRegularpp. 121–122The correctly annotated strings of an MSO relabelling form a regular language
For an mso relabelling with formulas , the language over of the strings such that for every the formula is true at position of is regular (Claim C.4.6 of Transducers). For each formula, the strings with one marked position at which the formula holds form a regular language by Lemma C.4.2, and the claim's language is the intersection, over the formulas, of the complements of the projections of the strings that violate it.
1 import Lax314295.MSORelabellings 2 … module docstring, 17 lines 20 21 namespace Lax314295.MSOAnnotationRegular 22 23 open Lax314295.MSOLogic Lax314295.MSORelabellings 24 25 /-- The strings annotated at every position with a formula true there form a 26 regular language. -/ 27 axiom isRegular_annotation {A B : Type} [Finite A] (R : MSORelabelling A B) : 28 Language.IsRegular 29 {u : List (A × R.Idx) | ∀ (p : ℕ) (hp : p < u.length), 30 MSO.Sat (u.map Prod.fst) (fun _ => p) (fun _ => ∅) (R.form (u.get ⟨p, hp⟩).2)} 31 32 end Lax314295.MSOAnnotationRegular 33 -
no assumptions
For an mso relabelling, the strings annotated at every position with a formula true there form a regular language (Claim C.4.6): the intersection, over the formulas, of the complements of the languages "some position carries a formula that fails there", each regular by Lemma C.4.2 ().
-
def
Lax314295.MSOTransductionspp. 125–126String-to-string MSO transductions
A string-to-string mso transduction (Definition C.4.7 of Transducers) is given by an input alphabet , an output alphabet , a linear type — on an input of length it has copies of each input position and extra elements — and mso formulas over : a universe formula , a letter formula for each , and an order formula . It is required that for every input, every element selected by the universe formula satisfies exactly one letter formula and the order formula is a linear order on the selected elements. The output on is then the string obtained by taking the selected elements of , ordering them by the order formula and labelling them by the letter formulas. Linearity of keeps the output of linear size; string-to-string mso transductions define exactly the regular functions (Theorem C.4.8).
1 import Lax314295.MSOLogic 2 … module docstring, 36 lines 39 40 namespace Lax314295.MSOTransductions 41 42 open Lax314295.MSOLogic 43 44 /-- A string-to-string mso transduction of the linear type `copies · n + extra`, 45 presented by families of ordinary mso formulas indexed by the variants of the 46 type. -/ 47 structure MSOTransduction (A B : Type) where 48 /-- The number of copies of the input positions. -/ 49 copies : ℕ 50 /-- The number of extra (constant) elements. -/ 51 extra : ℕ 52 /-- Universe formulas for the copies of the positions; free variable `x₀`. -/ 53 univP : Fin copies → MSO A 54 /-- Universe formulas for the extra elements; sentences. -/ 55 univC : Fin extra → MSO A 56 /-- Letter formulas for the copies of the positions; free variable `x₀`. -/ 57 labP : Fin copies → B → MSO A 58 /-- Letter formulas for the extra elements; sentences. -/ 59 labC : Fin extra → B → MSO A 60 /-- Order formulas between two copies of positions; free variables `x₀, x₁`. -/ 61 ordPP : Fin copies → Fin copies → MSO A 62 /-- Order formulas between a copy of a position and an extra element. -/ 63 ordPC : Fin copies → Fin extra → MSO A 64 /-- Order formulas between an extra element and a copy of a position. -/ 65 ordCP : Fin extra → Fin copies → MSO A 66 /-- Order formulas between two extra elements. -/ 67 ordCC : Fin extra → Fin extra → MSO A 68 69 namespace MSOTransduction 70 71 variable {A B : Type} 72 73 /-- The elements of the type `copies · n + extra`, before selection. -/ 74 abbrev Elt (T : MSOTransduction A B) : Type := (Fin T.copies × ℕ) ⊕ Fin T.extra 75 76 /-- The elements selected by the universe formulas. -/ 77 def selected (T : MSOTransduction A B) (w : List A) : T.Elt → Prop 78 | Sum.inl (i, p) => p < w.length ∧ MSO.Sat w (fun _ => p) (fun _ => ∅) (T.univP i) 79 | Sum.inr j => MSO.Sat w (fun _ => 0) (fun _ => ∅) (T.univC j) 80 81 /-- The order defined by the order formulas. -/ 82 def ordRel (T : MSOTransduction A B) (w : List A) : T.Elt → T.Elt → Prop 83 | Sum.inl (i, p), Sum.inl (i', p') => 84 MSO.Sat w (fun v => if v = 0 then p else p') (fun _ => ∅) (T.ordPP i i') 85 | Sum.inl (i, p), Sum.inr j => MSO.Sat w (fun _ => p) (fun _ => ∅) (T.ordPC i j) 86 | Sum.inr j, Sum.inl (i, p) => MSO.Sat w (fun _ => p) (fun _ => ∅) (T.ordCP j i) 87 | Sum.inr j, Sum.inr j' => MSO.Sat w (fun _ => 0) (fun _ => ∅) (T.ordCC j j') 88 89 /-- The labelling defined by the letter formulas. -/ 90 def labRel (T : MSOTransduction A B) (w : List A) : T.Elt → B → Prop 91 | Sum.inl (i, p), b => MSO.Sat w (fun _ => p) (fun _ => ∅) (T.labP i b) 92 | Sum.inr j, b => MSO.Sat w (fun _ => 0) (fun _ => ∅) (T.labC j b) 93 94 /-- The transduction outputs `v` on `w`: `v` lists the selected elements, without 95 repetition, in the order of the order formula, each labelled by a letter of 96 its letter formulas. -/ 97 def Outputs (T : MSOTransduction A B) (w : List A) (v : List B) : Prop := 98 ∃ es : List T.Elt, 99 es.Nodup ∧ 100 (∀ x, x ∈ es ↔ T.selected w x) ∧ 101 (∀ (i j : ℕ) (hi : i < es.length) (hj : j < es.length), 102 i < j → T.ordRel w (es.get ⟨i, hi⟩) (es.get ⟨j, hj⟩)) ∧ 103 es.length = v.length ∧ 104 ∀ (i : ℕ) (hi : i < es.length) (hi' : i < v.length), 105 T.labRel w (es.get ⟨i, hi⟩) (v.get ⟨i, hi'⟩) 106 107 /-- The requirement of Definition C.4.7: on every input, every selected element 108 satisfies exactly one letter formula, and the order formula is a linear order 109 on the selected elements. -/ 110 def Proper (T : MSOTransduction A B) : Prop := 111 ∀ w : List A, 112 (∀ x, T.selected w x → ∃! b, T.labRel w x b) ∧ 113 (∀ x, T.selected w x → T.ordRel w x x) ∧ 114 (∀ x y, T.selected w x → T.selected w y → 115 T.ordRel w x y → T.ordRel w y x → x = y) ∧ 116 (∀ x y z, T.selected w x → T.selected w y → T.selected w z → 117 T.ordRel w x y → T.ordRel w y z → T.ordRel w x z) ∧ 118 (∀ x y, T.selected w x → T.selected w y → T.ordRel w x y ∨ T.ordRel w y x) 119 120 /-- All formulas of the transduction are first-order. -/ 121 def AllFO (T : MSOTransduction A B) : Prop := 122 (∀ i, (T.univP i).IsFO) ∧ (∀ j, (T.univC j).IsFO) ∧ 123 (∀ i b, (T.labP i b).IsFO) ∧ (∀ j b, (T.labC j b).IsFO) ∧ 124 (∀ i i', (T.ordPP i i').IsFO) ∧ (∀ i j, (T.ordPC i j).IsFO) ∧ 125 (∀ j i, (T.ordCP j i).IsFO) ∧ (∀ j j', (T.ordCC j j').IsFO) 126 127 end MSOTransduction 128 129 /-- A function defined by a string-to-string mso transduction satisfying the 130 requirements of the definition. -/ 131 def IsMSOTransduction {A B : Type} (f : List A → List B) : Prop := 132 ∃ T : MSOTransduction A B, T.Proper ∧ ∀ w, T.Outputs w (f w) 133 134 /-- A function defined by a first-order transduction. -/ 135 def IsFOTransduction {A B : Type} (f : List A → List B) : Prop := 136 ∃ T : MSOTransduction A B, T.Proper ∧ T.AllFO ∧ ∀ w, T.Outputs w (f w) 137 138 end Lax314295.MSOTransductions 139 -
thm✓
Lax314295.MSOTransductionIffRegularp. 127MSO transductions define exactly the regular functions
String-to-string mso transductions define exactly the regular functions (Theorem C.4.8 of Transducers, Engelfriet and Hoogeboom). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax916827.RegularFunctions 2 import Lax314295.MSOTransductions 3 … module docstring, 14 lines 18 19 namespace Lax314295.MSOTransductionIffRegular 20 21 open Lax916827.RegularFunctions Lax314295.MSOTransductions 22 23 /-- A function is defined by an mso transduction if and only if it is regular. -/ 24 axiom isMSOTransduction_iff_isRegularFun {A B : Type} [Finite A] [Finite B] 25 (f : List A → List B) : IsMSOTransduction f ↔ IsRegularFun f 26 27 end Lax314295.MSOTransductionIffRegular 28 -
thm✓
Lax314295.RegularOfMSOTransductionp. 127MSO transductions define regular functions
Every function defined by a string-to-string mso transduction is regular (Theorem C.4.8 of Transducers, Engelfriet–Hoogeboom, the implication from transduction to regular). The transduction is normalised to one universe and one letter formula per copy and one order formula per pair of copies (Lemma C.4.9); the questions the formulas ask are precomputed by a letter-to-letter rational function (Lemma C.4.10); and a two-way transducer walks through the output order, moving to the successor of the current element by running the automaton of the precomputed language on the infix between them.
1 import Lax916827.RegularFunctions 2 import Lax314295.MSOTransductions 3 … module docstring, 18 lines 22 23 namespace Lax314295.RegularOfMSOTransduction 24 25 open Lax916827.RegularFunctions Lax314295.MSOTransductions 26 27 /-- A function defined by an mso transduction is regular. -/ 28 axiom isRegularFun_of_isMSOTransduction {A B : Type} [Finite A] [Finite B] 29 {f : List A → List B} (hf : IsMSOTransduction f) : IsRegularFun f 30 31 end Lax314295.RegularOfMSOTransduction 32 -
thm✓
Lax314295.MSOTransductionOfRegularp. 127Regular functions are MSO transductions
Every regular function is defined by a string-to-string mso transduction (Theorem C.4.8 of Transducers, Engelfriet–Hoogeboom, the implication from regular to transduction). A regular function is computed by a two-way transducer (Theorem C.2.9); the transduction's elements are the pairs of a configuration of its run and an index into the output produced there, and all its formulas — which configurations are reached, which letter is produced, which of two configurations comes first — are regular properties of the input with marked positions, hence mso-definable by Büchi's theorem.
1 import Lax916827.RegularFunctions 2 import Lax314295.MSOTransductions 3 … module docstring, 18 lines 22 23 namespace Lax314295.MSOTransductionOfRegular 24 25 open Lax916827.RegularFunctions Lax314295.MSOTransductions 26 27 /-- A regular function is defined by an mso transduction. -/ 28 axiom isMSOTransduction_of_isRegularFun {A B : Type} [Finite A] [Finite B] 29 {f : List A → List B} (hf : IsRegularFun f) : IsMSOTransduction f 30 31 end Lax314295.MSOTransductionOfRegular 32 -
Theorem C.4.8 as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax314295.LogicPrecomputationp. 128Precomputing the answers of MSO formulas by a rational function
For a finite set of mso formulas with one or two free first-order variables there is a letter-to-letter rational function such that each formula with one free variable corresponds to a set of letters — exactly when the letter of at position is in — and each formula with two free variables corresponds to a regular language — for , exactly when the infix of from to belongs to (Lemma C.4.10 of Transducers). The function decorates every position with the states, on the prefix and on the suffix, of the automata of Lemma C.4.2 for the formulas.
1 import Lax765601.ElementaryProperties 2 import Lax132576.RationalFunctions 3 import Lax314295.MSOLogic 4 … module docstring, 22 lines 27 28 namespace Lax314295.LogicPrecomputation 29 30 open Lax765601.ElementaryProperties Lax132576.RationalFunctions Lax314295.MSOLogic 31 32 /-- The answers of finitely many mso formulas with one or two free variables are 33 read off a letter-to-letter rational function: as letters, respectively as regular 34 languages of infixes. -/ 35 axiom exists_rational_precomputation {A : Type} [Finite A] 36 (Φ₁ Φ₂ : Set (MSO A)) (hΦ₁ : Φ₁.Finite) (hΦ₂ : Φ₂.Finite) : 37 ∃ (C : Type) (_ : Finite C) (f : List A → List C), 38 IsRationalFun f ∧ LengthPreserving f ∧ 39 (∀ φ ∈ Φ₁, ∃ F : Set C, ∀ (w : List A) (x : ℕ), x < w.length → 40 (MSO.Sat w (fun _ => x) (fun _ => ∅) φ ↔ ∃ c ∈ F, (f w)[x]? = some c)) ∧ 41 (∀ φ ∈ Φ₂, ∃ L : Language C, L.IsRegular ∧ ∀ (w : List A) (x y : ℕ), 42 x ≤ y → y < w.length → 43 (MSO.Sat w (fun i => if i = 0 then x else y) (fun _ => ∅) φ ↔ 44 ((f w).drop x).take (y - x + 1) ∈ L)) 45 46 end Lax314295.LogicPrecomputation 47 -
no assumptions
The answers of finitely many mso formulas with one or two free variables are read off a letter-to-letter rational function (Lemma C.4.10): a product of the automata of Lemma C.4.2 run from both ends, as a bimachine ().
-
thm✓
Lax314295.FOIffAperiodicp. 130First-order definable languages are exactly the aperiodic ones
A language is definable in first-order logic if and only if it is recognised by an aperiodic deterministic automaton (Theorem C.4.11 of Transducers, Schützenberger, McNaughton and Papert). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax765601.StateTransformations 2 import Lax314295.MSOLogic 3 … module docstring, 15 lines 19 20 namespace Lax314295.FOIffAperiodic 21 22 open Lax765601.StateTransformations Lax314295.MSOLogic 23 24 /-- A language is first-order definable if and only if some aperiodic dfa 25 recognises it. -/ 26 axiom foDefinable_iff_aperiodic_dfa {A : Type} [Finite A] (L : Language A) : 27 FODefinable L ↔ 28 ∃ (σ : Type) (_ : Finite σ) (M : DFA A σ), TransAperiodic M.step ∧ M.accepts = L 29 30 end Lax314295.FOIffAperiodic 31 -
thm✓
Lax314295.AperiodicOfFOp. 130First-order definable languages are aperiodic
Every language definable in first-order logic is recognised by an aperiodic deterministic automaton (Theorem C.4.11 of Transducers, the implication from definable to aperiodic). A first-order sentence of quantifier rank depends only on the -type of the string (Lemma C.4.13); the automaton whose states are the -types, which is finite and aperiodic by Lemma C.4.15, recognises the language.
1 import Lax765601.StateTransformations 2 import Lax314295.MSOLogic 3 … module docstring, 18 lines 22 23 namespace Lax314295.AperiodicOfFO 24 25 open Lax765601.StateTransformations Lax314295.MSOLogic 26 27 /-- A first-order definable language is recognised by an aperiodic dfa. -/ 28 axiom exists_aperiodic_dfa_of_foDefinable {A : Type} [Finite A] {L : Language A} 29 (hL : FODefinable L) : 30 ∃ (σ : Type) (_ : Finite σ) (M : DFA A σ), TransAperiodic M.step ∧ M.accepts = L 31 32 end Lax314295.AperiodicOfFO 33 -
thm✓
Lax314295.FOOfAperiodicp. 130Aperiodic automata recognise first-order definable languages
Every language recognised by an aperiodic deterministic automaton is definable in first-order logic (Theorem C.4.11 of Transducers, the implication from aperiodic to definable). The automaton, read as a Mealy machine, is a composition of flip-flops by Theorem A.2.8, and the state of a flip-flop at a position is determined by the last resetting letter before it, which first-order logic can express; composing the formulas along the decomposition gives a first-order description of the run.
1 import Lax765601.StateTransformations 2 import Lax314295.MSOLogic 3 … module docstring, 18 lines 22 23 namespace Lax314295.FOOfAperiodic 24 25 open Lax765601.StateTransformations Lax314295.MSOLogic 26 27 /-- The language of an aperiodic dfa is first-order definable. -/ 28 axiom foDefinable_of_aperiodic_dfa {A σ : Type} [Finite A] [Finite σ] (M : DFA A σ) 29 (hM : TransAperiodic M.step) : FODefinable M.accepts 30 31 end Lax314295.FOOfAperiodic 32 -
Theorem C.4.11 as a biconditional, glued from its two halves taken as assumptions.
-
def
Lax314295.KTypesp. 131The k-type of a string
The -type of a string (Definition C.4.12 of Transducers) is defined by induction on : the -type of every string is the same, and the -type of is the set of triples
over all factorisations of around one of its letters. Two strings have the same -type if and only if they satisfy the same first-order sentences of quantifier rank at most (Lemma C.4.13); -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).
1 import Mathlib.Data.Set.Basic 2 … module docstring, 21 lines 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 -
thm✓
Lax314295.KTypesFOEquivalencep. 132k-types capture first-order sentences of quantifier rank k
Two strings have the same -type if and only if they satisfy the same first-order sentences of quantifier rank at most (Lemma C.4.13 of Transducers). From equal types to equal satisfaction is the compositionality of first-order logic: a position chosen on one string can be matched on the other so that all formulas of one rank lower are preserved. Conversely the set of strings of a given -type is defined by a first-order sentence of quantifier rank , built by induction on with quantification relativised to the two sides of a chosen position.
1 import Lax314295.MSOLogic 2 import Lax314295.KTypes 3 … module docstring, 22 lines 26 27 namespace Lax314295.KTypesFOEquivalence 28 29 open Lax314295.MSOLogic Lax314295.KTypes 30 31 /-- Two strings have the same `k`-type if and only if they satisfy the same 32 first-order sentences of quantifier rank at most `k`. -/ 33 axiom tp_eq_iff_fo_equiv {A : Type} [Finite A] (k : ℕ) (w v : List A) : 34 tp k w = tp k v ↔ 35 ∀ φ : MSO A, φ.IsFO → φ.freeFO = ∅ → φ.qrank ≤ k → 36 ((∀ fo so, MSO.Sat w fo so φ) ↔ (∀ fo so, MSO.Sat v fo so φ)) 37 38 end Lax314295.KTypesFOEquivalence 39 -
⊢
Lax314295Proofs.Results.tp_eq_iff_fo_equivpp. 132–133no assumptions
Two strings have the same -type if and only if they satisfy the same first-order sentences of quantifier rank at most (Lemma C.4.13): compositionality of first-order logic for the direction from types to sentences, and Hintikka sentences describing the -type for the converse ().
-
thm✓
Lax314295.KTypesRefinementp. 133k-types refine each other
Strings with the same -type have the same -type (Lemma C.4.15 of Transducers, refinement): the -type of a string is determined by its -type.
1 import Lax314295.KTypes 2 … module docstring, 13 lines 16 17 namespace Lax314295.KTypesRefinement 18 19 open Lax314295.KTypes 20 21 /-- Equal `(k+1)`-types have equal `k`-types. -/ 22 axiom tp_eq_of_tp_succ_eq {A : Type} (k : ℕ) (w v : List A) (h : tp (k + 1) w = tp (k + 1) v) : 23 tp k w = tp k v 24 25 end Lax314295.KTypesRefinement 26 -
thm✓
Lax314295.KTypesCongruencep. 133k-types are a congruence for concatenation
The -type of a concatenation depends only on the -types of and of (Lemma C.4.15 of Transducers, congruence): the relation "same -type" is a congruence of the free monoid.
1 import Lax314295.KTypes 2 … module docstring, 13 lines 16 17 namespace Lax314295.KTypesCongruence 18 19 open Lax314295.KTypes 20 21 /-- The `k`-type of a concatenation is determined by the `k`-types of the parts. -/ 22 axiom tp_append_congr {A : Type} (k : ℕ) (w w' v v' : List A) 23 (hw : tp k w = tp k w') (hv : tp k v = tp k v') : tp k (w ++ v) = tp k (w' ++ v') 24 25 end Lax314295.KTypesCongruence 26 -
thm✓
Lax314295.KTypesAperiodicityp. 133k-types are aperiodic
For every string and every , the -types of the powers eventually stabilise (Lemma C.4.15 of Transducers, aperiodicity): all sufficiently large powers of a string have the same -type. This is what makes the automaton of -types aperiodic.
1 import Lax765601.Aperiodicity 2 import Lax314295.KTypes 3 … module docstring, 14 lines 18 19 namespace Lax314295.KTypesAperiodicity 20 21 open Lax765601.Aperiodicity Lax314295.KTypes 22 23 /-- The `k`-types of the powers of a string eventually stabilise. -/ 24 axiom exists_tp_npow_eq {A : Type} (k : ℕ) (w : List A) : 25 ∃ N : ℕ, ∀ n ≥ N, tp k (npow w n) = tp k (npow w N) 26 27 end Lax314295.KTypesAperiodicity 28 -
⊢
Lax314295Proofs.Results.tp_eq_of_tp_succ_eqpp. 133–134no assumptions
Equal -types have equal -types (Lemma C.4.15, refinement): induction on (, first conjunct).
-
thm✓
Lax314295.FORelabellingIffAperiodicBimachinep. 134First-order relabellings are exactly the aperiodic bimachines
A string-to-string function is a first-order relabelling if and only if it is computed by an aperiodic bimachine (Theorem C.4.16 of Transducers). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax132576.Bimachines 2 import Lax314295.MSORelabellings 3 … module docstring, 15 lines 19 20 namespace Lax314295.FORelabellingIffAperiodicBimachine 21 22 open Lax132576.Bimachines Lax314295.MSORelabellings 23 24 /-- A function is a first-order relabelling if and only if an aperiodic bimachine 25 computes it. -/ 26 axiom isFORelabelling_iff_isAperiodicBimachine {A B : Type} [Finite A] [Finite B] 27 (f : List A → List B) : IsFORelabelling f ↔ IsAperiodicBimachine f 28 29 end Lax314295.FORelabellingIffAperiodicBimachine 30 -
thm✓
Lax314295.AperiodicBimachineOfFORelabellingp. 134First-order relabellings are computed by aperiodic bimachines
Every first-order relabelling is computed by an aperiodic bimachine (Theorem C.4.16 of Transducers, the implication from relabelling to bimachine). For a first-order formula with one free variable, the prefixes and the suffixes on which it holds at the marked position are first-order definable languages, recognised by aperiodic automata (Theorem C.4.11), which become the prefix and suffix automata of the bimachine.
1 import Lax132576.Bimachines 2 import Lax314295.MSORelabellings 3 … module docstring, 16 lines 20 21 namespace Lax314295.AperiodicBimachineOfFORelabelling 22 23 open Lax132576.Bimachines Lax314295.MSORelabellings 24 25 /-- A first-order relabelling is computed by an aperiodic bimachine. -/ 26 axiom isAperiodicBimachine_of_isFORelabelling {A B : Type} [Finite A] [Finite B] 27 {f : List A → List B} (hf : IsFORelabelling f) : IsAperiodicBimachine f 28 29 end Lax314295.AperiodicBimachineOfFORelabelling 30 -
thm✓
Lax314295.FORelabellingOfAperiodicBimachinep. 134Aperiodic bimachines compute first-order relabellings
Every function computed by an aperiodic bimachine is a first-order relabelling (Theorem C.4.16 of Transducers, the implication from bimachine to relabelling). By Theorem C.4.11 the runs of the two aperiodic automata are described in first-order logic: for each pair of a transition of the prefix automaton and one of the suffix automaton there is a first-order formula selecting the positions at which they are used, and the output map is the output function of the bimachine.
1 import Lax132576.Bimachines 2 import Lax314295.MSORelabellings 3 … module docstring, 17 lines 21 22 namespace Lax314295.FORelabellingOfAperiodicBimachine 23 24 open Lax132576.Bimachines Lax314295.MSORelabellings 25 26 /-- A function computed by an aperiodic bimachine is a first-order relabelling. -/ 27 axiom isFORelabelling_of_isAperiodicBimachine {A B : Type} [Finite A] [Finite B] 28 {f : List A → List B} (hf : IsAperiodicBimachine f) : IsFORelabelling f 29 30 end Lax314295.FORelabellingOfAperiodicBimachine 31 -
Theorem C.4.16 as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax916827.RegularContinuityp. 86Regular functions are continuous
Regular functions are continuous (Theorem C.1.1 of Transducers, the continuity half). Continuous functions are closed under composition and rational functions are continuous (Theorem B.1.5), so it remains to see that map reverse and map duplicate are continuous, which is Lemma C.1.2 (reversal and duplication are continuous) lifted through Lemma C.1.3 (the map lifting of a continuous function is continuous).
1 import Lax765601.Continuity 2 import Lax916827.RegularFunctions 3 … module docstring, 17 lines 21 22 namespace Lax916827.RegularContinuity 23 24 open Lax765601.Continuity Lax916827.RegularFunctions 25 26 /-- A regular function is continuous. -/ 27 axiom continuous_of_isRegularFun {A B : Type} [Finite A] [Finite B] {f : List A → List B} 28 (hf : IsRegularFun f) : Continuous f 29 30 end Lax916827.RegularContinuity 31 -
thm✓
Lax916827.RegularCompositionp. 86Regular functions are closed under composition
Regular functions are closed under composition (Theorem C.1.1 of Transducers, the composition half): composition is built into the definition of the regular functions as compositions of primes.
1 import Lax916827.RegularFunctions 2 … module docstring, 13 lines 16 17 namespace Lax916827.RegularComposition 18 19 open Lax916827.RegularFunctions 20 21 /-- The composition of two regular functions is regular. -/ 22 axiom isRegularFun_comp {A B C : Type} [Finite B] {f : List A → List B} {g : List B → List C} 23 (hf : IsRegularFun f) (hg : IsRegularFun g) : IsRegularFun (g ∘ f) 24 25 end Lax916827.RegularComposition 26 -
no assumptions
Regular functions are continuous (Theorem C.1.1, the continuity half): induction on the composition tree, with Theorem B.1.5 for the rational primes and Lemmas C.1.2–C.1.3 for map reverse and map duplicate ().
-
thm✓
Lax916827.ReversalContinuousp. 86String reversal is continuous
String reversal is continuous (Lemma C.1.2 of Transducers, first half): the inverse image of a regular language under reversal is recognised by the automaton with all transitions reversed and initial and accepting states swapped.
1 import Lax765601.Continuity 2 … module docstring, 14 lines 17 18 namespace Lax916827.ReversalContinuous 19 20 open Lax765601.Continuity 21 22 /-- String reversal is continuous. -/ 23 axiom continuous_reverse {A : Type} [Finite A] : Continuous (List.reverse : List A → List A) 24 25 end Lax916827.ReversalContinuous 26 -
thm✓
Lax916827.DuplicationContinuousp. 86String duplication is continuous
String duplication is continuous (Lemma C.1.2 of Transducers, second half): the inverse image of a regular language is the union, over the states of an automaton for , of the strings that lead from an initial state to and from to an accepting state.
1 import Lax765601.Continuity 2 … module docstring, 14 lines 17 18 namespace Lax916827.DuplicationContinuous 19 20 open Lax765601.Continuity 21 22 /-- String duplication is continuous. -/ 23 axiom continuous_duplicate {A : Type} [Finite A] : Continuous (fun w : List A => w ++ w) 24 25 end Lax916827.DuplicationContinuous 26 -
no assumptions
String reversal is continuous (Lemma C.1.2, first half): the reversed automaton (, first conjunct).
-
thm✓
Lax916827.MapLiftingContinuityp. 86The map lifting of a continuous function is continuous
If a string-to-string function is continuous, then so is its map lifting (Lemma C.1.3 of Transducers). An automaton for the inverse image of a regular language under the map lifting guesses, for every block, the states of the automaton for the language at its two ends, and checks the transitions across the blocks by continuity of the lifted function and across the separators directly.
1 import Lax765601.Continuity 2 import Lax765601.MapLifting 3 … module docstring, 16 lines 20 21 namespace Lax916827.MapLiftingContinuity 22 23 open Lax765601.Continuity Lax765601.MapLifting 24 25 /-- The map lifting of a continuous function is continuous. -/ 26 axiom continuous_mapLift {A B : Type} [Finite A] [Finite B] {f : List A → List B} 27 (hf : Continuous f) : Continuous (mapLift f) 28 29 end Lax916827.MapLiftingContinuity 30 -
⊢
Lax916827Proofs.Results.continuous_mapLiftpp. 86–87no assumptions
The map lifting of a continuous function is continuous (Lemma C.1.3): the block automaton guessing the states at the ends of every block (), through Part A's .
-
thm✓
Lax916827.RegularEquivalenceDecidablep. 87Decidable equivalence of regular functions
Equivalence is decidable for regular functions (Theorem C.1.4 of Transducers), the functions being given by two-way transducers, which compute exactly the regular functions (Theorem C.2.9). The book reduces to equivalence of weighted automata over the rationals, as for rational functions: the class of functions that can be post-composed with weighted automata is closed under composition, contains the rational functions (Theorem B.3.6), and contains map reverse and map duplicate by two constructions with triples of states.
1 import Lax132576.TransducerCodes 2 import Lax916827.TwoWayCodes 3 … module docstring, 24 lines 28 29 namespace Lax916827.RegularEquivalenceDecidable 30 31 open Lax132576.TransducerCodes Lax916827.TwoWayCodes 32 33 /-- Equivalence of two total coded two-way transducers is decidable. -/ 34 axiom decidable_twoWayCodeRel_eq : 35 DecidableUnderPromise 36 (fun p : TwoWayCode × TwoWayCode => TwoWayCodeTotal p.1 ∧ TwoWayCodeTotal p.2) 37 (fun p => twoWayCodeRel p.1 = twoWayCodeRel p.2) 38 39 end Lax916827.RegularEquivalenceDecidable 40 -
def
Lax916827.TwoWayCodesp. 87Codes of two-way transducers
The equivalence problem for regular functions (Theorem C.1.4 of Transducers) is decided on two-way transducers, which by Theorem C.2.9 compute exactly the regular functions. A two-way transducer with states and letters in is described by a finite code: a lookup table for its transition function, listing for finitely many triples (letter to the left, state, letter to the right) the transition taken there. The initial state is , and a triple absent from the table halts with empty output. A code is total if the transducer it describes halts on every input.
1 import Mathlib.Computability.Primrec.List 2 import Lax916827.TwoWayTransducers 3 … module docstring, 22 lines 26 27 namespace Lax916827.TwoWayCodes 28 29 open Lax916827.TwoWayTransducers 30 31 /-- A code of a two-way transducer over `ℕ`: a lookup table from triples (letter to 32 the left, state, letter to the right) to transitions. -/ 33 abbrev TwoWayCode := List ((Option ℕ × ℕ × Option ℕ) × (List ℕ ⊕ (ℕ × List ℕ × Bool))) 34 35 /-- The two-way transducer described by a code: initial state `0`, and the table 36 entry of a triple, or halting with empty output when the triple is absent. -/ 37 def twoWayCodeAut (c : TwoWayCode) : TwoWay ℕ ℕ ℕ where 38 init := 0 39 step := fun l q r => 40 match c.lookup (l, q, r) with 41 | some x => x 42 | none => Sum.inl [] 43 44 /-- The relation computed by the coded transducer. -/ 45 def twoWayCodeRel (c : TwoWayCode) : List ℕ → List ℕ → Prop := (twoWayCodeAut c).Computes 46 47 /-- The coded transducer computes a total function: it halts on every input. -/ 48 def TwoWayCodeTotal (c : TwoWayCode) : Prop := ∀ w, ∃ v, twoWayCodeRel c w v 49 50 end Lax916827.TwoWayCodes 51 -
no assumptions
Equivalence of total coded two-way transducers is decidable (Theorem C.1.4), of the source.
-
def
Lax916827.StreamingStringTransducerspp. 109–110Streaming string transducers
A streaming string transducer (Definition C.3.1 of Transducers) processes its input in a single left-to-right pass, storing intermediate results in finitely many registers that hold strings over the output alphabet. It has a finite set of states with an initial state, a finite set of registers, all initially empty, and a transition function that on a state and an input letter gives a new state and a register update: for every register, a string over the output alphabet and the register names, which is evaluated by substituting the current contents of the registers. Updates are copyless: each register name occurs at most once across all the strings of an update, so that no register content is ever duplicated. After the whole input has been read, a final output string over the output alphabet and the register names, chosen by the final state, is evaluated in the same way. Streaming string transducers compute exactly the regular functions (Theorem C.3.2).
1 import Mathlib.Data.Fintype.Basic 2 import Mathlib.Data.List.Basic 3 … module docstring, 28 lines 32 33 namespace Lax916827.StreamingStringTransducers 34 35 /-- A register update is copyless if each register name occurs at most once in the 36 concatenation of the strings assigned to the registers. -/ 37 def Copyless {X B : Type} [Fintype X] (u : X → List (X ⊕ B)) : Prop := 38 ((Finset.univ.toList.map u).flatten.filterMap 39 (fun z => match z with | Sum.inl x => some x | Sum.inr _ => none)).Nodup 40 41 /-- A streaming string transducer with states `Q` and registers `X`. -/ 42 structure SST (A B Q X : Type) [Fintype X] where 43 /-- The initial state. -/ 44 init : Q 45 /-- The transition function: a new state and a register update. -/ 46 step : Q → A → Q × (X → List (X ⊕ B)) 47 /-- Every register update is copyless. -/ 48 step_copyless : ∀ q a, Copyless (step q a).2 49 /-- The final output string, chosen by the final state. -/ 50 final : Q → List (X ⊕ B) 51 52 namespace SST 53 54 variable {A B Q X : Type} [Fintype X] 55 56 /-- Substituting the contents of the registers into a string over `X + B`. -/ 57 def subst (η : X → List B) (s : List (X ⊕ B)) : List B := 58 (s.map (fun z => match z with | Sum.inl x => η x | Sum.inr b => [b])).flatten 59 60 /-- Reading one input letter: the new state and the new register contents. -/ 61 def stepConfig (T : SST A B Q X) (c : Q × (X → List B)) (a : A) : Q × (X → List B) := 62 ((T.step c.1 a).1, fun x => subst c.2 ((T.step c.1 a).2 x)) 63 64 /-- The state and register contents after reading an input string, starting from 65 the initial state with empty registers. -/ 66 def runConfig (T : SST A B Q X) (w : List A) : Q × (X → List B) := 67 w.foldl T.stepConfig (T.init, fun _ => []) 68 69 /-- The semantics: the final output string of the last state, with the final 70 register contents substituted. -/ 71 def eval (T : SST A B Q X) (w : List A) : List B := 72 subst (T.runConfig w).2 (T.final (T.runConfig w).1) 73 74 end SST 75 76 /-- A function computed by a streaming string transducer with finite state space 77 and finitely many registers. -/ 78 def IsSST {A B : Type} (f : List A → List B) : Prop := 79 ∃ (Q X : Type) (_ : Finite Q) (instX : Fintype X) (T : @SST A B Q X instX), T.eval = f 80 81 end Lax916827.StreamingStringTransducers 82 -
thm✓
Lax916827.SSTIffRegularp. 110Streaming string transducers compute exactly the regular functions
A string-to-string function is computed by a streaming string transducer if and only if it is regular (Theorem C.3.2 of Transducers). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax916827.RegularFunctions 2 import Lax916827.StreamingStringTransducers 3 … module docstring, 14 lines 18 19 namespace Lax916827.SSTIffRegular 20 21 open Lax916827.RegularFunctions Lax916827.StreamingStringTransducers 22 23 /-- A function is computed by a streaming string transducer if and only if it is 24 regular. -/ 25 axiom isSST_iff_isRegularFun {A B : Type} [Finite A] [Finite B] (f : List A → List B) : 26 IsSST f ↔ IsRegularFun f 27 28 end Lax916827.SSTIffRegular 29 -
thm✓
Lax916827.SSTOfRegularp. 110Every regular function is computed by a streaming string transducer
Every regular function is computed by a streaming string transducer (Theorem C.3.2 of Transducers, the implication from regular to sst). Streaming string transducers are closed under post-composition with every prime regular function — a rational function through the Krohn–Rhodes decomposition of its Mealy machines, map reverse and map duplicate by keeping the register contents as tuples indexed by the separators inside them — and the identity is an sst.
1 import Lax916827.RegularFunctions 2 import Lax916827.StreamingStringTransducers 3 … module docstring, 16 lines 20 21 namespace Lax916827.SSTOfRegular 22 23 open Lax916827.RegularFunctions Lax916827.StreamingStringTransducers 24 25 /-- A regular function is computed by a streaming string transducer. -/ 26 axiom isSST_of_isRegularFun {A B : Type} [Finite A] [Finite B] {f : List A → List B} 27 (hf : IsRegularFun f) : IsSST f 28 29 end Lax916827.SSTOfRegular 30 -
thm✓
Lax916827.RegularOfSSTp. 110Every streaming string transducer computes a regular function
Every function computed by a streaming string transducer is regular (Theorem C.3.2 of Transducers, the implication from sst to regular). The sst is first normalised — the register update depends only on the letter read, and no register occurs twice in a final output string — by annotating the input with the states through a rational function; a two-way transducer then expands the final output string depth-first, moving left to expand a register and right when an expansion is finished, the copyless restriction making the place to resume an expansion a function of the register and the letter returned to. Two-way transducers compute regular functions (Theorem C.2.9).
1 import Lax916827.RegularFunctions 2 import Lax916827.StreamingStringTransducers 3 … module docstring, 19 lines 23 24 namespace Lax916827.RegularOfSST 25 26 open Lax916827.RegularFunctions Lax916827.StreamingStringTransducers 27 28 /-- A function computed by a streaming string transducer is regular. -/ 29 axiom isRegularFun_of_isSST {A B : Type} [Finite A] [Finite B] {f : List A → List B} 30 (hf : IsSST f) : IsRegularFun f 31 32 end Lax916827.RegularOfSST 33 -
⊢
Lax916827Proofs.Results.isSST_iff_isRegularFunpp. 110–114Theorem C.3.2 as a biconditional, glued from its two halves taken as assumptions.
-
thm✓
Lax194892.ForIffPolyregularp. 157For-transducers compute exactly the polyregular functions
A string-to-string function is polyregular if and only if it is computed by a for-transducer (Theorem D.1.1 of Transducers). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax194892.PolyregularFunctions 2 import Lax194892.ForTransducers 3 … module docstring, 14 lines 18 19 namespace Lax194892.ForIffPolyregular 20 21 open Lax194892.PolyregularFunctions Lax194892.ForTransducers 22 23 /-- A function is polyregular if and only if a for-transducer computes it. -/ 24 axiom isPolyregular_iff_isForTransducer {A B : Type} [Finite A] [Finite B] 25 (f : List A → List B) : IsPolyregular f ↔ IsForTransducer f 26 27 end Lax194892.ForIffPolyregular 28 -
thm✓
Lax194892.ForOfPolyregularp. 157Polyregular functions are computed by for-transducers
Every polyregular function is computed by a for-transducer (Theorem D.1.1 of Transducers, the implication from polyregular to for-transducer): marked squaring is two nested loops, a regular function is computed by a two-way transducer whose run a for-transducer replays, and for-transducers are closed under composition (Lemma D.1.4).
1 import Lax194892.PolyregularFunctions 2 import Lax194892.ForTransducers 3 … module docstring, 15 lines 19 20 namespace Lax194892.ForOfPolyregular 21 22 open Lax194892.PolyregularFunctions Lax194892.ForTransducers 23 24 /-- A polyregular function is computed by a for-transducer. -/ 25 axiom isForTransducer_of_isPolyregular {A B : Type} [Finite A] [Finite B] 26 {f : List A → List B} (hf : IsPolyregular f) : IsForTransducer f 27 28 end Lax194892.ForOfPolyregular 29 -
thm✓
Lax194892.PolyregularOfForp. 157For-transducers compute polyregular functions
Every function computed by a for-transducer is polyregular (Theorem D.1.1 of Transducers, the implication from for-transducer to polyregular). The program is put in prenex form (Lemma D.1.3); the tuples of loop variables are enumerated, in the order of the loops, by iterated marked squaring, and the loop-free body is evaluated on each tuple by a rational function.
1 import Lax194892.PolyregularFunctions 2 import Lax194892.ForTransducers 3 … module docstring, 15 lines 19 20 namespace Lax194892.PolyregularOfFor 21 22 open Lax194892.PolyregularFunctions Lax194892.ForTransducers 23 24 /-- A function computed by a for-transducer is polyregular. -/ 25 axiom isPolyregular_of_isForTransducer {A B : Type} [Finite A] [Finite B] 26 {f : List A → List B} (hf : IsForTransducer f) : IsPolyregular f 27 28 end Lax194892.PolyregularOfFor 29 -
def
Lax194892.ForTransducersp. 157For-transducers
A for-transducer (Section D.1 of Transducers) is an imperative program with loops ranging over the positions of the input string, in increasing or decreasing order. It has position variables, bound by the loops and read only, and Boolean variables, initially false and assignable; its tests compare positions (, ), read the letter at a position () and read Boolean variables, with Boolean connectives; and its statements are , assignment to a Boolean variable, sequential composition, conditionals and loops. The output of a run is the concatenation of the output letters produced. A for-transducer is in prenex form (Definition D.1.2) if it is a block of nested loops whose body is loop-free and produces at most one output letter per iteration, followed by a loop-free epilogue. For-transducers compute exactly the polyregular functions (Theorem D.1.1).
1 import Mathlib.Logic.Function.Basic 2 import Mathlib.Data.List.Basic 3 … module docstring, 27 lines 31 32 namespace Lax194892.ForTransducers 33 34 /-- Tests of a for-transducer. -/ 35 inductive ForTest (A : Type) : Type 36 /-- The value of a Boolean variable. -/ 37 | boolVar : ℕ → ForTest A 38 /-- The equality test `x == y` on position variables. -/ 39 | eqPos : ℕ → ℕ → ForTest A 40 /-- The order test `x <= y` on position variables. -/ 41 | lePos : ℕ → ℕ → ForTest A 42 /-- The label test `w[x] == a`. -/ 43 | label : ℕ → A → ForTest A 44 /-- Negation. -/ 45 | not : ForTest A → ForTest A 46 /-- Conjunction. -/ 47 | and : ForTest A → ForTest A → ForTest A 48 /-- Disjunction. -/ 49 | or : ForTest A → ForTest A → ForTest A 50 51 /-- Programs of a for-transducer. -/ 52 inductive ForProg (A B : Type) : Type 53 /-- The empty program. -/ 54 | skip : ForProg A B 55 /-- `output(b)`. -/ 56 | output : B → ForProg A B 57 /-- `X = true` / `X = false`. -/ 58 | assign : ℕ → Bool → ForProg A B 59 /-- Sequential composition `I ; J`. -/ 60 | seq : ForProg A B → ForProg A B → ForProg A B 61 /-- A conditional. -/ 62 | ite : ForTest A → ForProg A B → ForProg A B → ForProg A B 63 /-- `for x in positions(w)` (`true`) or `for x in positions_reverse(w)` (`false`). -/ 64 | loop : Bool → ℕ → ForProg A B → ForProg A B 65 66 namespace ForTest 67 68 variable {A : Type} 69 70 /-- The truth value of a test under valuations of the position and Boolean 71 variables. -/ 72 def Holds (w : List A) (pos : ℕ → ℕ) (bv : ℕ → Bool) : ForTest A → Prop 73 | boolVar i => bv i = true 74 | eqPos i j => pos i = pos j 75 | lePos i j => pos i ≤ pos j 76 | label i a => w[pos i]? = some a 77 | not t => ¬ Holds w pos bv t 78 | and t s => Holds w pos bv t ∧ Holds w pos bv s 79 | or t s => Holds w pos bv t ∨ Holds w pos bv s 80 81 end ForTest 82 83 /-- Running the body of a loop over a list of positions, threading the Boolean 84 valuation and concatenating the outputs. -/ 85 def forLoopRun {B : Type} (body : (ℕ → Bool) → ℕ → (ℕ → Bool) × List B) : 86 List ℕ → (ℕ → Bool) → (ℕ → Bool) × List B 87 | [], bv => (bv, []) 88 | p :: ps, bv => 89 let r := body bv p 90 let r' := forLoopRun body ps r.1 91 (r'.1, r.2 ++ r'.2) 92 93 namespace ForProg 94 95 variable {A B : Type} 96 97 open scoped Classical in 98 /-- The semantics of a program: the final Boolean valuation and the output. -/ 99 noncomputable def exec (w : List A) : 100 ForProg A B → (ℕ → ℕ) → (ℕ → Bool) → (ℕ → Bool) × List B 101 | skip, _, bv => (bv, []) 102 | output b, _, bv => (bv, [b]) 103 | assign i v, _, bv => (Function.update bv i v, []) 104 | seq P Q, pos, bv => 105 let r := exec w P pos bv 106 let r' := exec w Q pos r.1 107 (r'.1, r.2 ++ r'.2) 108 | ite t P Q, pos, bv => 109 if ForTest.Holds w pos bv t then exec w P pos bv else exec w Q pos bv 110 | loop dir x P, pos, bv => 111 forLoopRun (fun bv' p => exec w P (Function.update pos x p) bv') 112 (if dir then List.range w.length else (List.range w.length).reverse) bv 113 114 /-- The function computed by a for-transducer. -/ 115 noncomputable def eval (P : ForProg A B) (w : List A) : List B := 116 (exec w P (fun _ => 0) (fun _ => false)).2 117 118 /-- A program without loops. -/ 119 def LoopFree : ForProg A B → Prop 120 | skip => True 121 | output _ => True 122 | assign _ _ => True 123 | seq P Q => LoopFree P ∧ LoopFree Q 124 | ite _ P Q => LoopFree P ∧ LoopFree Q 125 | loop _ _ _ => False 126 127 /-- Nested loops `for x₁ in τ₁: ⋯ for x_k in τ_k: body`. -/ 128 def nestLoops : List (Bool × ℕ) → ForProg A B → ForProg A B 129 | [], body => body 130 | (d, x) :: rest, body => ForProg.loop d x (nestLoops rest body) 131 132 /-- A program produces at most one output letter per execution. -/ 133 def OutputsAtMostOne (P : ForProg A B) : Prop := 134 ∀ (w : List A) (pos : ℕ → ℕ) (bv : ℕ → Bool), ((exec w P pos bv).2).length ≤ 1 135 136 /-- Prenex form: nested loops whose body is loop-free and outputs at most one 137 letter per iteration, followed by a loop-free epilogue. -/ 138 def PrenexForm (P : ForProg A B) : Prop := 139 ∃ (ls : List (Bool × ℕ)) (body epilogue : ForProg A B), 140 LoopFree body ∧ LoopFree epilogue ∧ OutputsAtMostOne body ∧ 141 P = ForProg.seq (nestLoops ls body) epilogue 142 143 end ForProg 144 145 /-- A function computed by a for-transducer. -/ 146 def IsForTransducer {A B : Type} (f : List A → List B) : Prop := 147 ∃ P : ForProg A B, ∀ w, P.eval w = f w 148 149 end Lax194892.ForTransducers 150 -
Theorem D.1.1 as a biconditional, glued from its two halves taken as assumptions.
-
def
Lax194892.ForTransducerspp. 157–159For-transducers
A for-transducer (Section D.1 of Transducers) is an imperative program with loops ranging over the positions of the input string, in increasing or decreasing order. It has position variables, bound by the loops and read only, and Boolean variables, initially false and assignable; its tests compare positions (, ), read the letter at a position () and read Boolean variables, with Boolean connectives; and its statements are , assignment to a Boolean variable, sequential composition, conditionals and loops. The output of a run is the concatenation of the output letters produced. A for-transducer is in prenex form (Definition D.1.2) if it is a block of nested loops whose body is loop-free and produces at most one output letter per iteration, followed by a loop-free epilogue. For-transducers compute exactly the polyregular functions (Theorem D.1.1).
1 import Mathlib.Logic.Function.Basic 2 import Mathlib.Data.List.Basic 3 … module docstring, 27 lines 31 32 namespace Lax194892.ForTransducers 33 34 /-- Tests of a for-transducer. -/ 35 inductive ForTest (A : Type) : Type 36 /-- The value of a Boolean variable. -/ 37 | boolVar : ℕ → ForTest A 38 /-- The equality test `x == y` on position variables. -/ 39 | eqPos : ℕ → ℕ → ForTest A 40 /-- The order test `x <= y` on position variables. -/ 41 | lePos : ℕ → ℕ → ForTest A 42 /-- The label test `w[x] == a`. -/ 43 | label : ℕ → A → ForTest A 44 /-- Negation. -/ 45 | not : ForTest A → ForTest A 46 /-- Conjunction. -/ 47 | and : ForTest A → ForTest A → ForTest A 48 /-- Disjunction. -/ 49 | or : ForTest A → ForTest A → ForTest A 50 51 /-- Programs of a for-transducer. -/ 52 inductive ForProg (A B : Type) : Type 53 /-- The empty program. -/ 54 | skip : ForProg A B 55 /-- `output(b)`. -/ 56 | output : B → ForProg A B 57 /-- `X = true` / `X = false`. -/ 58 | assign : ℕ → Bool → ForProg A B 59 /-- Sequential composition `I ; J`. -/ 60 | seq : ForProg A B → ForProg A B → ForProg A B 61 /-- A conditional. -/ 62 | ite : ForTest A → ForProg A B → ForProg A B → ForProg A B 63 /-- `for x in positions(w)` (`true`) or `for x in positions_reverse(w)` (`false`). -/ 64 | loop : Bool → ℕ → ForProg A B → ForProg A B 65 66 namespace ForTest 67 68 variable {A : Type} 69 70 /-- The truth value of a test under valuations of the position and Boolean 71 variables. -/ 72 def Holds (w : List A) (pos : ℕ → ℕ) (bv : ℕ → Bool) : ForTest A → Prop 73 | boolVar i => bv i = true 74 | eqPos i j => pos i = pos j 75 | lePos i j => pos i ≤ pos j 76 | label i a => w[pos i]? = some a 77 | not t => ¬ Holds w pos bv t 78 | and t s => Holds w pos bv t ∧ Holds w pos bv s 79 | or t s => Holds w pos bv t ∨ Holds w pos bv s 80 81 end ForTest 82 83 /-- Running the body of a loop over a list of positions, threading the Boolean 84 valuation and concatenating the outputs. -/ 85 def forLoopRun {B : Type} (body : (ℕ → Bool) → ℕ → (ℕ → Bool) × List B) : 86 List ℕ → (ℕ → Bool) → (ℕ → Bool) × List B 87 | [], bv => (bv, []) 88 | p :: ps, bv => 89 let r := body bv p 90 let r' := forLoopRun body ps r.1 91 (r'.1, r.2 ++ r'.2) 92 93 namespace ForProg 94 95 variable {A B : Type} 96 97 open scoped Classical in 98 /-- The semantics of a program: the final Boolean valuation and the output. -/ 99 noncomputable def exec (w : List A) : 100 ForProg A B → (ℕ → ℕ) → (ℕ → Bool) → (ℕ → Bool) × List B 101 | skip, _, bv => (bv, []) 102 | output b, _, bv => (bv, [b]) 103 | assign i v, _, bv => (Function.update bv i v, []) 104 | seq P Q, pos, bv => 105 let r := exec w P pos bv 106 let r' := exec w Q pos r.1 107 (r'.1, r.2 ++ r'.2) 108 | ite t P Q, pos, bv => 109 if ForTest.Holds w pos bv t then exec w P pos bv else exec w Q pos bv 110 | loop dir x P, pos, bv => 111 forLoopRun (fun bv' p => exec w P (Function.update pos x p) bv') 112 (if dir then List.range w.length else (List.range w.length).reverse) bv 113 114 /-- The function computed by a for-transducer. -/ 115 noncomputable def eval (P : ForProg A B) (w : List A) : List B := 116 (exec w P (fun _ => 0) (fun _ => false)).2 117 118 /-- A program without loops. -/ 119 def LoopFree : ForProg A B → Prop 120 | skip => True 121 | output _ => True 122 | assign _ _ => True 123 | seq P Q => LoopFree P ∧ LoopFree Q 124 | ite _ P Q => LoopFree P ∧ LoopFree Q 125 | loop _ _ _ => False 126 127 /-- Nested loops `for x₁ in τ₁: ⋯ for x_k in τ_k: body`. -/ 128 def nestLoops : List (Bool × ℕ) → ForProg A B → ForProg A B 129 | [], body => body 130 | (d, x) :: rest, body => ForProg.loop d x (nestLoops rest body) 131 132 /-- A program produces at most one output letter per execution. -/ 133 def OutputsAtMostOne (P : ForProg A B) : Prop := 134 ∀ (w : List A) (pos : ℕ → ℕ) (bv : ℕ → Bool), ((exec w P pos bv).2).length ≤ 1 135 136 /-- Prenex form: nested loops whose body is loop-free and outputs at most one 137 letter per iteration, followed by a loop-free epilogue. -/ 138 def PrenexForm (P : ForProg A B) : Prop := 139 ∃ (ls : List (Bool × ℕ)) (body epilogue : ForProg A B), 140 LoopFree body ∧ LoopFree epilogue ∧ OutputsAtMostOne body ∧ 141 P = ForProg.seq (nestLoops ls body) epilogue 142 143 end ForProg 144 145 /-- A function computed by a for-transducer. -/ 146 def IsForTransducer {A B : Type} (f : List A → List B) : Prop := 147 ∃ P : ForProg A B, ∀ w, P.eval w = f w 148 149 end Lax194892.ForTransducers 150 -
thm✓
Lax194892.PrenexNormalFormp. 159Every for-transducer has a prenex form
Every for-transducer is equivalent to one in prenex form (Lemma D.1.3 of Transducers): a block of nested loops over positions, in increasing or decreasing order, whose body is loop-free and outputs at most one letter per iteration, followed by a loop-free epilogue. Loops are pulled outwards one at a time, Boolean variables recording which iterations have already been executed.
1 import Lax194892.ForTransducers 2 … module docstring, 16 lines 19 20 namespace Lax194892.PrenexNormalForm 21 22 open Lax194892.ForTransducers 23 24 /-- Every for-transducer program is equivalent to one in prenex form. -/ 25 axiom exists_prenexForm {A B : Type} (P : ForProg A B) : 26 ∃ P' : ForProg A B, P'.PrenexForm ∧ ∀ w, P'.eval w = P.eval w 27 28 end Lax194892.PrenexNormalForm 29 -
no assumptions
Every for-transducer is equivalent to one in prenex form (Lemma D.1.3), .
-
thm✓
Lax194892.ForCompositionp. 159For-transducers are closed under composition
The functions computed by for-transducers are closed under composition (Lemma D.1.4 of Transducers). The second program is run on the output of the first, in prenex form: an output position of the first program is a tuple of loop variables of its prenex form, so a loop of the second program over output positions becomes a block of loops over input positions, and its tests on output letters become the loop-free body of the first program.
1 import Lax194892.ForTransducers 2 … module docstring, 16 lines 19 20 namespace Lax194892.ForComposition 21 22 open Lax194892.ForTransducers 23 24 /-- The composition of two functions computed by for-transducers is computed by a 25 for-transducer. -/ 26 axiom isForTransducer_comp {A B C : Type} {f : List A → List B} {g : List B → List C} 27 (hf : IsForTransducer f) (hg : IsForTransducer g) : IsForTransducer (g ∘ f) 28 29 end Lax194892.ForComposition 30 -
⊢
Lax194892Proofs.Results.isForTransducer_comppp. 159–160no assumptions
Functions computed by for-transducers are closed under composition (Lemma D.1.4), .
-
Transducers, Part D: Polyregular Functions
-
def
Lax194892.MarkedSquaringp. 151Marked squaring
The marked squaring function (Example 33 of Transducers) copies an input string of length exactly times, underlining the first letters of the -th copy:
The output has length over the alphabet , one copy of the input alphabet underlined and one plain. It is the one prime function of quadratic growth that, added to the regular functions, generates the polyregular functions (Definition D.0.1).
1 import Mathlib.Data.List.Basic 2 … module docstring, 20 lines 23 24 namespace Lax194892.MarkedSquaring 25 26 /-- Marked squaring: `n` copies of an input of length `n`, the first `i` letters 27 of the `i`-th copy underlined. -/ 28 def markedSquare (A : Type) (w : List A) : List (A ⊕ A) := 29 ((List.range w.length).map 30 (fun i => (w.take (i + 1)).map Sum.inl ++ (w.drop (i + 1)).map Sum.inr)).flatten 31 32 end Lax194892.MarkedSquaring 33 -
def
Lax194892.PolyregularFunctionspp. 151–152Polyregular functions
A string-to-string function is polyregular (Definition D.0.1 of Transducers) if it can be obtained as a finite composition of functions each of which is either regular or a marked squaring function:
The polyregular functions are the top step of the book's transducer ladder; Part D shows that they are the functions of for-transducers and of pebble transducers.
1 import Lax765601.CompositionClosure 2 import Lax916827.RegularFunctions 3 import Lax194892.MarkedSquaring 4 … module docstring, 19 lines 24 25 namespace Lax194892.PolyregularFunctions 26 27 open Lax765601.CompositionClosure Lax916827.RegularFunctions Lax194892.MarkedSquaring 28 29 /-- The family of prime polyregular functions: regular functions and marked 30 squaring, up to a renaming of the alphabets. -/ 31 def PolyregularFam : Family := fun A B f => 32 IsRegularFun f ∨ 33 (∃ (A₀ : Type) (e : A ≃ A₀) (e' : B ≃ A₀ ⊕ A₀), 34 ∀ w, f w = (markedSquare A₀ (w.map e)).map e'.symm) 35 36 /-- A function is polyregular if it is a finite composition of regular functions 37 and marked squaring. -/ 38 def IsPolyregular {A B : Type} (f : List A → List B) : Prop := CompClosure PolyregularFam A B f 39 40 end Lax194892.PolyregularFunctions 41 -
thm✓
Lax194892.PolyregularContinuityp. 152Polyregular functions are continuous
Polyregular functions are continuous (Theorem D.0.2 of Transducers): regular functions are, continuity is preserved by composition, and marked squaring is continuous — an automaton for the target language is run on the marked square from right to left, remembering the state transformation of the underlined suffix and how the state transformation of the prefix transforms the contribution of the suffix.
1 import Lax765601.Continuity 2 import Lax194892.PolyregularFunctions 3 … module docstring, 16 lines 20 21 namespace Lax194892.PolyregularContinuity 22 23 open Lax765601.Continuity Lax194892.PolyregularFunctions 24 25 /-- A polyregular function is continuous. -/ 26 axiom continuous_of_isPolyregular {A B : Type} [Finite A] [Finite B] {f : List A → List B} 27 (hf : IsPolyregular f) : Continuous f 28 29 end Lax194892.PolyregularContinuity 30 -
⊢
Lax194892Proofs.Results.continuous_of_isPolyregularpp. 152–153no assumptions
Polyregular functions are continuous (Theorem D.0.2): induction on the composition tree, with Theorem C.1.1 for the regular primes and a direct automaton for marked squaring ().
-
thm✓
Lax194892.PebbleContinuityp. 165Pebble transducers are continuous
Pebble transducers compute continuous functions (Theorem D.2.1 of Transducers). The languages recognised by pebble automata — pebble transducers with a yes/no answer — are regular, by induction on the number of pebbles; running an automaton for the target language on the output turns the transducer into a pebble automaton.
1 import Lax765601.Continuity 2 import Lax194892.PebbleTransducers 3 … module docstring, 15 lines 19 20 namespace Lax194892.PebbleContinuity 21 22 open Lax765601.Continuity Lax194892.PebbleTransducers 23 24 /-- A function computed by a pebble transducer is continuous. -/ 25 axiom continuous_of_isPebbleTransducer {A B : Type} [Finite A] [Finite B] {f : List A → List B} 26 (hf : IsPebbleTransducer f) : Continuous f 27 28 end Lax194892.PebbleContinuity 29 -
def
Lax194892.PebbleTransducersp. 165Pebble transducers
A pebble transducer (Section D.2 of Transducers) extends a two-way transducer by a stack of at most pebbles pointing to gaps of the input string; the topmost pebble is the head, and only it can be moved. The transducer has a finite set of states with an initial state; it looks at its state and, for every pebble on the stack, at the two input letters adjacent to it and the set of pebbles in the same place, and deterministically chooses a new state and an action: output a letter, move the head one position left or right, push a new pebble at the first gap, pop the head, or terminate. It computes on if the run from the initial state with an empty stack terminates with output . Pebble transducers compute exactly the functions of for-transducers (Theorem D.2.4), hence the polyregular functions.
1 import Mathlib.Data.Finite.Defs 2 import Mathlib.Data.List.Basic 3 … module docstring, 27 lines 31 32 namespace Lax194892.PebbleTransducers 33 34 /-- What a pebble transducer sees: for every pebble on the stack, from the 35 bottom, the two adjacent letters and the pebbles in the same place. -/ 36 abbrev PebbleView (A : Type) := List ((Option A × Option A) × List Bool) 37 38 /-- The view of the input from a stack of gaps. -/ 39 def viewOf {A : Type} (w : List A) (st : List ℕ) : PebbleView A := 40 st.map (fun p => ((if p = 0 then none else w[p - 1]?, w[p]?), 41 st.map (fun q => decide (q = p)))) 42 43 /-- The actions of a pebble transducer. -/ 44 inductive PebbleAction (B : Type) : Type 45 /-- Output a letter. -/ 46 | out : B → PebbleAction B 47 /-- Move the head right (`true`) or left (`false`). -/ 48 | move : Bool → PebbleAction B 49 /-- Push a new pebble at the first gap. -/ 50 | push : PebbleAction B 51 /-- Pop the topmost pebble. -/ 52 | pop : PebbleAction B 53 /-- Terminate. -/ 54 | terminate : PebbleAction B 55 56 /-- A `k`-pebble transducer: a deterministic machine with a stack of at most `k` 57 pebbles pointing to gaps of the input. -/ 58 structure Pebble (A B Q : Type) (k : ℕ) where 59 /-- The initial state. -/ 60 init : Q 61 /-- The transition function. -/ 62 step : Q → PebbleView A → Q × PebbleAction B 63 64 /-- A configuration: the state and the stack of gaps (from the bottom), or the 65 halting vertex. -/ 66 inductive PebbleCfg (Q : Type) : Type 67 | conf : Q → List ℕ → PebbleCfg Q 68 | halt : PebbleCfg Q 69 70 namespace Pebble 71 72 variable {A B Q : Type} {k : ℕ} 73 74 /-- One step: the produced output and the next configuration, undefined if the 75 head leaves the input, the stack bound is exceeded, or an empty stack is popped. -/ 76 def stepCfg (M : Pebble A B Q k) (w : List A) : PebbleCfg Q → Option (List B × PebbleCfg Q) 77 | PebbleCfg.halt => none 78 | PebbleCfg.conf q st => 79 let r := M.step q (viewOf w st) 80 match r.2 with 81 | PebbleAction.out b => some ([b], PebbleCfg.conf r.1 st) 82 | PebbleAction.terminate => some ([], PebbleCfg.halt) 83 | PebbleAction.push => 84 if st.length < k then some ([], PebbleCfg.conf r.1 (st ++ [0])) else none 85 | PebbleAction.pop => 86 if st = [] then none else some ([], PebbleCfg.conf r.1 st.dropLast) 87 | PebbleAction.move dir => 88 match st.getLast? with 89 | none => none 90 | some p => 91 if dir then 92 (if p < w.length then some ([], PebbleCfg.conf r.1 (st.dropLast ++ [p + 1])) 93 else none) 94 else 95 (if 0 < p then some ([], PebbleCfg.conf r.1 (st.dropLast ++ [p - 1])) 96 else none) 97 98 /-- Reachability in the configuration graph, recording the output. -/ 99 inductive Reaches (M : Pebble A B Q k) (w : List A) : 100 PebbleCfg Q → List B → PebbleCfg Q → Prop 101 | refl (c : PebbleCfg Q) : Reaches M w c [] c 102 | step {c c' c'' : PebbleCfg Q} {o o' : List B} : 103 M.stepCfg w c = some (o, c') → Reaches M w c' o' c'' → Reaches M w c (o ++ o') c'' 104 105 /-- The transducer produces `v` on `w`. -/ 106 def Computes (M : Pebble A B Q k) (w : List A) (v : List B) : Prop := 107 M.Reaches w (PebbleCfg.conf M.init []) v PebbleCfg.halt 108 109 end Pebble 110 111 /-- A function computed by a pebble transducer with finitely many states, for some 112 bound on the number of pebbles. -/ 113 def IsPebbleTransducer {A B : Type} (f : List A → List B) : Prop := 114 ∃ (k : ℕ) (Q : Type) (_ : Finite Q) (M : Pebble A B Q k), ∀ w, M.Computes w (f w) 115 116 end Lax194892.PebbleTransducers 117 -
no assumptions
Pebble transducers compute continuous functions (Theorem D.2.1), .
-
thm✓
Lax194892.PebbleReachabilityp. 166Reachability between configurations of a pebble transducer is regular
Reachability between two configurations of a -pebble transducer is definable: there is an mso formula over configurations which holds if some run begins in and ends in (Lemma D.2.2 of Transducers). Reachability is reduced, by induction on the height, to reachability between configurations that share their lower pebbles, which is checked by a pebble automaton with one pebble more.
1 import Mathlib.Computability.DFA 2 import Lax194892.PebbleConfigurationEncoding 3 … module docstring, 24 lines 28 29 namespace Lax194892.PebbleReachability 30 31 open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding 32 33 /-- The encodings of pairs of configurations connected by a run form a regular 34 language. -/ 35 axiom exists_regular_reachLang {A B Q : Type} {k : ℕ} [Finite A] [Finite Q] (M : Pebble A B Q k) : 36 ∃ L : Language (PairLetter A Q k), L.IsRegular ∧ 37 ∀ (q₁ q₂ : Q) (sts stt : List ℕ) (w : List A), 38 (∀ p ∈ sts, p ≤ w.length) → (∀ p ∈ stt, p ≤ w.length) → 39 sts.length ≤ k → stt.length ≤ k → 40 (pairEnc q₁ q₂ sts stt w ∈ L ↔ 41 ∃ v, M.Reaches w (PebbleCfg.conf q₁ sts) v (PebbleCfg.conf q₂ stt)) 42 43 end Lax194892.PebbleReachability 44 -
def
Lax194892.PebbleConfigurationEncodingp. 166String representations of pebble configurations, and balanced runs
Section D.2 of Transducers represents a configuration of a -pebble transducer on an input — a state and a stack of at most gaps of — as a string with one letter per gap of , the letter of a gap recording the state, the input letter that follows the gap and the set of pebbles sitting in the gap; the results on reachability speak about a pair of configurations at a time, encoded together. A run between two configurations of height is balanced if the pebble at height is never popped during it, although it may be moved.
1 import Lax194892.PebbleTransducers 2 … module docstring, 23 lines 26 27 namespace Lax194892.PebbleConfigurationEncoding 28 29 open Lax194892.PebbleTransducers 30 31 /-- Reachability along runs whose configurations all have height at least `ℓ`: 32 the topmost `ℓ` pebbles are never popped. -/ 33 inductive RestrReaches {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (ℓ : ℕ) : 34 PebbleCfg Q → PebbleCfg Q → Prop 35 /-- The empty run. -/ 36 | refl (q : Q) (st : List ℕ) (h : ℓ ≤ st.length) : 37 RestrReaches M w ℓ (PebbleCfg.conf q st) (PebbleCfg.conf q st) 38 /-- One step from a configuration of height at least `ℓ`. -/ 39 | step {q : Q} {st : List ℕ} {c' c'' : PebbleCfg Q} {o : List B} (h : ℓ ≤ st.length) 40 (hs : M.stepCfg w (PebbleCfg.conf q st) = some (o, c')) 41 (hr : RestrReaches M w ℓ c' c'') : 42 RestrReaches M w ℓ (PebbleCfg.conf q st) c'' 43 44 /-- A balanced run between two configurations of height `ℓ`: the pebble at 45 height `ℓ` is never popped. -/ 46 def BalancedRun {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (ℓ : ℕ) 47 (c c' : PebbleCfg Q) : Prop := 48 RestrReaches M w ℓ c c' 49 50 /-- The pebbles of the stack `st` sitting in the gap `p`. -/ 51 def ann (k : ℕ) (st : List ℕ) (p : ℕ) : Fin k → Bool := fun i => decide (st[(i : ℕ)]? = some p) 52 53 /-- A letter of the representation of a pair of configurations: the two states, the 54 input letter following the gap, and the pebbles of each configuration in the gap. -/ 55 abbrev PairLetter (A Q : Type) (k : ℕ) := Q × Q × Option A × (Fin k → Bool) × (Fin k → Bool) 56 57 /-- The string representation of the pair of configurations `(q₁, sts)` and 58 `(q₂, stt)` of the input `w`: one letter per gap. -/ 59 def pairEnc {A Q : Type} {k : ℕ} (q₁ q₂ : Q) (sts stt : List ℕ) (w : List A) : 60 List (PairLetter A Q k) := 61 (List.range (w.length + 1)).map fun p => (q₁, q₂, w[p]?, ann k sts p, ann k stt p) 62 63 end Lax194892.PebbleConfigurationEncoding 64 -
⊢
Lax194892Proofs.Results.exists_regular_reachLangpp. 166–168no assumptions
The string representations of pairs of configurations connected by a run form a regular language (Lemma D.2.2), .
-
thm✓
Lax194892.BalancedRunReachabilityp. 167Balanced runs between configurations are regular
For every height , the existence of a balanced run between two configurations and of height — sharing the stack of the lower pebbles, with the state and the position of the top pebble — is mso-definable (Claim D.2.3 of Transducers): during a balanced run the pebble at height is never popped, although it may be moved.
1 import Mathlib.Computability.DFA 2 import Lax194892.PebbleConfigurationEncoding 3 … module docstring, 18 lines 22 23 namespace Lax194892.BalancedRunReachability 24 25 open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding 26 27 /-- The encodings of pairs of configurations of height `ℓ` connected by a balanced 28 run form a regular language. -/ 29 axiom exists_regular_balancedLang {A B Q : Type} {k : ℕ} [Finite A] [Finite Q] 30 (M : Pebble A B Q k) (ℓ : ℕ) (hℓ1 : 1 ≤ ℓ) (hℓk : ℓ ≤ k) : 31 ∃ L : Language (PairLetter A Q k), L.IsRegular ∧ 32 ∀ (q₁ q₂ : Q) (x : List ℕ) (p₁ p₂ : ℕ) (w : List A), 33 (∀ p ∈ x, p ≤ w.length) → p₁ ≤ w.length → p₂ ≤ w.length → x.length = ℓ - 1 → 34 (pairEnc q₁ q₂ (x ++ [p₁]) (x ++ [p₂]) w ∈ L ↔ 35 BalancedRun M w ℓ (PebbleCfg.conf q₁ (x ++ [p₁])) (PebbleCfg.conf q₂ (x ++ [p₂]))) 36 37 end Lax194892.BalancedRunReachability 38 -
⊢
Lax194892Proofs.Results.exists_regular_balancedLangpp. 167–168no assumptions
For every height , the string representations of pairs of configurations of height connected by a balanced run form a regular language (Claim D.2.3), .
-
thm✓
Lax194892.PebbleIffForp. 168Pebble transducers and for-transducers compute the same functions
Pebble transducers and for-transducers compute the same string-to-string functions (Theorem D.2.4 of Transducers). The two implications are the separate statements and ; this statement is their conjunction.
1 import Lax194892.PebbleTransducers 2 import Lax194892.ForTransducers 3 … module docstring, 14 lines 18 19 namespace Lax194892.PebbleIffFor 20 21 open Lax194892.PebbleTransducers Lax194892.ForTransducers 22 23 /-- A function is computed by a pebble transducer if and only if it is computed by 24 a for-transducer. -/ 25 axiom isPebbleTransducer_iff_isForTransducer {A B : Type} [Finite A] [Finite B] 26 (f : List A → List B) : IsPebbleTransducer f ↔ IsForTransducer f 27 28 end Lax194892.PebbleIffFor 29 -
thm✓
Lax194892.ForOfPebblep. 168Pebble transducers are computed by for-transducers
Every function computed by a pebble transducer is computed by a for-transducer (Theorem D.2.4 of Transducers, the implication from pebble to for-transducer). The run is organised as a tree of configurations; the children of a configuration are produced by a for-transducer (Lemma D.2.5), and iterating this over the height of the stack, with the output letters read off the leaves, gives a polyregular function, hence a for-transducer.
1 import Lax194892.PebbleTransducers 2 import Lax194892.ForTransducers 3 … module docstring, 18 lines 22 23 namespace Lax194892.ForOfPebble 24 25 open Lax194892.PebbleTransducers Lax194892.ForTransducers 26 27 /-- A function computed by a pebble transducer is computed by a for-transducer. -/ 28 axiom isForTransducer_of_isPebbleTransducer {A B : Type} [Finite A] [Finite B] 29 {f : List A → List B} (hf : IsPebbleTransducer f) : IsForTransducer f 30 31 end Lax194892.ForOfPebble 32 -
thm✓
Lax194892.PebbleOfForp. 168For-transducers are computed by pebble transducers
Every function computed by a for-transducer is computed by a pebble transducer (Theorem D.2.4 of Transducers, the implication from for-transducer to pebble). In prenex form the loop variables are pushed as pebbles, in the order of the loops; the loop-free body is evaluated by a one-way pass with the pebbles in place, since it can only compare positions, read letters and read Boolean variables, which the state carries.
1 import Lax194892.PebbleTransducers 2 import Lax194892.ForTransducers 3 … module docstring, 16 lines 20 21 namespace Lax194892.PebbleOfFor 22 23 open Lax194892.PebbleTransducers Lax194892.ForTransducers 24 25 /-- A function computed by a for-transducer is computed by a pebble transducer. -/ 26 axiom isPebbleTransducer_of_isForTransducer {A B : Type} [Finite A] [Finite B] 27 {f : List A → List B} (hf : IsForTransducer f) : IsPebbleTransducer f 28 29 end Lax194892.PebbleOfFor 30 -
thm✓
Lax194892.ChildrenOfConfigurationp. 169A for-transducer produces the children of a configuration
For every -pebble transducer there is a for-transducer which inputs the string representation of a configuration and outputs all children of that configuration, as the concatenation of their string representations in order of execution (Lemma D.2.5 of Transducers). It is the composition of Claims D.2.6 and D.2.7: from the configuration to its child configuration graph, and from the graph to the children.
1 import Lax194892.ForTransducers 2 import Lax194892.ChildConfigurationGraphs 3 … module docstring, 21 lines 25 26 namespace Lax194892.ChildrenOfConfiguration 27 28 open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding 29 Lax194892.ChildConfigurationGraphs Lax194892.ForTransducers 30 31 /-- A for-transducer maps the representation of a configuration to the 32 concatenation of the representations of its children. -/ 33 axiom exists_forTransducer_children {A B Q : Type} [Finite A] [Finite Q] {k : ℕ} 34 (M : Pebble A B Q k) : 35 ∃ f : List (ConfLetter A Q k) → List (ConfLetter A Q k), IsForTransducer f ∧ 36 ∀ (q₀ : Q) (st : List ℕ) (w : List A) (ch : ℕ → Vtx Q) (m : ℕ), 37 (∀ p, p ∈ st → p ≤ w.length) → st.length < k → 38 IsChildSeq M w q₀ st ch m → 39 f (confEnc q₀ st w) 40 = ((List.range (m + 1)).map fun t => confEnc (ch t).1 (st ++ [(ch t).2]) w).flatten 41 42 end Lax194892.ChildrenOfConfiguration 43 -
def
Lax194892.ChildConfigurationGraphsp. 169Children of a configuration and child configuration graphs
Section D.2 of Transducers organises a run of a pebble transducer as a tree: the children of a configuration of height are the configurations of height that the run visits after it before coming back down to height ; between two consecutive children the run stays above height . The children are described by the child configuration graph: a directed graph whose vertices are pairs of a state and a gap — the position of the moving pebble — with an edge for the run between two consecutive children, annotated with the input string and the positions of the fixed pebbles . Like a configuration, a child configuration graph is represented as a string over a fixed finite alphabet with one letter per gap of the input, and the output of the graph is the concatenation of the string representations of the children in order of execution. Lemma D.2.5 and Claims D.2.6–D.2.7 say that a for-transducer computes the graph from the configuration and the children from the graph.
1 import Mathlib.Data.Nat.Find 2 import Mathlib.Data.Finite.Defs 3 import Lax194892.PebbleConfigurationEncoding 4 … module docstring, 38 lines 43 44 namespace Lax194892.ChildConfigurationGraphs 45 46 open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding 47 48 -- ## The children of a configuration 49 50 /-- The stack has height at least `h`; the halting vertex has no height. -/ 51 def HeightGe {Q : Type} (h : ℕ) : PebbleCfg Q → Prop 52 | PebbleCfg.conf _ st => h ≤ st.length 53 | PebbleCfg.halt => False 54 55 /-- A run of at least one step whose intermediate configurations have height at 56 least `h`. -/ 57 inductive StrictAbove {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (h : ℕ) : 58 PebbleCfg Q → PebbleCfg Q → Prop 59 /-- A single step. -/ 60 | one {c c' : PebbleCfg Q} {o : List B} : M.stepCfg w c = some (o, c') → StrictAbove M w h c c' 61 /-- A step to a configuration of height at least `h`, followed by such a run. -/ 62 | cons {c c' c'' : PebbleCfg Q} {o : List B} : M.stepCfg w c = some (o, c') → HeightGe h c' → 63 StrictAbove M w h c' c'' → StrictAbove M w h c c'' 64 65 /-- A vertex of a child configuration graph: a state and a gap. -/ 66 abbrev Vtx (Q : Type) := Q × ℕ 67 68 /-- The configuration of the child `v` of a configuration with stack `st`: the 69 moving pebble sits on top. -/ 70 def cfgOf {Q : Type} (st : List ℕ) (v : Vtx Q) : PebbleCfg Q := PebbleCfg.conf v.1 (st ++ [v.2]) 71 72 /-- `v'` is the child following the child `v`: the run from `v` first returns to 73 the children's height at `v'`. -/ 74 def NextChild {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (st : List ℕ) 75 (v v' : Vtx Q) : Prop := 76 StrictAbove M w (st.length + 2) (cfgOf st v) (cfgOf st v') 77 78 /-- `v` is the first child of the configuration `(q, st)`. -/ 79 def FirstChild {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (q : Q) (st : List ℕ) 80 (v : Vtx Q) : Prop := 81 StrictAbove M w (st.length + 2) (PebbleCfg.conf q st) (cfgOf st v) 82 83 /-- `ch 0, …, ch m` is the list of the children of `(q, st)`, in order of 84 execution. -/ 85 structure IsChildSeq {A B Q : Type} {k : ℕ} (M : Pebble A B Q k) (w : List A) (q : Q) 86 (st : List ℕ) (ch : ℕ → Vtx Q) (m : ℕ) : Prop where 87 /-- The list starts with the first child. -/ 88 first : FirstChild M w q st (ch 0) 89 /-- Each child is followed by the next one. -/ 90 next : ∀ t < m, NextChild M w st (ch t) (ch (t + 1)) 91 /-- The last child has no successor. -/ 92 stop : ∀ v, ¬ NextChild M w st (ch m) v 93 94 -- ## String representations 95 96 /-- A letter of the representation of a configuration: the state, the input letter 97 following the gap, and the pebbles in the gap. -/ 98 abbrev ConfLetter (A Q : Type) (k : ℕ) := Q × Option A × (Fin k → Bool) 99 100 /-- The string representation of the configuration `(q, st)` of `w`: one letter per 101 gap. -/ 102 def confEnc {A Q : Type} {k : ℕ} (q : Q) (st : List ℕ) (w : List A) : List (ConfLetter A Q k) := 103 (List.range (w.length + 1)).map fun p => (q, w[p]?, ann k st p) 104 105 /-- The direction of an edge: inside the column, one column right, one column left. -/ 106 abbrev Dir := Option Bool 107 108 /-- The column that the direction `d` leads to from the column `p`. -/ 109 def dest (p : ℕ) : Dir → Option ℕ 110 | none => some p 111 | some true => some (p + 1) 112 | some false => if p = 0 then none else some (p - 1) 113 114 /-- The direction from the column `a` to the adjacent column `b`. -/ 115 def dirOf (a b : ℕ) : Dir := if b = a then none else if a < b then some true else some false 116 117 /-- A letter of the representation of a child configuration graph: one gap of the 118 input, with the input letter, the fixed pebbles, the index of the moving pebble, 119 the states that are the first child in this column, and the outgoing and 120 incoming edges of the vertices of this column. -/ 121 structure CGLetter (A Q : Type) (k : ℕ) where 122 /-- The input letter following this gap, absent for the last gap. -/ 123 lett : Option A 124 /-- The fixed pebbles sitting in this gap. -/ 125 peb : Fin k → Bool 126 /-- The index of the moving pebble. -/ 127 nid : Fin k 128 /-- The states `q` for which `(q, this column)` is the first child. -/ 129 src : Q → Bool 130 /-- The outgoing edge of `(q, this column)`. -/ 131 nxt : Q → Option (Q × Dir) 132 /-- The incoming edge of `(q, this column)`. -/ 133 prv : Q → Option (Q × Dir) 134 135 open scoped Classical in 136 /-- The index at which `v` occurs among the first `m` children, if any. -/ 137 noncomputable def idxAt {Q : Type} (ch : ℕ → Vtx Q) (m : ℕ) (v : Vtx Q) : Option ℕ := 138 if h : ∃ t, t < m ∧ ch t = v then some (Nat.find h) else none 139 140 open scoped Classical in 141 /-- The index `t < m` such that `v` is the child following `ch t`, if any. -/ 142 noncomputable def idxSuccAt {Q : Type} (ch : ℕ → Vtx Q) (m : ℕ) (v : Vtx Q) : Option ℕ := 143 if h : ∃ t, t < m ∧ ch (t + 1) = v then some (Nat.find h) else none 144 145 open scoped Classical in 146 /-- The representation of the child configuration graph whose children are 147 `ch 0, …, ch m`, over an input with `n + 1` gaps carrying the letters `lett` and 148 the fixed pebbles `peb`, the moving pebble having the index `nid`. -/ 149 noncomputable def cgOfPath {A Q : Type} {k : ℕ} (lett : ℕ → Option A) (peb : ℕ → Fin k → Bool) 150 (nid : Fin k) (n : ℕ) (ch : ℕ → Vtx Q) (m : ℕ) : List (CGLetter A Q k) := 151 (List.range (n + 1)).map fun j => 152 { lett := lett j 153 peb := peb j 154 nid := nid 155 src := fun q' => decide ((q', j) = ch 0) 156 nxt := fun q' => (idxAt ch m (q', j)).map fun t => ((ch (t + 1)).1, dirOf j (ch (t + 1)).2) 157 prv := fun q' => (idxSuccAt ch m (q', j)).map fun t => ((ch t).1, dirOf (ch t).2 j) } 158 159 /-- The representation of the child configuration graph of a configuration of `w` 160 with stack `st`, moving pebble `nid` and children `ch 0, …, ch m`. -/ 161 noncomputable def cgOfChildren {A Q : Type} {k : ℕ} (w : List A) (st : List ℕ) (nid : Fin k) 162 (ch : ℕ → Vtx Q) (m : ℕ) : List (CGLetter A Q k) := 163 cgOfPath (fun j => w[j]?) (fun j => ann k st j) nid w.length ch m 164 165 -- ## Reading the children off a represented graph 166 167 /-- The vertex that the edge out of `v` leads to, if any. -/ 168 def succOf {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : Vtx Q) : Option (Vtx Q) := 169 (u[v.2]?).bind fun c => (c.nxt v.1).bind fun x => (dest v.2 x.2).map fun p' => (x.1, p') 170 171 /-- `v` is marked as the first child. -/ 172 def IsSrc {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : Vtx Q) : Prop := 173 ∃ c, u[v.2]? = some c ∧ c.src v.1 = true 174 175 /-- The representation of the child that the vertex `v` stands for: the state of 176 `v`, the input letters and the fixed pebbles of the graph, and the moving pebble 177 in the column of `v`. -/ 178 def confAt {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : Vtx Q) : 179 List (ConfLetter A Q k) := 180 u.mapIdx fun j c => (v.1, c.lett, fun i => c.peb i || (decide (i = c.nid) && decide (v.2 = j))) 181 182 /-- The letter to the left of the gap `i`. -/ 183 def leftLet {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (i : ℕ) : Option (CGLetter A Q k) := 184 if i = 0 then none else u[i - 1]? 185 186 open Classical in 187 /-- The local consistency test on two adjacent letters: every edge recorded by 188 `nxt` between or inside their columns is recorded by `prv` at its target, and a 189 vertex marked as the first child has no incoming edge. -/ 190 noncomputable def pairOK {A Q : Type} {k : ℕ} (a b : Option (CGLetter A Q k)) : Bool := decide ( 191 (∀ q q' : Q, ∀ ca cb, a = some ca → b = some cb → ca.nxt q = some (q', some true) → 192 cb.prv q' = some (q, some true)) ∧ 193 (∀ q q' : Q, ∀ ca cb, a = some ca → b = some cb → cb.nxt q = some (q', some false) → 194 ca.prv q' = some (q, some false)) ∧ 195 (∀ q q' : Q, ∀ cb, b = some cb → cb.nxt q = some (q', none) → cb.prv q' = some (q, none)) ∧ 196 (∀ q : Q, ∀ cb, b = some cb → cb.src q = true → cb.prv q = none)) 197 198 /-- The string is locally consistent at every gap. -/ 199 def Chk {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) : Prop := 200 ∀ i ≤ u.length, pairOK (leftLet u i) u[i]? = true 201 202 /-- `p 0, …, p m` is the run of children described by the locally consistent 203 string `u`: `p 0` is the unique first child, each `p (t+1)` is reached from `p t` 204 by the recorded edge, and `p m` has no outgoing edge. -/ 205 structure CGPath {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (m : ℕ) (p : ℕ → Vtx Q) : 206 Prop where 207 /-- The string is locally consistent. -/ 208 chk : Chk u 209 /-- `p 0` is the unique vertex marked as the first child. -/ 210 srcEq : ∀ v, IsSrc u v ↔ v = p 0 211 /-- Every vertex of the run sits in a real column. -/ 212 inRange : ∀ t ≤ m, (u[(p t).2]?).isSome 213 /-- Consecutive children are joined by the recorded edge. -/ 214 step : ∀ t < m, succOf u (p t) = some (p (t + 1)) 215 /-- The last child has no outgoing edge. -/ 216 last : succOf u (p m) = none 217 218 /-- The concatenation of the representations of the children, in order. -/ 219 def cgOut {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (m : ℕ) (p : ℕ → Vtx Q) : 220 List (ConfLetter A Q k) := 221 ((List.range (m + 1)).map fun t => confAt u (p t)).flatten 222 223 /-- `v` is the string representation of the children of the configuration whose 224 child configuration graph `u` represents. -/ 225 def CGOutIs {A Q : Type} {k : ℕ} (u : List (CGLetter A Q k)) (v : List (ConfLetter A Q k)) : 226 Prop := 227 ∃ m p, CGPath u m p ∧ v = cgOut u m p 228 229 end Lax194892.ChildConfigurationGraphs 230 -
no assumptions
A for-transducer maps the string representation of a configuration to the concatenation of the representations of its children (Lemma D.2.5), : the composition (Lemma D.1.4) of the for-transducers of Claims D.2.6 and D.2.7.
-
thm✓
Lax194892.ChildGraphOfConfigurationp. 170A for-transducer produces the child configuration graph
There is a for-transducer which inputs the string representation of a configuration and outputs the string representation of its child configuration graph (Claim D.2.6 of Transducers). Each letter of the graph is a Boolean combination of regular properties of the configuration with one marked gap — whether a given pair of children in adjacent columns is joined by a balanced run (Claim D.2.3) — so the graph is computed by a rational function, hence by a for-transducer.
1 import Lax194892.ForTransducers 2 import Lax194892.ChildConfigurationGraphs 3 … module docstring, 20 lines 24 25 namespace Lax194892.ChildGraphOfConfiguration 26 27 open Lax194892.PebbleTransducers Lax194892.PebbleConfigurationEncoding 28 Lax194892.ChildConfigurationGraphs Lax194892.ForTransducers 29 30 /-- A for-transducer maps the representation of a configuration to the 31 representation of its child configuration graph. -/ 32 axiom exists_forTransducer_childGraph {A B Q : Type} [Finite A] [Finite Q] {k : ℕ} 33 (M : Pebble A B Q k) : 34 ∃ f : List (ConfLetter A Q k) → List (CGLetter A Q k), IsForTransducer f ∧ 35 ∀ (q₀ : Q) (st : List ℕ) (w : List A) (ch : ℕ → Vtx Q) (m : ℕ) (nid : Fin k), 36 (∀ p, p ∈ st → p ≤ w.length) → st.length < k → (nid : ℕ) = st.length → 37 IsChildSeq M w q₀ st ch m → 38 f (confEnc q₀ st w) = cgOfChildren w st nid ch m 39 40 end Lax194892.ChildGraphOfConfiguration 41 -
no assumptions
A for-transducer maps the string representation of a configuration to the representation of its child configuration graph (Claim D.2.6), .
-
thm✓
Lax194892.ChildrenOfChildGraphp. 170A for-transducer reads the children off a child configuration graph
There is a for-transducer which inputs the string representation of a child configuration graph and outputs the concatenation of the string representations of the corresponding child configurations (Claim D.2.7 of Transducers). A two-pebble transducer walks along the path of the graph, one pebble marking the current child and the other printing its representation, and pebble transducers are for-transducers (Theorem D.2.4); the book instead proceeds by induction on the width of the graph, as for snake graphs.
1 import Lax194892.ForTransducers 2 import Lax194892.ChildConfigurationGraphs 3 … module docstring, 19 lines 23 24 namespace Lax194892.ChildrenOfChildGraph 25 26 open Lax194892.ChildConfigurationGraphs Lax194892.ForTransducers 27 28 /-- A for-transducer maps the representation of a child configuration graph to the 29 concatenation of the representations of the children. -/ 30 axiom exists_forTransducer_cgOut {A Q : Type} [Finite A] [Finite Q] (k : ℕ) : 31 ∃ f : List (CGLetter A Q k) → List (ConfLetter A Q k), 32 IsForTransducer f ∧ ∀ u v, CGOutIs u v → f u = v 33 34 end Lax194892.ChildrenOfChildGraph 35 -
⊢
Lax194892Proofs.Results.exists_forTransducer_cgOutpp. 170–171no assumptions
A for-transducer maps the string representation of a child configuration graph to the concatenation of the representations of the children (Claim D.2.7), .
Loading the paper…