LanglibBounded reachability for Aho's machine #
Logical work-width bounds carried across finite composite-machine runs.
Reachability with an invariant on every intermediate configuration #
The logical work word of a configuration fits in bound squares.
Instances For
def
IndexedGrammar.Aho.BoundedReaches
{T : Type}
(g : IndexedGrammar T)
[Fintype g.nt]
(input : List T)
(bound : ℕ)
(c c' : Config g)
:
Composite reachability whose initial configuration and both endpoints of every traversed edge satisfy the work-tape bound. Consequently every intermediate configuration is bounded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
IndexedGrammar.Aho.BoundedReaches.refl
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{bound : ℕ}
{c : Config g}
(hc : Config.Within bound c)
:
BoundedReaches g input bound c c
theorem
IndexedGrammar.Aho.BoundedReaches.single
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{bound : ℕ}
{c c' : Config g}
(hc : Config.Within bound c)
(hstep : CompositeStep g input c c')
(hc' : Config.Within bound c')
:
BoundedReaches g input bound c c'
theorem
IndexedGrammar.Aho.BoundedReaches.trans
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{bound : ℕ}
{c₁ c₂ c₃ : Config g}
(h₁₂ : BoundedReaches g input bound c₁ c₂)
(h₂₃ : BoundedReaches g input bound c₂ c₃)
:
BoundedReaches g input bound c₁ c₃
theorem
IndexedGrammar.Aho.BoundedReaches.toReflTransGen
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{bound : ℕ}
{c c' : Config g}
(h : BoundedReaches g input bound c c')
:
Relation.ReflTransGen (CompositeStep g input) c c'
Forget the invariant and retain ordinary composite reachability.
theorem
IndexedGrammar.Aho.BoundedReaches.mono
{T : Type}
{g : IndexedGrammar T}
[Fintype g.nt]
{input : List T}
{small large : ℕ}
(hsl : small ≤ large)
{c c' : Config g}
(h : BoundedReaches g input small c c')
:
BoundedReaches g input large c c'
Increase the available work bound.