KOS: Self-Repair via MaxPending (= head of Pending)

@cite{ginzburg-2012} §8.2 (pp. 282–290) "Unifying Self- and Other-Correction"

Per @cite{ginzburg-2012} §6.3 footnote 31 p. 168 and §8.2: MaxPending is the maximal element of dgb.pending, not a separate field. Self-repair operates on the head of Pending directly.

Operations

• TIS.maxPending — accessor: dgb.pending.head?
• TIS.replaceMaxPending — backwards-looking appropriateness repair (Ginzburg §8.2 ex. 31 p. 287 — the canonical repair operation): swap the current head of Pending with a corrected LocProp
• TIS.clearMaxPending — drop the head of Pending (abandon current incomplete utterance)
• TIS.extendMaxPendingPhon — extend the head's phon field (Ginzburg §8.2.3 incremental construction)
• TIS.pushMaxPending — push a new LocProp onto Pending (start a new in-construction utterance; equivalent to DGB.pushPending)

Caveat

TIS.extendMaxPendingPhon and the procedural startRepair/completeRepair sketched in earlier formaliser drafts are not Ginzburg operations per se — he describes (informally) "incrementalising" Pending word-by-word but doesn't enumerate operations. We expose only the replaceMaxPending operation (which corresponds to ex. 31 p. 287's Backwards-looking appropriateness repair) and the LocProp-stack manipulators that any incremental-construction model needs. The §8.2.3 incremental dynamics is deferred substrate work.

def Dialogue.KOS.TIS.maxPending {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) : Option (LocProp Cont)

The current MaxPending: the head of dgb.pending, if any. @cite{ginzburg-2012} §6.3 footnote 31 p. 168.

Equations

• tis.maxPending = tis.dgb.pending.head?

def Dialogue.KOS.TIS.pushMaxPending {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (lp : LocProp Cont) : TIS P Fact QContent Cont

Push a fresh LocProp onto Pending (start a new in-construction utterance, becoming the new MaxPending). Equivalent to DGB.pushPending lifted to TIS.

Equations

• tis.pushMaxPending lp = { dgb := tis.dgb.pushPending lp, priv := tis.priv }

def Dialogue.KOS.TIS.clearMaxPending {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) : TIS P Fact QContent Cont

Drop the current MaxPending (abandon the in-construction or ungrounded LocProp at the head of Pending).

Equations

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

def Dialogue.KOS.TIS.replaceMaxPending {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (replacement : LocProp Cont) : TIS P Fact QContent Cont

Backwards-looking appropriateness repair: replace the current MaxPending with a corrected LocProp.

@cite{ginzburg-2012} ex. 31 (p. 287): the speaker recognises that the current maxpending's content fails appropriateness (wrong word, wrong referent) and updates it to a candidate replacement.

If Pending is empty, this initializes it with the supplied form (lenient default — Ginzburg's rule presupposes a MaxPending to repair).

Equations

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

@[simp]

theorem Dialogue.KOS.pushMaxPending_becomes_max {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (lp : LocProp Cont) : (tis.pushMaxPending lp).maxPending = some lp

pushMaxPending makes the pushed LocProp the new MaxPending.

@[simp]

theorem Dialogue.KOS.clearMaxPending_drops_head {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) : tis.clearMaxPending.dgb.pending = tis.dgb.pending.tail

clearMaxPending removes the head of Pending.

@[simp]

theorem Dialogue.KOS.replaceMaxPending_becomes_max {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (replacement : LocProp Cont) : (tis.replaceMaxPending replacement).maxPending = some replacement

replaceMaxPending makes the replacement the new MaxPending.

@[simp]

theorem Dialogue.KOS.replaceMaxPending_preserves_tail {P : Type u_1} {Fact : Type u_2} {QContent : Type u_3} {Cont : Type} (tis : TIS P Fact QContent Cont) (replacement : LocProp Cont) : (tis.replaceMaxPending replacement).dgb.pending.tail = tis.dgb.pending.tail

replaceMaxPending preserves the rest of Pending (only the head changes).