Totalizer Annotated Stack

This file defines the finite stack annotations and regular lookahead queries used by the DPDA totalizer once a RegularEpsilonAnalysis has been built.

structure DPDA.AnalysisSummary {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : Type

The vector of DFA transition summaries stored for the stack suffix below a symbol.

• stop (q : Q) : A.StopState q → A.StopState q
• accept (q : Q) : A.AcceptState q → A.AcceptState q

def DPDA.AnalysisSummary.equivProd {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : AnalysisSummary A ≃ ((q : Q) → A.StopState q → A.StopState q) × ((q : Q) → A.AcceptState q → A.AcceptState q)

AnalysisSummary is just a pair of finite dependent function spaces.

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance DPDA.instFintypeAnalysisSummary {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : Fintype (AnalysisSummary A)

Equations

• DPDA.instFintypeAnalysisSummary A = Fintype.ofEquiv (((q : Q) → A.StopState q → A.StopState q) × ((q : Q) → A.AcceptState q → A.AcceptState q)) (DPDA.AnalysisSummary.equivProd A).symm

def DPDA.AnalysisSummary.id {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : AnalysisSummary A

The empty-suffix summary vector.

Equations

• DPDA.AnalysisSummary.id A = { stop := fun (x : Q) (x_1 : A.StopState x) => x_1, accept := fun (x : Q) (x_1 : A.AcceptState x) => x_1 }

def DPDA.SummaryRepresents {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (summary : AnalysisSummary A) (γ : List S) : Prop

A summary vector represents an original stack suffix when every component is the DFA transition function induced by reading that suffix.

Equations

• DPDA.SummaryRepresents A summary γ = ((∀ (q : Q), summary.stop q = (A.stopDFA q).stackSummary γ) ∧ ∀ (q : Q), summary.accept q = (A.acceptDFA q).stackSummary γ)

theorem DPDA.SummaryRepresents.eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {summary₁ summary₂ : AnalysisSummary A} {γ : List S} (h₁ : SummaryRepresents A summary₁ γ) (h₂ : SummaryRepresents A summary₂ γ) : summary₁ = summary₂

theorem DPDA.summaryRepresents_id {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : SummaryRepresents A (AnalysisSummary.id A) []

The identity summary represents the empty stack suffix.

def DPDA.AnalysisSummary.above {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (below : AnalysisSummary A) (γ : List S) : AnalysisSummary A

Update a summary vector by placing a block of original stack symbols above it.

Equations

• DPDA.AnalysisSummary.above A below γ = { stop := fun (q : Q) => (A.stopDFA q).summaryAbove (below.stop q) γ, accept := fun (q : Q) => (A.acceptDFA q).summaryAbove (below.accept q) γ }

theorem DPDA.SummaryRepresents.above {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {below : AnalysisSummary A} {δ : List S} (hbelow : SummaryRepresents A below δ) (γ : List S) : SummaryRepresents A (AnalysisSummary.above A below γ) (γ ++ δ)

Updating a correct summary with a block keeps it correct for the larger suffix.

theorem DPDA.SummaryRepresents.cons {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {below : AnalysisSummary A} {γ : List S} (hbelow : SummaryRepresents A below γ) (Z : S) : SummaryRepresents A (AnalysisSummary.above A below [Z]) (Z :: γ)

Placing one top symbol above a represented suffix gives a represented full stack.

@[reducible, inline]

abbrev DPDA.TotalStackSymbol {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : Type

Stack symbols of the totalized machine. none is the permanent bottom marker; some (Z, s) is an original stack symbol annotated with the summary vector of the original stack suffix below it.

Equations

• DPDA.TotalStackSymbol A = Option (S × DPDA.AnalysisSummary A)

def DPDA.annotateAbove {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (below : AnalysisSummary A) : List S → List (TotalStackSymbol A)

Annotate a replacement block above an already summarized suffix.

Equations

• DPDA.annotateAbove A below [] = []
• DPDA.annotateAbove A below (Z :: γ) = some (Z, DPDA.AnalysisSummary.above A below γ) :: DPDA.annotateAbove A below γ

@[simp]

theorem DPDA.annotateAbove_nil {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (below : AnalysisSummary A) : annotateAbove A below [] = []

@[simp]

theorem DPDA.annotateAbove_cons {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (below : AnalysisSummary A) (Z : S) (γ : List S) : annotateAbove A below (Z :: γ) = some (Z, AnalysisSummary.above A below γ) :: annotateAbove A below γ

def DPDA.eraseAnnotatedStack {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : List (TotalStackSymbol A) → List S

Erase annotations from a totalized stack, dropping the bottom marker.

Equations

• DPDA.eraseAnnotatedStack A [] = []
• DPDA.eraseAnnotatedStack A (none :: γ) = DPDA.eraseAnnotatedStack A γ
• DPDA.eraseAnnotatedStack A (some (Z, snd) :: γ) = Z :: DPDA.eraseAnnotatedStack A γ

theorem DPDA.erase_annotateAbove {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (below : AnalysisSummary A) (γ : List S) : eraseAnnotatedStack A (annotateAbove A below γ) = γ

theorem DPDA.eraseAnnotatedStack_append {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (γ δ : List (TotalStackSymbol A)) : eraseAnnotatedStack A (γ ++ δ) = eraseAnnotatedStack A γ ++ eraseAnnotatedStack A δ

def DPDA.StackWellAnnotated {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : List (TotalStackSymbol A) → Prop

The annotation invariant for totalizer stacks. Every original stack symbol stores a summary for the erased suffix below it; none is the unique bottom marker.

Equations

• DPDA.StackWellAnnotated A [] = True
• DPDA.StackWellAnnotated A (none :: γ) = (γ = [])
• DPDA.StackWellAnnotated A (some (Z, snd) :: γ) = (DPDA.SummaryRepresents A snd (DPDA.eraseAnnotatedStack A γ) ∧ DPDA.StackWellAnnotated A γ)

theorem DPDA.stackWellAnnotated_nil {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : StackWellAnnotated A []

theorem DPDA.stackWellAnnotated_none {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : StackWellAnnotated A [none]

theorem DPDA.stackWellAnnotated_cons_some_iff {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (Z : S) (below : AnalysisSummary A) (rest : List (TotalStackSymbol A)) : StackWellAnnotated A (some (Z, below) :: rest) ↔ SummaryRepresents A below (eraseAnnotatedStack A rest) ∧ StackWellAnnotated A rest

theorem DPDA.stackWellAnnotated_annotateAbove_append {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {below : AnalysisSummary A} {rest : List (TotalStackSymbol A)} (hbelow : SummaryRepresents A below (eraseAnnotatedStack A rest)) (hrest : StackWellAnnotated A rest) (γ : List S) : StackWellAnnotated A (annotateAbove A below γ ++ rest)

theorem DPDA.stackWellAnnotated_annotateAbove_bottom {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (γ : List S) : StackWellAnnotated A (annotateAbove A (AnalysisSummary.id A) γ ++ [none])

def DPDA.StackHasBottom {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : List (TotalStackSymbol A) → Prop

Reachable totalizer stacks retain a permanent bottom marker.

Equations

• DPDA.StackHasBottom A [] = False
• DPDA.StackHasBottom A (none :: rest) = (rest = [])
• DPDA.StackHasBottom A (some val :: rest) = DPDA.StackHasBottom A rest

theorem DPDA.stackHasBottom_none {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : StackHasBottom A [none]

theorem DPDA.stackHasBottom_nonempty {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {stack : List (TotalStackSymbol A)} (hstack : StackHasBottom A stack) : ∃ (top : TotalStackSymbol A) (rest : List (TotalStackSymbol A)), stack = top :: rest

theorem DPDA.stackHasBottom_annotateAbove_append {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {below : AnalysisSummary A} {rest : List (TotalStackSymbol A)} (hrest : StackHasBottom A rest) (γ : List S) : StackHasBottom A (annotateAbove A below γ ++ rest)

theorem DPDA.stackHasBottom_annotateAbove_bottom {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (γ : List S) : StackHasBottom A (annotateAbove A (AnalysisSummary.id A) γ ++ [none])

def DPDA.topStops {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) : TotalStackSymbol A → Prop

Does the semantic epsilon phase terminate from the configuration represented by the current top stack symbol?

Equations

• DPDA.topStops A q none = ((A.stopDFA q).evalFrom (A.stopDFA q).start [] ∈ (A.stopDFA q).accept)
• DPDA.topStops A q (some (Z, below)) = (below.stop q ((A.stopDFA q).step (A.stopDFA q).start Z) ∈ (A.stopDFA q).accept)

def DPDA.topAcceptsEpsilonClosure {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) : TotalStackSymbol A → Prop

If the input is exhausted at the configuration represented by the current top stack symbol, does the original machine accept along its epsilon closure?

Equations

• DPDA.topAcceptsEpsilonClosure A q none = ((A.acceptDFA q).evalFrom (A.acceptDFA q).start [] ∈ (A.acceptDFA q).accept)
• DPDA.topAcceptsEpsilonClosure A q (some (Z, below)) = (below.accept q ((A.acceptDFA q).step (A.acceptDFA q).start Z) ∈ (A.acceptDFA q).accept)

theorem DPDA.topStops_some_correct {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (Z : S) (below : AnalysisSummary A) : topStops A q (some (Z, below)) ↔ below.stop q ((A.stopDFA q).step (A.stopDFA q).start Z) ∈ (A.stopDFA q).accept

theorem DPDA.topAccepts_some_correct {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (Z : S) (below : AnalysisSummary A) : topAcceptsEpsilonClosure A q (some (Z, below)) ↔ below.accept q ((A.acceptDFA q).step (A.acceptDFA q).start Z) ∈ (A.acceptDFA q).accept

def DPDA.fullSummaryOfTop {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : TotalStackSymbol A → AnalysisSummary A

The full original-stack summary represented by the current top symbol.

Equations

• DPDA.fullSummaryOfTop A none = DPDA.AnalysisSummary.id A
• DPDA.fullSummaryOfTop A (some (Z, below)) = DPDA.AnalysisSummary.above A below [Z]

theorem DPDA.stackWellAnnotated_fullSummaryOfTop {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {top : TotalStackSymbol A} {rest : List (TotalStackSymbol A)} (hstack : StackWellAnnotated A (top :: rest)) : SummaryRepresents A (fullSummaryOfTop A top) (eraseAnnotatedStack A (top :: rest))

def DPDA.stopsFromSummary {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (summary : AnalysisSummary A) : Prop

The stop lookahead evaluated from a full-stack summary.

Equations

• DPDA.stopsFromSummary A q summary = (summary.stop q (A.stopDFA q).start ∈ (A.stopDFA q).accept)

def DPDA.acceptsFromSummary {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (summary : AnalysisSummary A) : Prop

The epsilon-acceptance lookahead evaluated from a full-stack summary.

Equations

• DPDA.acceptsFromSummary A q summary = (summary.accept q (A.acceptDFA q).start ∈ (A.acceptDFA q).accept)

theorem DPDA.stopsFromSummary_correct {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {summary : AnalysisSummary A} {γ : List S} (hsummary : SummaryRepresents A summary γ) (q : Q) : stopsFromSummary A q summary ↔ ∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt (q, γ) c'

Stop-lookahead correctness for a summary representing the current original stack.

theorem DPDA.acceptsFromSummary_correct {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {summary : AnalysisSummary A} {γ : List S} (hsummary : SummaryRepresents A summary γ) (q : Q) : acceptsFromSummary A q summary ↔ ∃ (q' : Q) (γ' : List S), M.EpsilonReaches (q, γ) (q', γ') ∧ q' ∈ M.final_states

Epsilon-acceptance lookahead correctness for a summary representing the current original stack.

def DPDA.acceptBit {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (summary : AnalysisSummary A) : Bool

Boolean form of acceptsFromSummary, used in the finite control.

Equations

• DPDA.acceptBit A q summary = if DPDA.acceptsFromSummary A q summary then true else false

theorem DPDA.acceptBit_eq_true_iff {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (summary : AnalysisSummary A) : acceptBit A q summary = true ↔ acceptsFromSummary A q summary

theorem DPDA.acceptBit_eq_false_iff {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (summary : AnalysisSummary A) : acceptBit A q summary = false ↔ ¬acceptsFromSummary A q summary

theorem DPDA.topStops_eq_stopsFromSummary {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (top : TotalStackSymbol A) : topStops A q top ↔ stopsFromSummary A q (fullSummaryOfTop A top)

theorem DPDA.topAccepts_eq_acceptsFromSummary {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) (top : TotalStackSymbol A) : topAcceptsEpsilonClosure A q top ↔ acceptsFromSummary A q (fullSummaryOfTop A top)

theorem DPDA.topStops_semantic_of_stackWellAnnotated {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {top : TotalStackSymbol A} {rest : List (TotalStackSymbol A)} (hstack : StackWellAnnotated A (top :: rest)) (q : Q) : topStops A q top ↔ ∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt (q, eraseAnnotatedStack A (top :: rest)) c'

theorem DPDA.topAccepts_semantic_of_stackWellAnnotated {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {top : TotalStackSymbol A} {rest : List (TotalStackSymbol A)} (hstack : StackWellAnnotated A (top :: rest)) (q : Q) : topAcceptsEpsilonClosure A q top ↔ ∃ (q' : Q) (γ' : List S), M.EpsilonReaches (q, eraseAnnotatedStack A (top :: rest)) (q', γ') ∧ q' ∈ M.final_states

theorem DPDA.topStops_none_correct {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) : topStops A q none ↔ ∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt (q, []) c'

theorem DPDA.topAccepts_none_correct {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) (q : Q) : topAcceptsEpsilonClosure A q none ↔ ∃ (q' : Q) (γ' : List S), M.EpsilonReaches (q, []) (q', γ') ∧ q' ∈ M.final_states

theorem DPDA.topStops_some_semantic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {below : AnalysisSummary A} {γ : List S} (hbelow : SummaryRepresents A below γ) (q : Q) (Z : S) : topStops A q (some (Z, below)) ↔ ∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt (q, Z :: γ) c'

theorem DPDA.topAccepts_some_semantic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) {below : AnalysisSummary A} {γ : List S} (hbelow : SummaryRepresents A below γ) (q : Q) (Z : S) : topAcceptsEpsilonClosure A q (some (Z, below)) ↔ ∃ (q' : Q) (γ' : List S), M.EpsilonReaches (q, Z :: γ) (q', γ') ∧ q' ∈ M.final_states