Adding a history states to a nondeterministic automaton.

The evolution of the history state can depend on both the original state and the past history state. But the evolution of the original state is not constrained by the history state.

def Cslib.Automata.NA.addHist {Symbol : Type u_1} {State : Type u_2} {Hist : Type u_3} (na : NA State Symbol) (start' : State → Hist) (tr' : State × Hist → Symbol → State → Hist) : NA (State × Hist) Symbol

The construction of adding a history state. Note that start' can depend on the initial value of the original state and tr' can depend on the new value of the original state. So there is no loss of generality in their being functions, rather than relations.

Equations

• na.addHist start' tr' = { Tr := fun (s : State × Hist) (x : Symbol) (t : State × Hist) => na.Tr s.1 x t.1 ∧ tr' s x t.1 = t.2, start := {s : State × Hist | s.1 ∈ na.start ∧ start' s.1 = s.2} }

theorem Cslib.Automata.NA.hist_run_proj {Symbol : Type u_1} {State : Type u_2} {Hist : Type u_3} {na : NA State Symbol} {start' : State → Hist} {tr' : State × Hist → Symbol → State → Hist} {xs : ωSequence Symbol} {ss : ωSequence (State × Hist)} (h_run : (na.addHist start' tr').Run xs ss) : na.Run xs (ωSequence.map Prod.fst ss)

Every run of the history automaton projects onto a run of the original automaton.

def Cslib.Automata.NA.makeHist {Symbol : Type u_1} {State : Type u_2} {Hist : Type u_3} (start' : State → Hist) (tr' : State × Hist → Symbol → State → Hist) (xs : ωSequence Symbol) (ss : ωSequence State) : ℕ → Hist

Given a run of the original automaton, makeHist builds a run of the history state.

Equations

• Cslib.Automata.NA.makeHist start' tr' xs ss 0 = start' (ss 0)
• Cslib.Automata.NA.makeHist start' tr' xs ss n.succ = tr' (ss n, Cslib.Automata.NA.makeHist start' tr' xs ss n) (xs n) (ss (n + 1))

theorem Cslib.Automata.NA.hist_run_exists {Symbol : Type u_1} {State : Type u_2} {Hist : Type u_3} {na : NA State Symbol} {start' : State → Hist} {tr' : State × Hist → Symbol → State → Hist} {xs : ωSequence Symbol} {ss : ωSequence State} (h_run : na.Run xs ss) : ∃ (ss' : ωSequence (State × Hist)), (na.addHist start' tr').Run xs ss' ∧ ωSequence.map Prod.fst ss' = ss

For every run ss of the original automaton, there exists a run ss' of the history automaton which projects back onto ss.