Reduction and shift candidates in canonical item states

Complete valid items give semantic reduction candidates. A valid item whose dot precedes a terminal gives a genuine later handle whenever the remainder of its production can derive a terminal word. The latter proof follows that rightmost derivation to its final step; this is what turns an ordinary shift item into exactly the second handle required by Knuth's semantic LR(k) condition.

theorem CF_grammar.LRk.Valid.reductionCandidate {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {u : Lookahead T k} {i : Item G k} (hi : Valid G k gamma i) (hcomplete : i.Complete) (hlook : i.lookahead = u) : ReductionCandidate G k gamma u (ruleAt G i.rule)

A complete valid item is a semantic reduction candidate.

def CF_grammar.LRk.ShiftItemCandidate {T : Type} (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.nt)) (u : Lookahead T k) (a : T) (i : Item G k) : Prop

Semantic data attached to a shift item. z is the terminal yield of the production suffix after the shifted terminal; consequently a :: z, followed by the item's own lookahead, is the current input lookahead.

Equations

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

theorem CF_grammar.LRk.ShiftItemCandidate.laterHandleCandidate {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {u : Lookahead T k} {a : T} {i : Item G k} (hi : ShiftItemCandidate G k gamma u a i) : LaterHandleCandidate G k gamma u

A semantic shift item supplies a later handle in the precise form consumed by CoreIsLRk.not_reductionCandidate_and_laterHandleCandidate.

def CF_grammar.LRk.StateReduction {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) (u : Lookahead T k) (r : G.augment.nt × List (symbol T G.augment.nt)) : Prop

A reduction exposed by a canonical item state.

Equations

• CF_grammar.LRk.StateReduction G k gamma u r = ∃ i ∈ CF_grammar.LRk.itemState G k gamma, i.Complete ∧ i.lookahead = u ∧ CF_grammar.LRk.ruleAt G.augment i.rule = r

def CF_grammar.LRk.StateShift {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) (u : Lookahead T k) (a : T) : Prop

A terminal shift exposed by a canonical item state, filtered by productive continuation and the complete k-symbol input buffer.

Equations

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

theorem CF_grammar.LRk.StateReduction.reductionCandidate {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.augment.nt)} {u : Lookahead T k} {r : G.augment.nt × List (symbol T G.augment.nt)} (h : StateReduction G k gamma u r) : ReductionCandidate G.augment k gamma u r

theorem CF_grammar.LRk.StateShift.laterHandleCandidate {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.augment.nt)} {u : Lookahead T k} {a : T} (h : StateShift G k gamma u a) : LaterHandleCandidate G.augment k gamma u

theorem CF_grammar.LRk.IsLRk.not_stateReduction_and_stateShift {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} (hLR : G.IsLRk k) {gamma : List (symbol T G.augment.nt)} {u : Lookahead T k} {r : G.augment.nt × List (symbol T G.augment.nt)} (hred : StateReduction G k gamma u r) {a : T} : ¬StateShift G k gamma u a

At a canonical state and fixed lookahead, an LR(k) augmented grammar cannot both reduce and shift.

theorem CF_grammar.LRk.IsLRk.stateReduction_unique {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} (hLR : G.IsLRk k) {gamma : List (symbol T G.augment.nt)} {u : Lookahead T k} {r₁ r₂ : G.augment.nt × List (symbol T G.augment.nt)} (h₁ : StateReduction G k gamma u r₁) (h₂ : StateReduction G k gamma u r₂) : r₁ = r₂

Reductions exposed by a canonical LR(k) state are unique.