Lax765601.MapLiftingDecomposition
Map lifting preserves decompositions into primes
concepts/Lax765601/MapLiftingDecomposition.lean · lax-765601
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
In the paper
- page 21 of the paper of lax-157538, Transducers
Theorem
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.
Lean source view on GitHub
| 1 | import Lax765601.PrimeMealyMachines |
| 2 | import Lax765601.MapLifting |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Map lifting preserves decompositions into primes |
| 7 | type: theorem |
| 8 | --- |
| 9 | If a Mealy machine decomposes into prime Mealy machines, then so does its map |
| 10 | lifting (Lemma A.2.4 of *Transducers*). Since map lifting commutes with |
| 11 | composition, it suffices to lift a single prime. A flip-flop is lifted by |
| 12 | resetting its state at every separator. A reversible machine needs more care, |
| 13 | because resetting would break reversibility: the book computes, by a reversible |
| 14 | machine, the state transformation of every prefix in the variant |
| 15 | where the separator does nothing, stores the value at the last separator by a |
| 16 | flip-flop delay machine, and recovers the state transformation of the current |
| 17 | block by the cancellation law , |
| 18 | all of which is a one-state machine's work. |
| 19 | |
| 20 | # Formalization notes |
| 21 | |
| 22 | Finiteness of the input alphabet is assumed; the finiteness of the output |
| 23 | alphabet, which the book assumes globally, is not needed here and is dropped. |
| 24 | The map lifting is `MapLifting.mapLift`, over the alphabets `Option A` and |
| 25 | `Option B`. |
| 26 | -/ |
| 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 |
Formalization notes
Finiteness of the input alphabet is assumed; the finiteness of the output alphabet, which the book assumes globally, is not needed here and is dropped. The map lifting is , over the alphabets and .
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments