Documentation

Linglib.Studies.Anaphora.HaugDalrymple2020

Haug & Dalrymple (2020) @cite{haug-dalrymple-2020} #

Reciprocity: Anaphora, scope, and quantification. Semantics & Pragmatics 13:10, 1–62. doi:10.3765/sp.13.10.

The relational analysis of reciprocals in Partial Plural Compositional DRT (PPCDRT). Each other is a pronoun bearing an anaphoric relation (reciprocity R) to its antecedent; the narrow/wide scope ambiguity reduces to the choice of antecedent relation between the matrix subject and the embedded local antecedent (group identity ∪ vs. binding =).

What is formalized #

Witness-based formalisation of the paper's empirical contributions over the PPCDRT substrate (Theories/Semantics/Dynamic/PPCDRT/):

Paper §TopicWitness type
§3Scope readings (narrow / wide)PluralAssign Person
§3.3Crossed readings (4-cell classification)RecipReading triples
§4.2Underspecified RECIP/REFLunderspecifiedCond lattice
§4.4Multiple reciprocalsTwo-reciprocal witness
§4.5Subgroup readings (forks, gravity)Weak-vs-strong contrast
§4.6Collective antecedentsDistinctness neutralization
§5Quantified antecedents + truth-value gapTruth3 via removeGap
§6Maximize Anaphora as a principleR_u + maximizeAnaphora
§6.2Multi-reciprocal pairwise predictionR_u over two reciprocals
§6.3MA interacting with scopeTracy/Matty/Chris case

Sections paper-acknowledged but not formalised (out of scope for a study-file size budget): the full §2.3 Δ-relativised distribution machinery (deferred — the substrate-trimming pass removed the prototyped delta///max^u operators since no consumer exercised them; they will return alongside a Brasoveanu 2007 / Dotlačil 2013 study file); the §5.2 empirical-fit table; the §7 typological excursus.

Connections to existing linglib substrate #

Source-paper attribution note #

The §4.2 paragraph in @cite{haug-dalrymple-2020} attributes the German sich / Romance reflexive examples to @cite{cable-2014} (paper p. 32), not to @cite{murray-2008} alone — the latter focuses on Cheyenne. The docstrings here follow that attribution.

Three salient discourse participants. Reused throughout the paper's examples (Tracy and Chris in §3, Tracy/Matty/Chris in §6.3).

Instances For
    @[implicit_reducible]
    Equations
    def HaugDalrymple2020.instReprPerson.repr :
    PersonStd.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]

      Standard dref indices used throughout.

      Equations
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            Equations
            Instances For

              A partial assignment with u₁ ↦ a, u₂ ↦ b, u₃ ↦ c.

              Equations
              Instances For
                @[simp]
                theorem HaugDalrymple2020.assign2_u₁ (a b : Person) :
                assign2 a b u₁ = some a
                @[simp]
                theorem HaugDalrymple2020.assign2_u₂ (a b : Person) :
                assign2 a b u₂ = some b
                @[simp]
                theorem HaugDalrymple2020.assign3_u₁ (a b c : Person) :
                assign3 a b c u₁ = some a
                @[simp]
                theorem HaugDalrymple2020.assign3_u₂ (a b c : Person) :
                assign3 a b c u₂ = some b
                @[simp]
                theorem HaugDalrymple2020.assign3_u₃ (a b c : Person) :
                assign3 a b c u₃ = some c

                Narrow-scope state for paper eq 49: two assignments where each girl has herself as the embedded subject pronoun. The matrix subject (u₁) and the embedded subject pronoun (u₂) have IDENTICAL value-sets: {Tracy, Chris}. This is group identity (∪u₂ = ∪u₁).

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

                  The summed value of u₁ across the narrow-scope state is {tracy, chris}.

                  The summed value of u₂ across the narrow-scope state is {tracy, chris}.

                  Narrow scope is group identity (paper §3, eq 49). The matrix subject (u₁) and the embedded subject pronoun (u₂) have the same value-set, witnessing the groupIdentityCond of the relational analysis.

                  Wide-scope state for paper eq 51: u₂ is bound by u₁ — pointwise identity of values. Each girl thought only of herself as the winner.

                  UNVERIFIED collapse. The paper distinguishes narrow eq 49 (a 4-row table including a doxastic-world column w) from wide eq 51 (a 2-row table without w). The empirical contrast lives in the presence/absence of the doxastic-alternative column, which the intensional δ_w machinery (paper §3.1) makes visible. The current narrowScopeState/wideScopeState encoding flattens both to a 2-row table — the pointwise-vs-coverage distinction is correct at each row but the row-multiplicity contrast is lost. Setting wideScopeState := narrowScopeState reflects this collapse honestly: until the substrate exposes δ_w, the two states are extensionally identical for the 2-element domain.

                  Equations
                  Instances For

                    Wide scope is binding (paper §3, eq 51). In every state of the plural information state, the embedded subject pronoun's value equals the matrix subject's value as Option E.

                    Wide scope also satisfies group identity (binding ⊆ group identity). This is the substrate-level fact binding_implies_groupIdentity applied to this concrete case.

                    Narrow-scope reciprocity state for paper eq 53: u₁ (matrix subject) and u₂ (embedded subject) are group-identical (each girl thought of the group); u₃ (reciprocal) takes the other girl's value at each state. Tracy saw Chris, Chris saw Tracy.

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

                      Reciprocity satisfies group identity between subject pronoun and reciprocal (∪u₃ = ∪u₂).

                      theorem HaugDalrymple2020.reciprocity_distinct (s : Core.PartialAssign Person) :
                      s reciprocityState∀ (d_a d_b : Person), s u₂ = some d_as u₃ = some d_bd_a d_b

                      Reciprocity satisfies per-state distinctness (∂(u₂ ≠ u₃)).

                      The two-parameter classification: locus × antecedent relation. Three cells are attested; the (low, bound) cell is empirically empty per paper p. 24 — bound antecedents force high locus.

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

                        The empty fourth cell: there is no RecipReading with low locus and binding antecedent. Paper p. 24: "the bound reading of the reciprocal's antecedent cannot cooccur with a low locus for the reciprocal, because it does not make available the plurality that the reciprocal needs."

                        Crossed readings (paper §3.3, eq 56): high locus + group-identity antecedent + group-identity reciprocal slot. The reciprocity comes from the DRS distinctness presupposition ∂(u₃ ≠ u₂), not from an anaphoric reciprocity relation. Empirically attested via the Jennifer Lawrence interview headline (paper p. 25, ex. 57) and related corpus examples.

                        Underspecified anaphors (German sich, Cheyenne REFL/RECIP affix) contribute group identity without the distinctness presupposition. They permit reflexive (binding-style), reciprocal, and mixed readings. The semantic core is just groupIdentityCond — reciprocity is one specialization among others.

                        Underspecified anaphors also admit reciprocity readings — reciprocity strengthens underspecified by adding distinctness.

                        Multiple-reciprocal state for paper (85a) reading "where the second reciprocal takes the first one as its antecedent" — semantically interpretation (84b): "Tracy gave Chris a picture of Tracy, and Chris gave Tracy a picture of Chris." Per paper eq 85 (p. 35–36):

                        • u₁ = subject (each girl, the giver)
                        • u₂ = first reciprocal (each other₁), antecedent u₁
                        • u₃ = pictures
                        • u₄ = second reciprocal (each other₂), antecedent u₂; per the reading, u₄ takes the value of "the other member of u₂'s antecedent group" = u₁ (the giver).

                        Distinctness conditions per eq 85b: ∂(u₁ ≠ u₂) and ∂(u₂ ≠ u₄). Each reciprocal is distinct from its OWN antecedent. There is no constraint between u₃ (pictures) and any reciprocal.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem HaugDalrymple2020.multipleRecip_both_distinct :
                          (∀ smultipleRecipState, ∀ (d_a d_b : Person), s u₁ = some d_as u₂ = some d_bd_a d_b) smultipleRecipState, ∀ (d_a d_b : Person), s u₂ = some d_as u₄ = some d_bd_a d_b

                          Both reciprocals satisfy the paper's distinctness conditions per eq 85b: u₂ ≠ u₁ (first reciprocal distinct from antecedent u₁) and u₄ ≠ u₂ (second reciprocal distinct from its antecedent u₂).

                          "The forks are propped against each other" (paper eq 88b): each fork is supported by a group containing one or more of the others — possibly all, but not necessarily. This is weak reciprocity: R_u need not be the full Cartesian product minus the diagonal.

                          Implementation: a 3-fork example where fork₁ leans on fork₂, fork₂ on fork₃, fork₃ on fork₁ (a chain). R_u = {(1,2), (2,3), (3,1)} — NOT the full strong-reciprocity {(1,2), (2,1), (1,3), (3,1), (2,3), (3,2)}.

                          Note on paper eq 92. The paper's actual analysis (eq 92) wraps the support relation in δ_{u_1} distribution and uses sum-dref ∪u_2 on the supporter side. Our flat 3-row encoding shows the R_u-shape weak-reciprocity property at the value-set level but does not exercise the equivalence-class structure that distribution builds. The δ-side of the analysis is substrate-deferred (PPCDRT delta was trimmed in P6).

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

                            Strong reciprocity would require each fork to lean on EVERY other — e.g., (tracy, matty) would also need to be in R_u. The fork-chain state does NOT satisfy strong reciprocity.

                            Collective antecedents NEUTRALIZE the distinctness condition: when the predicate work-together is interpreted collectively on ∪u₁, the per-state distinctness u₁u₃ becomes vacuous.

                            The state below has u₁ = sailor at each row, with u₃ = ship-of pointing to (possibly the same!) sailor as u₁. Reciprocity-as-stated fails (no per-state distinctness), but the sentence is felicitous because the collective interpretation of u₁ does the predicational work. Paper p. 39.

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

                              The collective state satisfies group identity (∪u₁ = ∪u₃) but FAILS per-state distinctness — formal reciprocity does not hold. The sentence is felicitous because work-together is collective.

                              Paper §5 introduces max^u(K) and shows that quantified antecedents of reciprocals (most members know each other; few have spoken to each other) give rise to a truth-value gap: True iff true on both the maximal-set reading and the reference-set reading; False iff false on both; Neither otherwise (paper eq 109). The paper invokes @cite{champollion-bumford-henderson-2019}, following @cite{kriz-2015}, for the supervaluationist machinery.

                              Here we encode the truth-value gap directly via `Truth3`, exploiting
                              the existing `Theories/Semantics/Homogeneity/Basic.lean` substrate
                              (`removeGap`, `Truth3.metaAssert`). 
                              
                              def HaugDalrymple2020.quantifiedReciprocalTV (maximalSetReading refSetReading : Prop) [Decidable maximalSetReading] [Decidable refSetReading] :

                              The truth value of a quantified-antecedent reciprocal sentence, given its truth on the maximal-set reading and on the reference-set reading. Paper eq 109.

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

                                The two precisifications H&D §5 makes available for a quantified-antecedent reciprocal sentence: the maximal set reading (u ranges over the largest restrictor-satisfying set) and the reference set reading (u ranges over the largest set such that the scope-plus-reciprocal relation holds). Paper §5.1, eq 99.

                                Instances For
                                  @[implicit_reducible]
                                  Equations
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def HaugDalrymple2020.hdEval (maximalSetReading refSetReading : Prop) :

                                    Lift a (maximal-set-reading, reference-set-reading) pair of Props to a Prop-valued evaluation over the H&D precisification space.

                                    Equations
                                    Instances For
                                      @[implicit_reducible]
                                      instance HaugDalrymple2020.hdEval.instDecidable (m r : Prop) [Decidable m] [Decidable r] :
                                      DecidablePred (hdEval m r)
                                      Equations
                                      • One or more equations did not get rendered due to their size.

                                      Bridge theorem (P8) — H&D §5's truth-value gap (paper eq 109) instantiates a 2-precisification supervaluation construction. Paper §5 footnote 23 cites Križ 2015 and Champollion-Bumford-Henderson 2019 as inspirations for the gap shape; this theorem makes the structural correspondence Lean-checkable: quantifiedReciprocalTV m r agrees with superTrue (hdEval m r) hdSpec over the two-element {maximalSet, referenceSet} precisification space.

                                      The paper itself is more guarded than "the §5 gap is CBH 2019" — it says §5 is inspired by CBH/Križ. The theorem here exhibits the truth-table reproducibility (paper eq 109 ↔ superTrue on a 2-element space), not a deeper claim about identity of analyses.

                                      Sibling parallel — Križ 2016 plural homogeneity. Phenomena/Plurals/Studies/Kriz2016.lean's barePluralTV_eq_superTrue proves barePluralTV P x w = superTrue (fun a => P a w) ⟨x, hne⟩ — plural homogeneity reduces to superTrue over atoms in the plurality as specification points. The bridge above shows the H&D §5 reciprocal gap reduces to superTrue over precisifications of the reciprocal's restrictor ({maximalSet, referenceSet}). Both instances share the supervaluationist shape; only the spec-space sort differs. The Križ2016 §7 docstring explicitly enumerates this as one of five linglib instances of the same pattern (Fine/Križ/dist/ selectional/H&D), making the H&D ↔ Križ structural agreement grep-able from either end.

                                      This theorem is the Lean-level smoke test: H&D's gap agrees with the image of superTrue evaluated at the H&D spec-eval pair, exactly as Križ's gap agrees with superTrue at the atomic-spec pair.

                                      The R_u set for the narrow-scope reciprocity state. Reciprocity means R_u(u₂, u₃) is the full off-diagonal pair set on the value range — for a 2-element range {Tracy, Chris}, this is exactly two pairs: (Tracy, Chris) and (Chris, Tracy). Paper eq 127.

                                      A "diagonal" pair like (Tracy, Tracy) is NOT in R_u for reciprocity: the per-state distinctness condition rules it out.

                                      Paper §6.1 (p. 55) argues SMH over-strengthens. The substrate-level refutation lives in Reciprocals.lean as SMH_diverges_from_relational — the relational analysis with MA leaves both readings available on the default property bundle, while SMH commits to narrow only.

                                      Related principles cited by paper §6: the Maximal Interpretation
                                      Hypothesis of @cite{sabato-winter-2012} and @cite{winter-2001}
                                      (p. 54), the typicality-constrained MA of @cite{poortman-struiksma-kerem-friedmann-winter-2018}
                                      (p. 54), the anaphora-as-exhaustive principle of @cite{kadmon-1990}
                                      (p. 54), and the experimental evidence of @cite{majewski-2014}
                                      (paper §6 docstring reference). The trio MIH/MA/SMH form the natural
                                      scaffold for a principled treatment of the §4.5 reciprocal-strength
                                      typology — see the open work in the future-directions note below. 
                                      

                                      Paper §6.2 (p. 56): for "The classmates gave each other pictures of each other," Maximize Anaphora predicts pairwise maximization (each classmate gave a picture-of-each-other to each other classmate), NOT the all-triples reading.

                                      The state here witnesses the pairwise reading: in each state, u₃ (the picture's subject) and u₄ (the receiver) form a swap pair.

                                      Equations
                                      Instances For

                                        The pairwise R_u u₂ u₁ for the first reciprocal (each other₁, antecedent u₁) has exactly two pairs: (Chris, Tracy) and (Tracy, Chris) — read as (receiver, giver) per the paper's pair convention.

                                        Witnesses: row 1 (Tracy gave Chris) gives (u₂=Chris, u₁=Tracy) and row 2 (Chris gave Tracy) gives (u₂=Tracy, u₁=Chris).

                                        Paper eq 135: "Tracy, Matty and Chris think they praised each other." Three-element antecedent group; the wide-scope reading on the matrix plural information state is witnessed below. Paper eq 136 shows the sample output state with three girls × two complement-mate pairs.

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

                                          The bridge theorem from PPCDRT/Cumulativity.lean is consumable here: group identity reduces to Beck-Sauerland ** over the Finset of value pairs. This is the formal realization of @cite{langendoen-1978}'s reciprocity-as-cumulativity claim, asserted in the original Reciprocals.lean docstring as prose (audit finding 4).