CRDC: Conjunct Referential Dependency Constraint

[OL23]

The Conjunct Referential Dependency Constraint of [OL23], p. 651 (verbatim):

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.

The CRDC governs only configurations in which one of the relevant positions sits inside a coordinate structure; non-coordinate binding falls under Conditions A/B/C, on which the paper is explicit that the CRDC is silent (p. 651). Marginality is constitutive of its empirical content: the paper's crowdsourced acceptability table (p. 630 fn. 3) maps mean scores to markers — ? (1.65–2.29), ?? (2.30–2.94), * (2.95–4.00) — and the CRDC's prediction is ??, Judgment.questionable in the project's enum.

Each theorem builds the tree of a stimulus from Data.Examples.OsborneLi2023 and compares crdcPredictedJudgment with the row's recorded judgment: equality where the CRDC is the operative principle, and a recorded divergence for ex9b, whose sentence-level marginality is Condition B's contribution.

Implementation notes

• "Valent" is operationalised as a direct UD valency-relation dependent of the predicate (UD.DepRel.isValencyArg) — a deliberate simplification of the paper's catena-based notion (§4); the example set does not exercise the difference.
• UD's basic-tree convention makes the first conjunct head the coordinate structure, with remaining conjuncts attached via .conj; the conjunct helpers are two-liners over Graph.children.
• Binding theories elsewhere in linglib (Studies/Chomsky1981.lean, Syntax/HPSG/Coreference.lean) make categorical predictions on non-coordinate stimuli; the CRDC contributes a graded prediction on coordinate ones. A head-to-head comparison needs coordination-aware binding parsers and Judgment-valued output on their side.

TODO

• Cover §6's counterexamples (e.g. the vote-predicate identity split, ex (55a) in the data) with a third-party-referent treatment.

Predicate-valent type

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, per UD) plus 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) (predIdx valentIdx : Fin n) : Prop

Word valentIdx is a conjunct valent of predicate predIdx: a conjunct of a coordinate structure that fills a valency role of predIdx.

Equations

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

@[instance_reducible]

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

Equations

• OsborneLi2023.instDecidableIsConjunctValent g predIdx valentIdx = Finset.decidableExistsAndFinset

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

Word valentIdx is a full valent of predIdx: a valent that is not a conjunct valent — the paper's definition (p. 651): "a valent of a given predicate is a full valent thereof if it is complete, that is, it is not a conjunct valent."

Equations

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

@[instance_reducible]

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

Equations

• OsborneLi2023.instDecidableIsFullValent g predIdx valentIdx = OsborneLi2023.instDecidableIsFullValent._aux_1 g predIdx valentIdx

CRDC prediction

def OsborneLi2023.crdcPredictedJudgment {n : ℕ} (t : DependencyGrammar.Graph n) (predIdx anaIdx anteIdx : Fin n) : Features.Judgment

The CRDC's predicted judgment for co-valuing anaphor anaIdx with antecedent anteIdx under predicate predIdx: .questionable exactly when the anaphor is a full valent and the antecedent a conjunct valent of the same predicate; .acceptable otherwise — the CRDC is silent, and other binding principles may still apply.

Equations

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

CRDC predictions against the data rows

def OsborneLi2023.coordSubject : DependencyGrammar.Graph 6

Ex (2a): "Max and Lucie talked about him." Max(0) and(1) Lucie(2) talked(3) about(4) him(5).

Equations

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

theorem OsborneLi2023.coordSubject_matches_data : crdcPredictedJudgment coordSubject 3 5 0 = Examples.ex2a.judgment

Full-valent him over conjunct-valent Max: the CRDC fires and matches the observed ??.

def OsborneLi2023.reflexiveBaseline : DependencyGrammar.Graph 4

Ex (9a): "Max talked about himself." — non-coordinate baseline.

Equations

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

theorem OsborneLi2023.reflexiveBaseline_matches_data : crdcPredictedJudgment reflexiveBaseline 1 3 0 = Examples.ex9a.judgment

def OsborneLi2023.pronounBaseline : DependencyGrammar.Graph 4

Ex (9b): "Max talked about him." — non-coordinate Condition B context. The CRDC is silent; the row's marginality is Condition B's contribution, so prediction and row diverge by design.

Equations

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

theorem OsborneLi2023.pronounBaseline_crdc_silent : crdcPredictedJudgment pronounBaseline 1 3 0 = Features.Judgment.acceptable ∧ Examples.ex9b.judgment = Features.Judgment.questionable

def OsborneLi2023.coordObject : DependencyGrammar.Graph 7

Ex (24a): "John talked about himself and his mother." — coordinate object; himself heads the coordination, so it is a conjunct valent and John a full valent: the CRDC's permitted direction.

Equations

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

theorem OsborneLi2023.coordObject_matches_data : crdcPredictedJudgment coordObject 1 3 0 = Examples.ex24a.judgment

def OsborneLi2023.pairedCoordSubject : DependencyGrammar.Graph 6

Ex (5a): "Both John and Mary love him." — coordinate subject with paired coordinator; pronoun in object position. The CRDC fires and matches the observed ??.

Equations

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

theorem OsborneLi2023.pairedCoordSubject_matches_data : crdcPredictedJudgment pairedCoordSubject 4 5 1 = Examples.ex5a.judgment

def OsborneLi2023.raisingCoordObject : DependencyGrammar.Graph 8

Ex (28d): "John expected Mary and him to be able to leave soon." — coordinate object under raising-to-object: him is a conjunct valent, so the CRDC is silent on co-valuing it with John.

Equations

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

theorem OsborneLi2023.raisingCoordObject_matches_data : crdcPredictedJudgment raisingCoordObject 1 4 0 = Examples.ex28d.judgment

Directionality

theorem OsborneLi2023.direction_asymmetry : crdcPredictedJudgment coordSubject 3 5 0 = Features.Judgment.questionable ∧ crdcPredictedJudgment coordSubject 3 0 5 = Features.Judgment.acceptable

The CRDC is asymmetric: on ex2a's tree, only the full-anaphor-of- conjunct-antecedent direction fires; swapping anaphor and antecedent leaves the CRDC silent.