Docs / Syntax / Agreement / ConjunctAgreement

Agreement with conjoined noun phrases

import Linglib.Syntax.Agreement.ConjunctAgreement · namespace Agreement

A target whose controller consists of conjoined noun phrases agrees with one of them or with all of them. Agreement with one conjunct is normally with the nearest, which is the first or the last according to the side of the conjuncts the target stands on, and occasionally with the first when it is the more distant; agreement with the last when it is the more distant is excluded. Agreement with all conjuncts requires access to the features of every conjunct, from which resolution rules compute the target's values (Agreement.ResolutionRule). A head that checks its selectional features against coordinated arguments has the same options.

This file defines the three options by the conjuncts whose features each gives the target access to, given the conjuncts in linear order and the side of them the target is on.

Main definitions

Agreement.ConjunctAgreement: agreement with the nearest conjunct, with the first, or with all.
Agreement.ConjunctAgreement.conjuncts: the conjuncts an option gives the target access to.

Main results

Agreement.ConjunctAgreement.conjuncts_nearest_eq_first_iff: the nearest conjunct is the first for every coordination exactly when the target precedes the conjuncts.
Agreement.ConjunctAgreement.eq_nearest_of_conjuncts_eq_singleton: a target agrees with the last of several conjuncts alone only by agreeing with the nearest, and only when it follows them.

Implementation notes

The side of the conjuncts the target is on is a HeadDirection, the target counting as the head, so a verb before its conjoined subject is head-initial.
An option says which conjuncts the target accesses, not how its values are computed from theirs: agreement with one conjunct takes that conjunct's values, agreement with all resolves them.
The first conjunct is first in linear order; whether an analysis picks it for its position or as the structurally highest conjunct is left to the analysis.

References

Corbett 2000, Number formalized
Corbett 1991, Gender formalized
Bruening & Al Khalaf 2020, Category mismatches in coordination revisited formalized

Declarations

A target agrees with conjoined noun phrases by agreeing with one conjunct, the nearest or the first, or with all of them.

inductive ConjunctAgreement L52–61

Type

nearest : ConjunctAgreement
Agreement with the nearest conjunct.
first : ConjunctAgreement
Agreement with the first conjunct, the more distant one when the target follows them.
all : ConjunctAgreement
Agreement with all conjuncts, by resolution.

Derives DecidableEq, Fintype, Repr.

Used by ConjunctAgreement.conjuncts, ConjunctAgreement.conjuncts_sublist, ConjunctAgreement.eq_nearest_of_conjuncts_eq_singleton

Used in Corbett2000

a.conjuncts d cs lists the conjuncts, of the conjuncts cs in linear order, whose features a target on side d of them accesses when it agrees by the option a.

def ConjunctAgreement.conjuncts L67–72

{α : Type u_1} :

ConjunctAgreement → HeadDirection → List α → List α

ConjunctAgreement.nearest.conjuncts x✝¹ x✝ = (x✝¹.nearest x✝).toList
ConjunctAgreement.first.conjuncts x✝¹ x✝ = List.take 1 x✝
ConjunctAgreement.all.conjuncts x✝¹ x✝ = x✝

Built from

Used by ConjunctAgreement.conjuncts_nearest, ConjunctAgreement.conjuncts_first, ConjunctAgreement.conjuncts_all, ConjunctAgreement.conjuncts_sublist, ConjunctAgreement.conjuncts_nearest_headInitial, ConjunctAgreement.conjuncts_nearest_eq_first_iff, ConjunctAgreement.conjuncts_nearest_swap_reverse, ConjunctAgreement.eq_nearest_of_conjuncts_eq_singleton

Used in Bruening2025, BrueningAlKhalaf2020, Corbett2000, Schwarzer2026

The nearest conjunct is the first for every coordination exactly when the target precedes the conjuncts, so only a target that follows them tells agreement with the nearest from agreement with the first.

theorem ConjunctAgreement.conjuncts_nearest_eq_first_iff L93–103

{α : Type u_1} {d : HeadDirection} [Nontrivial α] :

(∀ (cs : List α), nearest.conjuncts d cs = first.conjuncts d cs) ↔ d = HeadDirection.headInitial

Built from

L105–107

Agreement with the last conjunct alone is agreement with the nearest by a target that follows the conjuncts: agreement with the last when it is the more distant is excluded (Corbett 2000, p. 197).

theorem ConjunctAgreement.eq_nearest_of_conjuncts_eq_singleton L109–115

{α : Type u_1} {a : ConjunctAgreement} {d : HeadDirection} {l : List α} {x : α} (hl : l ≠ []) (hx : x ∉ l) (h : a.conjuncts d (l ++ [x]) = [x]) :

a = nearest ∧ d = HeadDirection.headFinal

Built from ,