Documentation

Cslib.Computability.Automata.NA.Preimage

Preimage construction on nondeterministic automata #

source
def Cslib.Automata.NA.FinAcc.preimage {State : Type u_1} {Symbol : Type u_2} {Symbol' : Type u_3} (f : Language.Hom Symbol' Symbol) (na : FinAcc State Symbol) :
FinAcc State Symbol'

Given a language homomorphism f from Symbol' to Symbol and an NA na on Symbol, na.preimage f is an NA on Symbol with the same state space, start states, and accept states, but with a different transition relation: the step that na.preimage f takes on input x is the composition of the steps taken by na on inputs f [x].

Equations
Instances For
    source
    @[simp]
    theorem Cslib.Automata.NA.FinAcc.preimage_start {State : Type u_1} {Symbol : Type u_2} {Symbol' : Type u_3} (f : Language.Hom Symbol' Symbol) (na : FinAcc State Symbol) :
    (preimage f na).start = na.start
    source
    @[simp]
    theorem Cslib.Automata.NA.FinAcc.preimage_accept {State : Type u_1} {Symbol : Type u_2} {Symbol' : Type u_3} (f : Language.Hom Symbol' Symbol) (na : FinAcc State Symbol) :
    (preimage f na).accept = na.accept
    source
    @[simp]
    theorem Cslib.Automata.NA.FinAcc.preimage_mTr {State : Type u_1} {Symbol : Type u_2} {Symbol' : Type u_3} (f : Language.Hom Symbol' Symbol) (na : FinAcc State Symbol) {xs' : List Symbol'} {s t : State} :
    (preimage f na).MTr s xs' t ↔ na.MTr s (f xs') t
    source
    @[simp]
    theorem Cslib.Automata.NA.FinAcc.accepts_preimage {State : Type u_1} {Symbol : Type u_2} {Symbol' : Type u_3} (f : Language.Hom Symbol' Symbol) {na : FinAcc State Symbol} {xs' : List Symbol'} :
    Acceptor.Accepts (preimage f na) xs' ↔ Acceptor.Accepts na (f xs')

    na.preimage f accepts a word xs' iff na accepts the word f xs'.

    source
    @[simp]
    theorem Cslib.Automata.NA.FinAcc.preimage_language_eq {State : Type u_1} {Symbol : Type u_2} {Symbol' : Type u_3} (f : Language.Hom Symbol' Symbol) (na : FinAcc State Symbol) :
    Acceptor.language (preimage f na) = Language.preimage (⇑f) (Acceptor.language na)

    na.preimage f accepts the preimage under f of the language accepted by na.