Osborne and Li (2023): Coordination and Referential Dependencies

This file formalizes Osborne and Li's Conjunct Referential Dependency Constraint, the descriptive generalization of the paper's fifth section: a referentially dependent conjunct valent can be co-valued with a full co-valent, but a referentially dependent full valent can hardly be co-valued with a conjunct co-valent. A conjunct valent of a predicate is a conjunct of a coordinate structure that is a valent of the predicate, and a full valent is a valent that is not a conjunct valent (IsConjunctValent, IsFullValent); the constraint is violated when a pronoun that is a full valent takes a conjunct co-valent as its antecedent (Violates), so it is silent where no coordinate structure is present (not_violates_of_no_conjuncts), and since a conjunct valent is never a full valent no pair violates it in both directions (Violates.not_symm). The paper's judgments are crowdsourced mean scores on a scale from 1, the co-valued reading easily possible, to 4, impossible, the double question mark marking the strongly marginal middle, the library's questionable judgment. Each stimulus is a dependency tree over one of the paper's examples, and over the stimuli a violation is never acceptable while a coordinate stimulus without a violation is acceptable (violation_degraded, no_violation_acceptable), the non-coordinate baselines falling under Condition B, on which the paper is silent. The vote answer of (55a) is the paper's own counterexample, a violation judged acceptable (vote_counterexample).

Implementation notes

A valent is a direct valency-relation dependent of the predicate, a simplification of the paper's catena-based notion that the example set does not exercise; the first conjunct heads the coordinate structure in the Universal Dependencies convention, and referential dependence is being a pronoun. The rows of Data/Examples/OsborneLi2023 carry the paper's respondent counts and mean scores.

References

• [OL23]

Conjunct and full valents

def OsborneLi2023.allConjuncts {n : ℕ} (g : DependencyGrammar.Graph n) (c : Fin n) : Finset (Fin n)

The conjuncts of the coordinate structure headed at c: the head, the first conjunct, and its conj dependents.

Equations

• OsborneLi2023.allConjuncts g c = insert c ({w ∈ g.children c | g.label c w = some UD.DepRel.conj})

def OsborneLi2023.HasConjuncts {n : ℕ} (g : DependencyGrammar.Graph n) (c : Fin n) : Prop

Position c heads a coordinate structure: it has a conj dependent.

Equations

• OsborneLi2023.HasConjuncts g c = ∃ w ∈ g.children c, g.label c w = some UD.DepRel.conj

@[instance_reducible]

instance OsborneLi2023.instDecidableHasConjuncts {n : ℕ} (g : DependencyGrammar.Graph n) (c : Fin n) : Decidable (HasConjuncts g c)

Equations

• OsborneLi2023.instDecidableHasConjuncts g c = Finset.decidableExistsAndFinset

def OsborneLi2023.IsConjunctValent {n : ℕ} (g : DependencyGrammar.Graph n) (pred valent : Fin n) : Prop

valent is a conjunct valent of pred: a conjunct of a coordinate structure that fills a valency role of pred.

Equations

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

@[instance_reducible]

instance OsborneLi2023.instDecidableIsConjunctValent {n : ℕ} (g : DependencyGrammar.Graph n) (pred valent : Fin n) : Decidable (IsConjunctValent g pred valent)

Equations

• OsborneLi2023.instDecidableIsConjunctValent g pred valent = Finset.decidableExistsAndFinset

def OsborneLi2023.IsFullValent {n : ℕ} (g : DependencyGrammar.Graph n) (pred valent : Fin n) : Prop

valent is a full valent of pred: a valent that is complete, that is, not a conjunct valent.

Equations

• OsborneLi2023.IsFullValent g pred valent = ((∃ r ∈ g.label pred valent, r.isValencyArg = true) ∧ ¬OsborneLi2023.IsConjunctValent g pred valent)

@[instance_reducible]

instance OsborneLi2023.instDecidableIsFullValent {n : ℕ} (g : DependencyGrammar.Graph n) (pred valent : Fin n) : Decidable (IsFullValent g pred valent)

Equations

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

def OsborneLi2023.Violates {n : ℕ} (g : DependencyGrammar.Graph n) (pred ana ante : Fin n) : Prop

The constraint is violated when the pronoun ana, a full valent of pred, is co-valued with a conjunct valent ante of the same predicate.

Equations

• OsborneLi2023.Violates g pred ana ante = ((g.words ana).cat = UD.UPOS.PRON ∧ OsborneLi2023.IsFullValent g pred ana ∧ OsborneLi2023.IsConjunctValent g pred ante)

@[instance_reducible]

instance OsborneLi2023.instDecidableViolates {n : ℕ} (g : DependencyGrammar.Graph n) (pred ana ante : Fin n) : Decidable (Violates g pred ana ante)

Equations

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

theorem OsborneLi2023.Violates.not_symm {n : ℕ} {g : DependencyGrammar.Graph n} {pred ana ante : Fin n} (h : Violates g pred ana ante) : ¬Violates g pred ante ana

A conjunct valent is not a full valent, so no pair violates the constraint in both directions: the permitted direction is the reverse of the forbidden one.

theorem OsborneLi2023.not_violates_of_no_conjuncts {n : ℕ} {g : DependencyGrammar.Graph n} (h : ∀ (c : Fin n), ¬HasConjuncts g c) (pred ana ante : Fin n) : ¬Violates g pred ana ante

Without a coordinate structure the constraint is silent.

The stimuli

structure OsborneLi2023.Stimulus : Type

A stimulus: the dependency tree of an example, its predicate, the referentially dependent expression and its intended antecedent, and the example's row.

• n : ℕ
• tree : DependencyGrammar.Graph self.n
• pred : Fin self.n
• ana : Fin self.n
• ante : Fin self.n
• row : Datum

def OsborneLi2023.Stimulus.Violates (s : Stimulus) : Prop

The stimulus violates the constraint.

Equations

• s.Violates = OsborneLi2023.Violates s.tree s.pred s.ana s.ante

@[instance_reducible]

instance OsborneLi2023.instDecidablePredStimulusViolates : DecidablePred Stimulus.Violates

Equations

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

def OsborneLi2023.Stimulus.Coordinate (s : Stimulus) : Prop

The stimulus contains a coordinate structure.

Equations

• s.Coordinate = ∃ (c : Fin s.n), OsborneLi2023.HasConjuncts s.tree c

@[instance_reducible]

instance OsborneLi2023.instDecidablePredStimulusCoordinate : DecidablePred Stimulus.Coordinate

Equations

• OsborneLi2023.instDecidablePredStimulusCoordinate x✝ = Fintype.decidableExistsFintype

def OsborneLi2023.ex2a : Stimulus

(2a) Max and Lucie talked about him: a full-valent pronoun with a conjunct antecedent.

Equations

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

def OsborneLi2023.ex3a : Stimulus

(3a) John and Mary talked about himself: the reflexive fares no better.

Equations

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

def OsborneLi2023.ex5a : Stimulus

(5a) Both John and Mary love him: the paired coordinator forces distribution, and the sentence is judged worse than the constraint alone predicts.

Equations

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

def OsborneLi2023.ex9a : Stimulus

(9a) Max talked about himself: the non-coordinate reflexive baseline.

Equations

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

def OsborneLi2023.ex9b : Stimulus

(9b) Max talked about him: the non-coordinate pronoun baseline, marginal by Condition B, on which the constraint is silent.

Equations

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

def OsborneLi2023.ex11a : Stimulus

(11a) Max and Lucie talked about his work: the possessive is no valent of the verb.

Equations

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

def OsborneLi2023.ex11e : Stimulus

(11e) Max and Lucie talked about Max: a name is not referentially dependent.

Equations

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

def OsborneLi2023.ex20b : Stimulus

(20b) Hank and Hillary appear to her to be good friends: the experiencer of a raising predicate is a full valent.

Equations

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

def OsborneLi2023.ex24a : Stimulus

(24a) John talked about himself and his mother: the reflexive heads the coordinate object, so it is a conjunct valent and John a full valent, the permitted direction.

Equations

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

def OsborneLi2023.ex28d : Stimulus

(28d) John expected Mary and him to be able to leave soon: the pronoun is a conjunct of the raised object.

Equations

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

def OsborneLi2023.stimuli : List Stimulus

The paper's stimuli.

Equations

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

theorem OsborneLi2023.violation_degraded (s : Stimulus) : s ∈ stimuli → s.Violates → s.row.judgment ≠ Judgment.acceptable

A violation of the constraint is never judged acceptable.

theorem OsborneLi2023.no_violation_acceptable (s : Stimulus) : s ∈ stimuli → s.Coordinate → ¬s.Violates → s.row.judgment = Judgment.acceptable

A coordinate stimulus that does not violate the constraint is judged acceptable.

The counterexample of the sixth section

def OsborneLi2023.ex55a : Stimulus

(55a) Who voted for Sophy? Sophy and Edgar voted for her: a violation the informants accept, which the paper attributes to an identity split between the candidate and the voter.

Equations

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

theorem OsborneLi2023.vote_counterexample : ex55a.Violates ∧ ex55a.row.judgment = Judgment.acceptable