Uniform Membership Check for Encoded Context-Free Grammars

Saturation Algorithm Definitions

def matchRHS {T : Type} [DecidableEq T] (w : List T) (nc : ℕ) (S : List (ℕ × ℕ × ℕ)) (rhs : List (ℕ ⊕ T)) (startPos : ℕ) : List ℕ

Match a rule's RHS against a substring of word w, starting from position startPos. Returns all possible end positions after matching the full RHS.

Equations

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

def satStep {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) : List (ℕ × ℕ × ℕ)

One step of the saturation.

Equations

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

def satFixpoint {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (steps : ℕ) : List (ℕ × ℕ × ℕ)

Iterate the saturation step.

Equations

• satFixpoint nc rules w steps = (satStep nc rules w)^[steps] []

def checkMembershipEncoded {T : Type} [DecidableEq T] [Fintype T] (p : EncodedCFG T × List T) : Bool

Check membership of word w in the language of encoded CFG G.

Equations

• checkMembershipEncoded p = decide ((p.1.initialIdx % p.1.ntCount, 0, p.2.length) ∈ satFixpoint p.1.ntCount p.1.rawRules p.2 (p.1.ntCount * (p.2.length + 1) * (p.2.length + 1) + 1))

Monotonicity

theorem satStep_mono {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) (t : ℕ × ℕ × ℕ) : t ∈ S → t ∈ satStep nc rules w S

theorem satFixpoint_mono {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (n m : ℕ) (h : n ≤ m) (t : ℕ × ℕ × ℕ) : t ∈ satFixpoint nc rules w n → t ∈ satFixpoint nc rules w m

Soundness Lemmas

def TripleDerives {T : Type} (G : EncodedCFG T) (w : List T) (nt i j : ℕ) : Prop

Property that a triple represents a valid derivation.

Equations

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

def AllSound {T : Type} (G : EncodedCFG T) (w : List T) (S : List (ℕ × ℕ × ℕ)) : Prop

Property that all triples in a set represent valid derivations.

Equations

• AllSound G w S = ∀ (nt i j : ℕ), (nt, i, j) ∈ S → TripleDerives G w nt i j

theorem matchRHS_sound {T : Type} [DecidableEq T] (G : EncodedCFG T) (w : List T) (S : List (ℕ × ℕ × ℕ)) (hS : AllSound G w S) (rhs : List (ℕ ⊕ T)) (startPos endPos : ℕ) (hstart : startPos ≤ w.length) (hmatch : endPos ∈ matchRHS w G.ntCount S rhs startPos) : startPos ≤ endPos ∧ endPos ≤ w.length ∧ CF_derives G.toCFGrammar (List.map G.toSymbol rhs) (List.map symbol.terminal (List.take (endPos - startPos) (List.drop startPos w)))

theorem mem_satStep_iff {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) (nt i j : ℕ) : (nt, i, j) ∈ satStep nc rules w S → (nt, i, j) ∈ S ∨ ∃ rule ∈ rules, ∃ startPos ≤ w.length, nt = rule.1 % nc ∧ i = startPos ∧ j ∈ matchRHS w nc S rule.2 startPos

theorem satStep_sound {T : Type} [DecidableEq T] (G : EncodedCFG T) (w : List T) (S : List (ℕ × ℕ × ℕ)) (hS : AllSound G w S) : AllSound G w (satStep G.ntCount G.rawRules w S)

theorem satFixpoint_sound {T : Type} [DecidableEq T] (G : EncodedCFG T) (w : List T) (steps : ℕ) : AllSound G w (satFixpoint G.ntCount G.rawRules w steps)

matchRHS structural lemmas

def matchOneSym {T : Type} [DecidableEq T] (w : List T) (nc : ℕ) (S : List (ℕ × ℕ × ℕ)) (sym : ℕ ⊕ T) (pos : ℕ) : List ℕ

The single-symbol matching step.

Equations

• One or more equations did not get rendered due to their size.
• matchOneSym w nc S (Sum.inr t) pos = match w[pos]? with | some c => if (c == t) = true then [pos + 1] else [] | none => []

theorem matchRHS_foldl_append {T : Type} [DecidableEq T] (w : List T) (nc : ℕ) (S : List (ℕ × ℕ × ℕ)) (rhs : List (ℕ ⊕ T)) (p1 p2 : List ℕ) : List.foldl (fun (positions : List ℕ) (sym : ℕ ⊕ T) => List.flatMap (matchOneSym w nc S sym) positions) (p1 ++ p2) rhs = List.foldl (fun (positions : List ℕ) (sym : ℕ ⊕ T) => List.flatMap (matchOneSym w nc S sym) positions) p1 rhs ++ List.foldl (fun (positions : List ℕ) (sym : ℕ ⊕ T) => List.flatMap (matchOneSym w nc S sym) positions) p2 rhs

theorem matchRHS_cons {T : Type} [DecidableEq T] (w : List T) (nc : ℕ) (S : List (ℕ × ℕ × ℕ)) (sym : ℕ ⊕ T) (rest : List (ℕ ⊕ T)) (startPos : ℕ) : matchRHS w nc S (sym :: rest) startPos = List.flatMap (matchRHS w nc S rest) (matchOneSym w nc S sym startPos)

Completeness Lemmas

theorem mem_satStep_of_matchRHS {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) (lhs : ℕ) (rhs : List (ℕ ⊕ T)) (hrule : (lhs, rhs) ∈ rules) (startPos endPos : ℕ) (hstart : startPos ≤ w.length) (hmatch : endPos ∈ matchRHS w nc S rhs startPos) : (lhs % nc, startPos, endPos) ∈ satStep nc rules w S

Monotonicity of matchRHS in S

theorem matchRHS_mono {T : Type} [DecidableEq T] (w : List T) (nc : ℕ) (S₁ S₂ : List (ℕ × ℕ × ℕ)) (hS : ∀ t ∈ S₁, t ∈ S₂) (rhs : List (ℕ ⊕ T)) (startPos e : ℕ) : e ∈ matchRHS w nc S₁ rhs startPos → e ∈ matchRHS w nc S₂ rhs startPos

Additional splitting lemmas

theorem terminal_derives_in_self {T : Type} (g : CF_grammar T) (t : T) (n : ℕ) (w : List T) (h : CF_derives_in g n [symbol.terminal t] (List.map symbol.terminal w)) : n = 0 ∧ w = [t]

theorem no_terminal_eq_nonterminal {T : Type} (g : CF_grammar T) (nt : g.nt) (w' : List T) : [symbol.nonterminal nt] ≠ List.map symbol.terminal w'

theorem transforms_single_nonterminal {T : Type} (g : CF_grammar T) (nt : g.nt) (mid : List (symbol T g.nt)) (h : CF_transforms g [symbol.nonterminal nt] mid) : ∃ (rhs : List (symbol T g.nt)), (nt, rhs) ∈ g.rules ∧ mid = rhs

theorem rawRule_of_toCFGrammar_rule {T : Type} (G : EncodedCFG T) (nt : Fin G.ntCount) (rhs : List (symbol T (Fin G.ntCount))) (hrule : (nt, rhs) ∈ G.toCFGrammar.rules) : ∃ (lhs_raw : ℕ) (rhs_raw : List (ℕ ⊕ T)), (lhs_raw, rhs_raw) ∈ G.rawRules ∧ G.toNT lhs_raw = nt ∧ rhs = List.map G.toSymbol rhs_raw

theorem matchRHS_in_satFixpoint {T : Type} [DecidableEq T] (G : EncodedCFG T) (w : List T) (n : ℕ) (ih_outer : ∀ m < n + 1, ∀ (nt : Fin G.ntCount) (i j : ℕ), i ≤ j → j ≤ w.length → CF_derives_in G.toCFGrammar m [symbol.nonterminal nt] (List.map symbol.terminal (List.take (j - i) (List.drop i w))) → ∃ (bound : ℕ), (↑nt, i, j) ∈ satFixpoint G.ntCount G.rawRules w bound) (rhs : List (ℕ ⊕ T)) (startPos endPos : ℕ) (hstart : startPos ≤ endPos) (hend : endPos ≤ w.length) (nder : ℕ) (hnder : nder ≤ n) (hder : CF_derives_in G.toCFGrammar nder (List.map G.toSymbol rhs) (List.map symbol.terminal (List.take (endPos - startPos) (List.drop startPos w)))) : ∃ (bound : ℕ), endPos ∈ matchRHS w G.ntCount (satFixpoint G.ntCount G.rawRules w bound) rhs startPos

theorem satFixpoint_complete {T : Type} [DecidableEq T] (G : EncodedCFG T) (w : List T) (nt : Fin G.ntCount) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ w.length) (hder : CF_derives G.toCFGrammar [symbol.nonterminal nt] (List.map symbol.terminal (List.take (j - i) (List.drop i w)))) : ∃ (bound : ℕ), (↑nt, i, j) ∈ satFixpoint G.ntCount G.rawRules w bound

Saturation Stabilization

theorem satStep_prefix {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) : S <+: satStep nc rules w S

theorem satStep_fst_bound {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) (nt i j : ℕ) (hnc : 0 < nc) (hS : ∀ (nt' i' j' : ℕ), (nt', i', j') ∈ S → nt' < nc) (h : (nt, i, j) ∈ satStep nc rules w S) : nt < nc

theorem matchRHS_endPos_bound {T : Type} [DecidableEq T] (w : List T) (nc : ℕ) (S : List (ℕ × ℕ × ℕ)) (hS : ∀ (nt i j : ℕ), (nt, i, j) ∈ S → j ≤ w.length) (rhs : List (ℕ ⊕ T)) (startPos endPos : ℕ) (hstart : startPos ≤ w.length) (hmatch : endPos ∈ matchRHS w nc S rhs startPos) : endPos ≤ w.length

theorem satStep_pos_bound {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) (hS : ∀ (nt i j : ℕ), (nt, i, j) ∈ S → i ≤ w.length ∧ j ≤ w.length) (nt i j : ℕ) (h : (nt, i, j) ∈ satStep nc rules w S) : i ≤ w.length ∧ j ≤ w.length

theorem satStep_nodup {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (S : List (ℕ × ℕ × ℕ)) (hS : S.Nodup) : (satStep nc rules w S).Nodup

theorem satFixpoint_nodup {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (n : ℕ) : (satFixpoint nc rules w n).Nodup

theorem satFixpoint_entries_bounded {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (hnc : 0 < nc) (n nt i j : ℕ) (h : (nt, i, j) ∈ satFixpoint nc rules w n) : nt < nc ∧ i ≤ w.length ∧ j ≤ w.length

theorem satFixpoint_length_bounded {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (hnc : 0 < nc) (n : ℕ) : (satFixpoint nc rules w n).length ≤ nc * (w.length + 1) * (w.length + 1)

theorem satFixpoint_stable_after {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (k : ℕ) (hk : satFixpoint nc rules w k = satFixpoint nc rules w (k + 1)) (m : ℕ) : m ≥ k → satFixpoint nc rules w m = satFixpoint nc rules w k

theorem satFixpoint_converges {T : Type} [DecidableEq T] (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (w : List T) (hnc : 0 < nc) (t : ℕ × ℕ × ℕ) : (∃ (n : ℕ), t ∈ satFixpoint nc rules w n) → t ∈ satFixpoint nc rules w (nc * (w.length + 1) * (w.length + 1) + 1)

Main Correctness

theorem checkMembershipEncoded_correct {T : Type} [DecidableEq T] [Fintype T] (G : EncodedCFG T) (w : List T) : checkMembershipEncoded (G, w) = true ↔ w ∈ CF_language G.toCFGrammar