Heim, Lasnik and May (1991): Reciprocity and Plurality

This file formalizes the quantificational analysis of reciprocals in [heim-lasnik-may-1991]: each other decomposes at LF into a distributor, each, which moves to the antecedent NP, and a reciprocator, e other, each keeping the semantics of its non-reciprocal use, so that "the men saw each other" is [[the men]₁ each₂] saw [e₂ other]₃ ((8), (20)). The pieces other (16), reciprocator (18), and distributor (19)/(28) compose to eachOtherLF, which is Strong Reciprocity (eachOtherLF_iff_strongReciprocity), is vacuous on a singleton, and is contradictory over an asymmetric relation ((68)). The grain problem of §3, that (43) is three-ways ambiguous under a single indexing, is resolved by the range and distribution indices of plural NPs: the four construals of an embedded pronoun (49) yield the four readings, with the I and you readings bound variables and the we readings coreference, which a preposed adjunct (60) filters. The scope puzzle of §4 is the attachment site of each (67): narrow scope forces coreference and broad scope a bound variable, because distributors need sum-denoting hosts and do not iterate (72) and the trace of each must be bound (74).

Implementation notes

Pluralities are Finsets of atoms and proper atomic parthood is membership, matching the substrate's Reciprocal. The reciprocator has universal force, as the paper adopts while considering groups of two, where universal and existential force coincide; the weaker schemes for larger groups are [dalrymple-et-al-1998]'s. The grain and scope solutions are stated over the finite construal and attachment types, with readings and anaphora types derived; the syntactic derivation of each-movement itself is not represented.

TODO

• §4.2 long-distance reciprocals and the Specified Subject Condition effects of §4.3.

References

• [heim-lasnik-may-1991]
• [higginbotham-1980]
• [higginbotham-1985]
• [dalrymple-et-al-1998]

The compositional pieces (§2.2)

HLM's model is ⟨D, A, Π⟩: a domain with mereological structure, atoms A, and proper-part-of Π; ·Π is the proper-atomic-part relation. Pluralities are encoded here as Finset A (sums of atoms) with ·Π as membership, matching the (R, X) signature of Reciprocal.

def HeimLasnikMay1991.other {A : Type u_1} (contrast : A) (range : Finset A) (z : A) : Prop

(16): other as a 3-place relation — referent z is an atomic part of the range y distinct from the contrast x. In reciprocals both implicit arguments are supplied by the derived antecedent phrase: the contrast is bound by each, the range is coreferential with the antecedent.

Equations

• HeimLasnikMay1991.other contrast range z = (z ∈ range ∧ z ≠ contrast)

def HeimLasnikMay1991.reciprocator {A : Type u_1} (range : Finset A) (ζ : A → A → Prop) (x : A) : Prop

(18): the reciprocator [e other] with universal force: x stands in ζ to every other atomic part of the range. The paper adopts universal force while considering groups of two, where universal and existential force coincide.

Equations

• HeimLasnikMay1991.reciprocator range ζ x = ∀ (z : A), HeimLasnikMay1991.other x range z → ζ x z

def HeimLasnikMay1991.distributor {A : Type u_1} (np : Finset A) (φ : A → Prop) : Prop

(19)/(28): the distributor — each or the covert D — universally quantifies over the atomic parts of its host NP. The world-free Finset form of Plurality.distMaximal (English floated each) and of Algebra.D (Link's D operator).

Equations

• HeimLasnikMay1991.distributor np φ = ∀ x ∈ np, φ x

def HeimLasnikMay1991.eachOtherLF {A : Type u_1} (np : Finset A) (R : A → A → Prop) : Prop

The LF of "np V each other" after each-movement (8)/(20): the distributor scopes over the reciprocated predicate, with the reciprocator's range and contrast both anaphoric to the derived antecedent.

Equations

• HeimLasnikMay1991.eachOtherLF np R = HeimLasnikMay1991.distributor np (HeimLasnikMay1991.reciprocator np R)

The keystone (21)

theorem HeimLasnikMay1991.eachOtherLF_iff_strongReciprocity {A : Type u_1} (np : Finset A) (R : A → A → Prop) : eachOtherLF np R ↔ Reciprocal.StrongReciprocity R np

The compositional each∘other analysis derives Strong Reciprocity: HLM's truth conditions "coincide with those of the standard semantic analyses". Through the entailment lattice of Reciprocal, the weaker schemes follow (strong_imp_weak, …).

theorem HeimLasnikMay1991.eachOtherLF_singleton {A : Type u_1} (a : A) (R : A → A → Prop) : eachOtherLF {a} R

Distribution over a singleton yields a vacuously true reciprocal — no reciprocal content at all. HLM derive the plural-antecedent requirement (*Mary saw each other) more strongly: ·Π is defined only on sum counterdomains, so distributors cannot apply to singular NPs; this vacuity is the semantic shadow of that definedness restriction.

theorem HeimLasnikMay1991.eachOtherLF_asymmetric_contradictory {A : Type u_1} {np : Finset A} {R : A → A → Prop} (hasym : ∀ (x y : A), R x y → ¬R y x) (hcard : 2 ≤ np.card) : ¬eachOtherLF np R

(68) "They are taller than each other" is contradictory: the each∘other composition over an asymmetric relation fails on every genuine plurality. Under embedding, only broad scope of each rescues it ((69)/(70)); with an explicit matrix distributor, re-attachment would stack distributors ((71)/(72)), so only the contradictory narrow reading survives.

The grain problem (§3)

Plural NPs bear a range index and, optionally, a distribution index ((26)–(28)); in a reciprocal LF the reciprocator contributes a third index. An embedded plural pronoun anaphoric to the antecedent therefore has exactly four construals ((29)/(49)) — the theory is exactly as fine-grained as the attested ambiguity of "John and Mary told each other that they should leave".

inductive HeimLasnikMay1991.PronounConstrual : Type

The four construals of an embedded plural pronoun in a reciprocal sentence ((49a–d)).

• range : PronounConstrual

  coindexed with the antecedent's referential range index

• rangeDistributed : PronounConstrual

  range-coindexed, with its own covert distributor D

• distributor : PronounConstrual

  bound by the distribution index contributed by each

• reciprocator : PronounConstrual

  bound by the reciprocator's index

@[instance_reducible]

instance HeimLasnikMay1991.instDecidableEqPronounConstrual : DecidableEq PronounConstrual

Equations

• HeimLasnikMay1991.instDecidableEqPronounConstrual x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HeimLasnikMay1991.instReprPronounConstrual : Repr PronounConstrual

Equations

• HeimLasnikMay1991.instReprPronounConstrual = { reprPrec := HeimLasnikMay1991.instReprPronounConstrual.repr }

def HeimLasnikMay1991.instReprPronounConstrual.repr : PronounConstrual → ℕ → Std.Format

Equations

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

inductive HeimLasnikMay1991.GrainReading : Type

The readings of "John and Mary told each other that they should leave" ((43): I = "each told the other: I should leave", you = "…: you should leave", we together/separately).

• I : GrainReading
• you : GrainReading
• weTogether : GrainReading
• weSeparately : GrainReading

@[instance_reducible]

instance HeimLasnikMay1991.instDecidableEqGrainReading : DecidableEq GrainReading

Equations

• HeimLasnikMay1991.instDecidableEqGrainReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HeimLasnikMay1991.instReprGrainReading.repr : GrainReading → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HeimLasnikMay1991.instReprGrainReading : Repr GrainReading

Equations

• HeimLasnikMay1991.instReprGrainReading = { reprPrec := HeimLasnikMay1991.instReprGrainReading.repr }

def HeimLasnikMay1991.PronounConstrual.reading : PronounConstrual → GrainReading

(49a–d): each construal yields exactly one reading.

Equations

• HeimLasnikMay1991.PronounConstrual.distributor.reading = HeimLasnikMay1991.GrainReading.I
• HeimLasnikMay1991.PronounConstrual.reciprocator.reading = HeimLasnikMay1991.GrainReading.you
• HeimLasnikMay1991.PronounConstrual.range.reading = HeimLasnikMay1991.GrainReading.weTogether
• HeimLasnikMay1991.PronounConstrual.rangeDistributed.reading = HeimLasnikMay1991.GrainReading.weSeparately

inductive HeimLasnikMay1991.AnaphoraType : Type

Bound-variable vs coreference anaphora — the type distinction the grain solution encodes structurally (§3.1, against [higginbotham-1985]'s linking alternative, where I/we would be one vague reading).

• boundVariable : AnaphoraType
• coreference : AnaphoraType

@[instance_reducible]

instance HeimLasnikMay1991.instDecidableEqAnaphoraType : DecidableEq AnaphoraType

Equations

• HeimLasnikMay1991.instDecidableEqAnaphoraType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HeimLasnikMay1991.instReprAnaphoraType.repr : AnaphoraType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HeimLasnikMay1991.instReprAnaphoraType : Repr AnaphoraType

Equations

• HeimLasnikMay1991.instReprAnaphoraType = { reprPrec := HeimLasnikMay1991.instReprAnaphoraType.repr }

def HeimLasnikMay1991.PronounConstrual.anaphoraType : PronounConstrual → AnaphoraType

Construals bound by the quantificational each/other indices are singular bound variables; range-coindexed construals are coreference with the referential sum. Hence I/you = bound variable, we = coreference.

Equations

• HeimLasnikMay1991.PronounConstrual.distributor.anaphoraType = HeimLasnikMay1991.AnaphoraType.boundVariable
• HeimLasnikMay1991.PronounConstrual.reciprocator.anaphoraType = HeimLasnikMay1991.AnaphoraType.boundVariable
• HeimLasnikMay1991.PronounConstrual.range.anaphoraType = HeimLasnikMay1991.AnaphoraType.coreference
• HeimLasnikMay1991.PronounConstrual.rangeDistributed.anaphoraType = HeimLasnikMay1991.AnaphoraType.coreference

def HeimLasnikMay1991.PronounConstrual.DenotesAtom (c : PronounConstrual) : Prop

A bound-variable construal ranges over atoms; a coreferential one denotes the antecedent's sum (§2.4).

Equations

• c.DenotesAtom = (c.anaphoraType = HeimLasnikMay1991.AnaphoraType.boundVariable)

def HeimLasnikMay1991.PronounConstrual.HostsDistributor : PronounConstrual → Prop

The construal places the pronoun under a distributor of its own ((49d)).

Equations

• HeimLasnikMay1991.PronounConstrual.rangeDistributed.HostsDistributor = True
• x✝.HostsDistributor = False

def HeimLasnikMay1991.PronounConstrual.AvailableInPreposedAdjunct (c : PronounConstrual) : Prop

Preposed adjuncts block bound-variable anaphora ((61): a quantifier cannot bind into a preposed adjunct), so "After they had left the room, the candidates criticized each other" (60) keeps only the we construals, while the postposed (57) is fully ambiguous.

Equations

• c.AvailableInPreposedAdjunct = (c.anaphoraType = HeimLasnikMay1991.AnaphoraType.coreference)

@[instance_reducible]

instance HeimLasnikMay1991.instDecidablePredPronounConstrualDenotesAtom : DecidablePred PronounConstrual.DenotesAtom

Equations

• HeimLasnikMay1991.instDecidablePredPronounConstrualDenotesAtom c = HeimLasnikMay1991.instDecidablePredPronounConstrualDenotesAtom._aux_1 c

@[instance_reducible]

instance HeimLasnikMay1991.instDecidablePredPronounConstrualHostsDistributor : DecidablePred PronounConstrual.HostsDistributor

Equations

• One or more equations did not get rendered due to their size.
• HeimLasnikMay1991.instDecidablePredPronounConstrualHostsDistributor HeimLasnikMay1991.PronounConstrual.rangeDistributed = isTrue trivial
• HeimLasnikMay1991.instDecidablePredPronounConstrualHostsDistributor HeimLasnikMay1991.PronounConstrual.range = isFalse HeimLasnikMay1991.instDecidablePredPronounConstrualHostsDistributor._proof_1

@[instance_reducible]

instance HeimLasnikMay1991.instDecidablePredPronounConstrualAvailableInPreposedAdjunct : DecidablePred PronounConstrual.AvailableInPreposedAdjunct

Equations

• HeimLasnikMay1991.instDecidablePredPronounConstrualAvailableInPreposedAdjunct c = HeimLasnikMay1991.instDecidablePredPronounConstrualAvailableInPreposedAdjunct._aux_1 c

theorem HeimLasnikMay1991.not_availableInPreposedAdjunct_iff (c : PronounConstrual) : ¬c.AvailableInPreposedAdjunct ↔ c.reading = GrainReading.I ∨ c.reading = GrainReading.you

The preposed-adjunct diagnostic isolates exactly the bound-variable construals: what (60) loses relative to (57) is the I and you readings.

The scope puzzle (§4)

"John and Mary think they like each other" (64) has a narrow reading (they think: we like each other) and a broad one (each thinks: I like the other). HLM resolve it as the attachment site of each ((67)): to the embedded pronoun (narrow) or to the matrix subject (broad). The correlation with anaphora type is derived: distributors need sum-denoting hosts and cannot iterate, and the trace of each must be bound by the index its host acquires (Principle A).

inductive HeimLasnikMay1991.EachAttachment : Type

Where each attaches at LF ((67a)/(67b)).

• embedded : EachAttachment

  [they₁ each₂] like [e₂ other] — narrow scope

• matrix : EachAttachment

  [[John and Mary]₁ each₂] think they₂ like [e₂ other] — broad

@[instance_reducible]

instance HeimLasnikMay1991.instDecidableEqEachAttachment : DecidableEq EachAttachment

Equations

• HeimLasnikMay1991.instDecidableEqEachAttachment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HeimLasnikMay1991.instReprEachAttachment.repr : EachAttachment → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HeimLasnikMay1991.instReprEachAttachment : Repr EachAttachment

Equations

• HeimLasnikMay1991.instReprEachAttachment = { reprPrec := HeimLasnikMay1991.instReprEachAttachment.repr }

def HeimLasnikMay1991.ScopeWellFormed : EachAttachment → PronounConstrual → Prop

Wellformedness of an attachment–construal pair, from two independent constraints: an each attached to the embedded pronoun needs a sum-denoting host that is not already distributed ((72): distributors do not iterate), and under matrix attachment the pronoun must carry the distribution index so that the trace of each is A-bound (Principle A, (74)).

Equations

• HeimLasnikMay1991.ScopeWellFormed HeimLasnikMay1991.EachAttachment.embedded x✝ = (¬x✝.DenotesAtom ∧ ¬x✝.HostsDistributor)
• HeimLasnikMay1991.ScopeWellFormed HeimLasnikMay1991.EachAttachment.matrix x✝ = (x✝ = HeimLasnikMay1991.PronounConstrual.distributor)

theorem HeimLasnikMay1991.narrow_forces_coreference (c : PronounConstrual) (h : ScopeWellFormed EachAttachment.embedded c) : c.anaphoraType = AnaphoraType.coreference

Narrow scope forces a coreferential pronoun ((67a)).

theorem HeimLasnikMay1991.broad_forces_bound_variable (c : PronounConstrual) (h : ScopeWellFormed EachAttachment.matrix c) : c.anaphoraType = AnaphoraType.boundVariable

Broad scope forces a bound-variable pronoun ((67b)): scope and anaphora type covary, the paper's answer to Williams's nonscope alternative (§4.1).

theorem HeimLasnikMay1991.embedded_unique_construal (c : PronounConstrual) : ScopeWellFormed EachAttachment.embedded c ↔ c = PronounConstrual.range

Under embedded attachment exactly one construal survives: plain range coreference — (67a)'s indexing is forced.