Lax132576.SubsequentialTransducers
Subsequential transducers
concepts/Lax132576/SubsequentialTransducers.lean · lax-132576
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
In the paper
- page 71 of the paper of lax-157538, Transducers
Definition
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.
Lean source view on GitHub
| 1 | import Lax765601.StateTransformations |
| 2 | import Lax132576.SequentialTransducers |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Subsequential transducers |
| 7 | type: definition |
| 8 | --- |
| 9 | A *subsequential transducer* (Section B.4.3 of *Transducers*) is a sequential |
| 10 | transducer equipped with a partial *end-of-input* function, which is applied to |
| 11 | the state reached after the whole input has been read: its value, if defined, |
| 12 | is appended to the output, and if it is undefined the transducer has no output. |
| 13 | Subsequential transducers therefore compute *partial* functions; they can, for |
| 14 | instance, append a letter to their input, which a sequential transducer cannot, |
| 15 | and a function that is undefined on some inputs can be computed. Theorem B.4.8 |
| 16 | characterises the subsequential functions. |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | A partial function is a function into `Option (List B)`. The end-of-input |
| 21 | function is `Q → Option (List B)`; the semantics is the output of the |
| 22 | sequential part followed by the end-of-input value at the state reached, when |
| 23 | that value is defined. `IsSubsequential f` asks for a finite state space. |
| 24 | -/ |
| 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 |
Formalization notes
A partial function is a function into . The end-of-input function is ; the semantics is the output of the sequential part followed by the end-of-input value at the state reached, when that value is defined. asks for a finite state space.
From Mathlib
none
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