Lax132576.EpsilonFreeAutomata
Extended transitions and the elimination of ε-transitions
concepts/Lax132576/EpsilonFreeAutomata.lean · lax-132576
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
In the paper
- page 46 of the paper of lax-157538, Transducers
Definition
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.
Lean source view on GitHub
| 1 | import Mathlib.Computability.DFA |
| 2 | import Lax132576.RationalRelations |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Extended transitions and the elimination of ε-transitions |
| 7 | type: definition |
| 8 | --- |
| 9 | Transitions with empty input (-transitions) are essential to |
| 10 | automata with output in two roles: producing an output for the empty input, and |
| 11 | producing infinitely many outputs for one input. Lemma B.2.4 of *Transducers* |
| 12 | shows that, up to these two caveats, they can be eliminated. An automaton with |
| 13 | *extended transitions* carries, instead of an output string, a regular language |
| 14 | of output strings on every transition; the relation it computes takes as |
| 15 | outputs all strings in the concatenation of the languages along an accepting |
| 16 | run. An automaton (with ordinary or extended transitions) is in the |
| 17 | *ε-free normal form* of the lemma if in every accepting run, either the input |
| 18 | is nonempty and each transition reads exactly one letter, or the input is empty |
| 19 | and the run consists of exactly one transition. |
| 20 | |
| 21 | # Formalization notes |
| 22 | |
| 23 | An automaton with extended transitions is a labelled automaton whose labels are |
| 24 | languages over `B`; `IsExtendedNFAO` asks that every label be regular, and |
| 25 | `extRel` is its relation, `v` ranging over the product of the languages of the |
| 26 | run. `EpsilonFree` is the normal form, stated for any labelled automaton so that |
| 27 | both halves of Lemma B.2.4 can use it. |
| 28 | -/ |
| 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 |
Formalization notes
An automaton with extended transitions is a labelled automaton whose labels are languages over ; asks that every label be regular, and is its relation, ranging over the product of the languages of the run. is the normal form, stated for any labelled automaton so that both halves of Lemma B.2.4 can use it.
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