KOS: LocProp Grounding & CRification

@cite{ginzburg-2012} Ch. 6 §6.5–6.7

The Pending → Facts vs Pending → CR-on-QUD branching for utterance integration. When a LocProp enters the Pending field, the addressee either grounds it (cparams instantiable from addressee beliefs → content enters FACTS) or CRifies it (some cparam not instantiable → a clarification request question is pushed onto QUD via a CCUR).

Two integration APIs

This file provides two integration interfaces:

• integrateLocProp — the one-shot stub (legacy): branches purely on whether lp.cparams is empty. Sufficient for the binary grounding/CRification contrast that downstream studies test, but collapses Ginzburg's contextual-instantiation step.
• integrateLocPropCCUR — the multi-stage CCURs pipeline (faithful): Pending Update → Contextual Instantiation → (Grounding | CCUR application). Models the §6.6–6.7 protocol where the addressee's belief base may witness dgb-params even when lp.cparams is non-empty.

Both produce an IntegrationResult. The CCUR variant is the one the Ginzburg2012 §9 grounding-protocol section consumes.

CCURs (Clarification Context Update Rules)

@cite{ginzburg-2012} Ch. 6 footnote 30 p. 167 introduces "CCURs" as the renamed and reformulated successors to the 2004 coercion operations. The book posits TWO canonical CCURs (p. 167; full treatments at ex. 73-79 pp. 192-195 and ex. 80-86 pp. 196-198):

• Parameter Identification (constituent CR — "What is the intended reference of u_i?", ex. 31 p. 167)
• Parameter Focussing (clausal CR — "Was Ariadne asking if JO SREDOVIC left?", p. 167)

A third construct, Repetition CR (Ginzburg §6.8), is included for completeness with the caveat that its CCUR-vs-RequestRepeat status is contested in the book.

Belief Base

The addressee's BeliefBase is modeled as a partial assignment from cparam indices to string witnesses. In a fuller TTR-typed substrate, witnesses would be typed values (records); the string version suffices for paper-replication studies.

Replaces

The 2004 coercion-operations apparatus (parameterFocussing, parameterIdentification, existentialGeneralization) is the predecessor to this protocol; it lives in Phenomena/Ellipsis/Studies/GinzburgCooper2004.lean (paper-anchored, single-consumer demotion).

def Dialogue.KOS.LocProp.isFullyResolved {Cont : Type} (lp : LocProp Cont) : Prop

Whether a LocProp has all contextual parameters resolved. A fully resolved LocProp can be grounded directly.

Equations

• lp.isFullyResolved = (List.length lp.cparams = 0)

@[implicit_reducible]

instance Dialogue.KOS.instDecidableIsFullyResolved {Cont : Type} (lp : LocProp Cont) : Decidable lp.isFullyResolved

Equations

• Dialogue.KOS.instDecidableIsFullyResolved lp = Dialogue.KOS.instDecidableIsFullyResolved._aux_1 lp

inductive Dialogue.KOS.IntegrationResult (Cont : Type) (QContent : Type u_1) : Type u_1

The result of integrating a LocProp into a DGB. Either grounded (content → FACTS) or CRified (CR question → QUD).

• grounded {Cont : Type} {QContent : Type u_1} (content : Cont) : IntegrationResult Cont QContent

  All cparams resolved: content enters FACTS.

• crification {Cont : Type} {QContent : Type u_1} (crQuestion : QContent) (unresolvedParam : CParam) : IntegrationResult Cont QContent

  Some cparam unresolved: CR question pushed onto QUD.

def Dialogue.KOS.instReprIntegrationResult.repr {Cont✝ : Type} {QContent✝ : Type u_1} [Repr Cont✝] [Repr QContent✝] : IntegrationResult Cont✝ QContent✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dialogue.KOS.instReprIntegrationResult {Cont✝ : Type} {QContent✝ : Type u_1} [Repr Cont✝] [Repr QContent✝] : Repr (IntegrationResult Cont✝ QContent✝)

Equations

• Dialogue.KOS.instReprIntegrationResult = { reprPrec := Dialogue.KOS.instReprIntegrationResult.repr }

def Dialogue.KOS.IntegrationResult.isGrounded {Cont : Type} {QContent : Type u_1} : IntegrationResult Cont QContent → Bool

Is this integration result a grounding?

Equations

• (Dialogue.KOS.IntegrationResult.grounded a).isGrounded = true
• (Dialogue.KOS.IntegrationResult.crification a a_1).isGrounded = false

def Dialogue.KOS.integrateLocProp {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (toCR : CParam → QContent) : IntegrationResult Cont QContent

Integrate a LocProp: ground if resolved, CRify otherwise.

The toCR function converts an unresolved parameter to a clarification question — this is domain-specific (e.g., "Who do you mean by 'Bo'?").

Stub caveat: this is a one-shot branching version. Ginzburg's actual integration is a multi-stage pipeline (Pending Update → Contextual Instantiation → CCURs); use integrateLocPropCCUR for the faithful version that consults addressee beliefs.

Equations

• Dialogue.KOS.integrateLocProp lp toCR = match lp.cparams with | [] => Dialogue.KOS.IntegrationResult.grounded lp.cont | p :: tail => Dialogue.KOS.IntegrationResult.crification (toCR p) p

theorem Dialogue.KOS.resolved_always_grounds {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (toCR : CParam → QContent) (h : lp.isFullyResolved) : (integrateLocProp lp toCR).isGrounded = true

A fully resolved LocProp always grounds.

theorem Dialogue.KOS.no_coercion_fallback {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (toCR : CParam → QContent) (p : CParam) (ps : CParamSet) (h : lp.cparams = p :: ps) : (integrateLocProp lp toCR).isGrounded = false

If there are no coercion options and the LocProp has unresolved params, integration produces a CRification — there is no silent fallback.

@[reducible, inline]

abbrev Dialogue.KOS.BeliefBase : Type

The addressee's belief base: a partial assignment from cparam indices to string witnesses.

@cite{ginzburg-2012} eq. 48 (p. 178): contextual instantiation tries to discharge dgb-params by binding each index to a witness from the addressee's beliefs.

Equations

• Dialogue.KOS.BeliefBase = List (String × String)

def Dialogue.KOS.CParam.instantiate (cp : CParam) (beliefs : BeliefBase) : Option String

Try to find a witness for a cparam in the belief base.

Equations

• cp.instantiate beliefs = Option.map (fun (x : String × String) => x.2) (List.find? (fun (x : String × String) => x.1 == cp.index) beliefs)

inductive Dialogue.KOS.ContextualInstantiationResult : Type

The result of contextual instantiation: either every cparam was witnessed, or some remained unresolved.

@cite{ginzburg-2012} eq. 48 (p. 178).

• fullyInstantiated (witnesses : List (String × String)) : ContextualInstantiationResult

  All cparams instantiated; the resolved bindings carry the witnesses.

• partiallyResolved (resolved : List (String × String)) (unresolved : CParamSet) : ContextualInstantiationResult

  Some cparams remain unresolved after consulting beliefs.

@[implicit_reducible]

instance Dialogue.KOS.instReprContextualInstantiationResult : Repr ContextualInstantiationResult

Equations

• Dialogue.KOS.instReprContextualInstantiationResult = { reprPrec := Dialogue.KOS.instReprContextualInstantiationResult.repr }

def Dialogue.KOS.instReprContextualInstantiationResult.repr : ContextualInstantiationResult → ℕ → Std.Format

Equations

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

def Dialogue.KOS.contextualInstantiate {Cont : Type} (lp : LocProp Cont) (beliefs : BeliefBase) : ContextualInstantiationResult

Attempt to instantiate every cparam of a LocProp from a belief base. @cite{ginzburg-2012} eq. 48 (p. 178).

Equations

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

theorem Dialogue.KOS.contextualInstantiate_empty {Cont : Type} (lp : LocProp Cont) (h : lp.cparams = []) (beliefs : BeliefBase) : ∃ (ws : List (String × String)), contextualInstantiate lp beliefs = ContextualInstantiationResult.fullyInstantiated ws

Contextual instantiation on an empty cparam list always fully succeeds.

inductive Dialogue.KOS.CCUR (Cont : Type) (QContent : Type u_1) : Type u_1

The Clarification Context Update Rules of @cite{ginzburg-2012} §6.6 (canonical pair) and §6.8 (debated third).

Each CCUR fires when contextual instantiation fails and produces a specific kind of CR question:

• parameterIdentification (Ginzburg ex. 31 p. 167, §6.6 ex. 73-79 pp. 192-195): target one unresolved cparam, ask "What is the intended reference of u_i?" — the constituent CR
• parameterFocussing (Ginzburg p. 167, §6.6 ex. 80-86 pp. 196-198): abstract over the target's content while instantiating all other parameters, ask a confirmation question about the antecedent proposition — the clausal CR
• repetitionCR (Ginzburg §6.8): a debated CCUR-analog handling phonetic repetition requests; included for completeness

These replace the three coercion operations of @cite{ginzburg-cooper-2004} (parameterFocussing, parameterIdentification, existentialGeneralization), which now live as paper-specific apparatus in Phenomena/Ellipsis/Studies/GinzburgCooper2004.lean §0. The 2004→2012 correspondence: parameterFocussing (2004) ↔ parameterFocussing (2012); parameterIdentification (both); existentialGeneralization (2004) has no 2012 CCUR analog (the 2012 framework handles it via contextual instantiation succeeding without a CR being needed).

• parameterIdentification {Cont : Type} {QContent : Type u_1} (paramIdx : String) (crQuestion : QContent) : CCUR Cont QContent

  Parameter Identification (Ginzburg ex. 31 p. 167): target one unresolved cparam, ask "What is the intended reference of u_i?" (constituent CR).

• parameterFocussing {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (crQuestion : QContent) : CCUR Cont QContent

  Parameter Focussing (Ginzburg p. 167): abstract over the target's content while instantiating all other parameters, ask a confirmation question (clausal CR — polar confirmation).

• repetitionCR {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (crQuestion : QContent) : CCUR Cont QContent

  Repetition CR (Ginzburg §6.8): a debated CCUR-analog for phonetic repetition requests ("Pardon?").

@[implicit_reducible]

instance Dialogue.KOS.instReprCCUR {Cont✝ : Type} {QContent✝ : Type u_1} [Repr Cont✝] [Repr QContent✝] : Repr (CCUR Cont✝ QContent✝)

Equations

• Dialogue.KOS.instReprCCUR = { reprPrec := Dialogue.KOS.instReprCCUR.repr }

def Dialogue.KOS.instReprCCUR.repr {Cont✝ : Type} {QContent✝ : Type u_1} [Repr Cont✝] [Repr QContent✝] : CCUR Cont✝ QContent✝ → ℕ → Std.Format

Equations

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

def Dialogue.KOS.CCUR.crQuestion {Cont : Type} {QContent : Type u_1} : CCUR Cont QContent → QContent

Project a CCUR back to its CR question content.

Equations

• (Dialogue.KOS.CCUR.parameterIdentification a a_1).crQuestion = a_1
• (Dialogue.KOS.CCUR.parameterFocussing a a_1).crQuestion = a_1
• (Dialogue.KOS.CCUR.repetitionCR a a_1).crQuestion = a_1

def Dialogue.KOS.integrateLocPropCCUR {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (beliefs : BeliefBase) (toCR : CParam → QContent) : IntegrationResult Cont QContent

The faithful @cite{ginzburg-2012} §6.6 integration pipeline.

Stages:

1. The LocProp lp enters Pending (caller's responsibility).
2. Contextual Instantiation (Ginzburg §6.5): consult addressee beliefs to instantiate cparams.
3. Branching:
   • If fully instantiated → grounding (content enters FACTS)
   • If partial → apply a CCUR: this implementation defaults to Parameter Identification on the first unresolved cparam (the most common case per Ginzburg's worked examples in §6.6, and the form instantiated by the running "Did Jo leave?"/"Jo?" example, ex. 31 p. 167). Choice between parameterIdentification and parameterFocussing depends on whether the target is a sub-utterance (former) or the whole utterance (latter).

The toCR function constructs the CR question for an unresolved param.

This replaces integrateLocProp for substrate uses requiring the contextual-instantiation step.

Equations

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

theorem Dialogue.KOS.resolved_grounds_via_ccur {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (beliefs : BeliefBase) (toCR : CParam → QContent) (h : lp.isFullyResolved) : (integrateLocPropCCUR lp beliefs toCR).isGrounded = true

A fully-resolved LocProp grounds via the CCUR pipeline regardless of beliefs (since contextual instantiation trivially succeeds with empty cparams).

theorem Dialogue.KOS.belief_resolution_grounds_via_ccur {Cont : Type} {QContent : Type u_1} (lp : LocProp Cont) (beliefs : BeliefBase) (toCR : CParam → QContent) (h : ∀ cp ∈ lp.cparams, (cp.instantiate beliefs).isSome = true) : (integrateLocPropCCUR lp beliefs toCR).isGrounded = true

A LocProp with cparams but full belief coverage grounds via the CCUR pipeline. This is the substantive difference from the one-shot stub: unresolved cparams aren't an automatic CRification trigger when addressee beliefs witness them.