Documentation

Linglib.Theories.Semantics.Dynamic.PPCDRT.Anaphora

PPCDRT — Anaphoric Relations and Maximize Anaphora #

@cite{haug-dalrymple-2020} @cite{dotlacil-2013} @cite{murray-2008} @cite{langendoen-1978}

The anaphoric-relation conditions on top of the PPCDRT substrate, plus the R_u set construction and the Maximize Anaphora principle.

Three relations distinguished by @cite{higginbotham-1985}, @cite{williams-1991} and formalized in @cite{haug-dalrymple-2020}:

The reciprocity-as-cumulativity link asserted by @cite{langendoen-1978} shows up as a structural theorem in Cumulativity.lean: groupIdentityCond is the bidirectional-coverage shape that Plurality.Cumulativity.cumulativeOp expresses for plural arguments.

§6 of @cite{haug-dalrymple-2020} adds the Maximize Anaphora principle (eq 128): when interpreting a discourse referent introduced by a reciprocal with antecedent and relation φ, maximize the set R_u of pairs in the relation, subject to consistency with world knowledge. The substrate-level statement is given here; the §6.1/§6.2/§6.3 applications (the SMH contrast, the multi-reciprocal pairwise prediction, the Tracy/Matty/Chris case) live in Phenomena/Anaphora/Studies/HaugDalrymple2020.lean.

source
def Theories.Semantics.Dynamic.PPCDRT.bindingCond {E : Type u} (uAnaph uAnt : ℕ) :
PPDRSCond E

Binding (u_anaph = u_ant): pointwise dref equality across the plural state. The two drefs hold the same Option E value at every state — either both defined and equal, or both undefined.

Per @cite{haug-dalrymple-2020} eq 30: u_anaph = u_ant ≡ ∀ s ∈ S. v(s)(u_anaph) = v(s)(u_ant). The pointwise Option equality matches this — both drefs hold the same value (defined or undefined) at every state. Stronger than the coreference presupposition (the eq-29 → abbreviation), which only requires defined-and-equal where both are defined.

Equations
Instances For
    source
    def Theories.Semantics.Dynamic.PPCDRT.coverCond {E : Type u} (uAnaph uAnt : ℕ) :
    PPDRSCond E

    One-direction sum-dref coverage: every value uAnaph takes across the plural state is also a value uAnt takes.

    Note: this is NOT @cite{haug-dalrymple-2020} eq 29 (the asymmetric →). Paper eq 29 is λS.λΔ.∀s ∈ S. u_anaph(s,[s]_Δ) = u_ant(s,S) — an equation between two evaluations, not a subset relation. At Δ = ∅ paper eq 29 reduces to pointwise bindingCond, not to coverCond. The closer paper match is the SUM-dref equality of eq 37 (p. 16), but eq 37 is also bidirectional.

    coverCond is a derived auxiliary used solely by the bidirectional bridge groupIdentityCond_iff_bidir_coverCond below — it spells out one direction of the value-set equality so consumers can reason about it directly. It is not itself paper-stipulated.

    Equations
    Instances For
      source
      def Theories.Semantics.Dynamic.PPCDRT.groupIdentityCond {E : Type u} (uAnaph uAnt : ℕ) :
      PPDRSCond E

      Group identity (∪u_anaph = ∪u_ant): the value-sets of the two drefs across the plural state are equal.

      @cite{haug-dalrymple-2020} eq 41 stipulates ∂(∪u = ∪𝒜(u)) for each other — exactly this symmetric equality on sum-drefs. Bidirectional coverCond is an alternative formulation provable via groupIdentityCond_iff_bidir_coverCond below.

      Equations
      Instances For
        source
        theorem Theories.Semantics.Dynamic.PPCDRT.groupIdentityCond_iff_bidir_coverCond {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) :
        groupIdentityCond uAnaph uAnt S Δ ↔ coverCond uAnaph uAnt S Δ ∧ coverCond uAnt uAnaph S Δ

        Group identity is the bidirectional version of coverCond.

        source
        def Theories.Semantics.Dynamic.PPCDRT.reciprocityCond {E : Type u} (uAnaph uAnt : ℕ) :
        PPDRSCond E

        Reciprocity (∂(∪u = ∪u') ∧ ∂(u ≠ u')): group identity plus per-state distinctness. The presupposition wrappers are realized semantically when consumers project to Truth3.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Theories.Semantics.Dynamic.PPCDRT.underspecifiedCond {E : Type u} (uAnaph uAnt : ℕ) :
          PPDRSCond E

          Underspecified reflexive/reciprocal: group identity with no distinctness. Permits reflexive, reciprocal, and mixed readings. @cite{murray-2008} (Cheyenne), @cite{cable-2014} (German sich).

          Equations
          Instances For
            source
            theorem Theories.Semantics.Dynamic.PPCDRT.binding_implies_groupIdentity {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (h : bindingCond uAnaph uAnt S Δ) :
            groupIdentityCond uAnaph uAnt S Δ

            Binding implies group identity: pointwise Option equality of dref values yields equality of value-sets. @cite{haug-dalrymple-2020} fig 1.

            source
            theorem Theories.Semantics.Dynamic.PPCDRT.reciprocity_excludes_binding {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (hdef : ∃ (s : Core.PartialAssign E), s ∈ S ∧ ∃ (d : E), s uAnaph = some d) (h : reciprocityCond uAnaph uAnt S Δ) :
            ¬bindingCond uAnaph uAnt S Δ

            Reciprocity excludes binding when there is some state where both drefs are defined: per-state distinctness then contradicts pointwise equality. The hdef hypothesis is necessary because PPCDRT allows both drefs to be undefined at a state, in which case binding (Option none = none) and reciprocity (vacuous distinctness) trivially co-exist.

            source
            theorem Theories.Semantics.Dynamic.PPCDRT.reciprocity_strengthens_underspecified {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (h : reciprocityCond uAnaph uAnt S Δ) :
            underspecifiedCond uAnaph uAnt S Δ

            Reciprocity strengthens underspecified: reciprocity = underspecified

            • per-state distinctness, so reciprocity implies underspecified.
            source
            def Theories.Semantics.Dynamic.PPCDRT.R_u {E : Type u} (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) :
            Set (E × E)

            The set of (anaphor-value, antecedent-value) pairs across the plural state. @cite{haug-dalrymple-2020} eq 127: R_u = {⟨v(s)(u_anaph), v(s)(u_ant)⟩ : s ∈ S}.

            Equations
            Instances For
              source
              theorem Theories.Semantics.Dynamic.PPCDRT.R_u_mono {E : Type u} (uAnaph uAnt : ℕ) {S₁ S₂ : Core.PluralAssign E} (h : ∀ (g : Core.PartialAssign E), g ∈ S₁ → g ∈ S₂) :
              R_u uAnaph uAnt S₁ ⊆ R_u uAnaph uAnt S₂

              A bigger plural state yields a (weakly) bigger R_u.

              source
              def Theories.Semantics.Dynamic.PPCDRT.maximizeAnaphora {E : Type u} (φ : ℕ → ℕ → PPDRSCond E) (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) :
              Prop

              Maximize Anaphora (@cite{haug-dalrymple-2020} eq 128). In interpreting a DRS containing a discourse referent u introduced by a reciprocal with antecedent u' and relation φ, maximize the set R_u of pairs standing in φ, subject to the constraint that φ holds in the local DRS given world knowledge.

              The substrate-level statement: for the chosen plural state S, no proper extension of S (in the lifted-Set sense on R_u) also satisfies φ. Per @cite{haug-dalrymple-2020} §6, this is a generation principle, not a decidable predicate — concrete examples supply per-instance decide-checks.

              Note: the principle replaces the Strongest Meaning Hypothesis of @cite{dalrymple-et-al-1998}; §6.1 of @cite{haug-dalrymple-2020} discusses the empirical contrast (paper eq 132–133).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Theories.Semantics.Dynamic.PPCDRT.maximizeAnaphora_implies_relation {E : Type u} (φ : ℕ → ℕ → PPDRSCond E) (uAnaph uAnt : ℕ) (S : Core.PluralAssign E) (Δ : Set ℕ) (h : maximizeAnaphora φ uAnaph uAnt S Δ) :
                φ uAnaph uAnt S Δ

                Maximize Anaphora implies the chosen state satisfies the relation.