Bruening and Al Khalaf 2020: category mismatches in coordination

Bruening and Al Khalaf argue that coordinated arguments must match in category and may violate selection in two configurations only, a clause beside a noun phrase where only noun phrases are selected and a non-ly adverb beside an adjective before a noun. The violating conjunct is never the one next to the selector, and the two violations are those ellipsis and displacement permit. They derive the clausal case from a null N that makes a noun phrase of a clause but bears none of the semantic selectional features (S-features) a selector checks, with c-selection checked against every conjunct and S-features checked once, as soon as possible, in a structure built from left to right. A coordinate phrase stacks its conjuncts' features by recency, so a selector that precedes it checks the first conjunct and one that follows it the last, HeadDirection.nearest, where the accounts that make the first conjunct prominent check List.take 1. The adverbial case rests on a silent Adv head that ellipsis or a partial copy can leave out. The paper's examples are the rows of Data/Examples/BrueningAlKhalaf2020.

Main definitions

• Conjunct: a phrase as it enters a coordination, itself or a clause under the null N.
• Licensed, Satisfies, Admits: the conditions on coordinated arguments and predicates.
• checkedOnce: the conjunct a selector checks its S-features against, once.
• NominalCoordination, Displaced: an adverb's two escapes from the ban on modifying a noun.

Main results

• mem_cats_of_mem_nearest: the phrase next to the selector is selected in its own category.
• mem_cats_or_of_admits: the only violation is a clause where a noun phrase is selected.
• exists_admits_iff_admits_elided: a phrase may violate selection in a coordination exactly when ellipsis of the selector may strand it.
• mem_cats_of_admits_id: speakers whose S-features persist admit no violation in coordination.
• nominalCoordination_iff, displaced_iff: a non-ly adverb may modify a noun when coordinated before an adjective or displaced.
• argument_rows and its siblings: the model's verdict on each example is its judgment.

Implementation notes

• Coordinated predicates bear the supercategory Pred of Sag, Gazdar, Wasow and Weisler, which is all coordination compares, so they need only Satisfies. The coordinator is left implicit.
• Argument–modifier coordination (§2.1) and the displacement of clauses (§§4.1, 4.5) are not formalized. The questionable (69) counts as excluded.

References

• [BAK20]
• [Mun93]
• [SGWW85]
• [Zha10]

Conjuncts

inductive BrueningAlKhalaf2020.Conjunct : Type

A phrase enters a coordination as a phrase of its own category or, if it is a clause, as the complement of the null N (78), a noun phrase whose semantically empty head bears no S-features (§4.2). The null N has category N and default φ-features, which enter number resolution ((93b)).

• phrase (c : PhraseStructure.Cat) : Conjunct

  A phrase of category c, bearing S-features.

• nullN : Conjunct

  A clause under the null N.

def BrueningAlKhalaf2020.instDecidableEqConjunct.decEq (x✝ x✝¹ : Conjunct) : Decidable (x✝ = x✝¹)

Equations

• BrueningAlKhalaf2020.instDecidableEqConjunct.decEq (BrueningAlKhalaf2020.Conjunct.phrase a) (BrueningAlKhalaf2020.Conjunct.phrase b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• BrueningAlKhalaf2020.instDecidableEqConjunct.decEq (BrueningAlKhalaf2020.Conjunct.phrase c) BrueningAlKhalaf2020.Conjunct.nullN = isFalse ⋯
• BrueningAlKhalaf2020.instDecidableEqConjunct.decEq BrueningAlKhalaf2020.Conjunct.nullN (BrueningAlKhalaf2020.Conjunct.phrase c) = isFalse ⋯
• BrueningAlKhalaf2020.instDecidableEqConjunct.decEq BrueningAlKhalaf2020.Conjunct.nullN BrueningAlKhalaf2020.Conjunct.nullN = isTrue ⋯

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidableEqConjunct : DecidableEq Conjunct

Equations

• BrueningAlKhalaf2020.instDecidableEqConjunct = BrueningAlKhalaf2020.instDecidableEqConjunct.decEq

def BrueningAlKhalaf2020.Conjunct.cat : Conjunct → PhraseStructure.Cat

x.cat is the category the conjunct x projects.

Equations

• (BrueningAlKhalaf2020.Conjunct.phrase c).cat = c
• BrueningAlKhalaf2020.Conjunct.nullN.cat = PhraseStructure.Cat.N

def BrueningAlKhalaf2020.Conjunct.Contentful : Conjunct → Prop

A conjunct bears S-features unless its head is the null N, which is semantically empty (fn. 27).

Equations

• (BrueningAlKhalaf2020.Conjunct.phrase c).Contentful = True
• BrueningAlKhalaf2020.Conjunct.nullN.Contentful = False

@[instance_reducible]

instance BrueningAlKhalaf2020.Conjunct.instDecidablePredContentful : DecidablePred Contentful

Equations

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

def BrueningAlKhalaf2020.Conjunct.ofCat : PhraseStructure.Cat → List Conjunct

ofCat c lists the conjuncts a phrase of category c can be, itself and, for a clause, the noun phrase the null N makes of it.

Equations

• BrueningAlKhalaf2020.Conjunct.ofCat (PhraseStructure.Cat.lex UD.UPOS.SCONJ) = [BrueningAlKhalaf2020.Conjunct.phrase PhraseStructure.Cat.C, BrueningAlKhalaf2020.Conjunct.nullN]
• BrueningAlKhalaf2020.Conjunct.ofCat x✝ = [BrueningAlKhalaf2020.Conjunct.phrase x✝]

theorem BrueningAlKhalaf2020.Conjunct.mem_ofCat {x : Conjunct} {c : PhraseStructure.Cat} : x ∈ ofCat c ↔ x = phrase c ∨ c = PhraseStructure.Cat.C ∧ x = nullN

theorem BrueningAlKhalaf2020.Conjunct.eq_phrase_of_mem_ofCat {x : Conjunct} {c : PhraseStructure.Cat} (h : x ∈ ofCat c) (hx : x.Contentful) : x = phrase c

Licensing

def BrueningAlKhalaf2020.Coordinable (cs : List Conjunct) : Prop

Coordination combines phrases of one category only, since a coordinator selects a category and projects it (82).

Equations

• BrueningAlKhalaf2020.Coordinable cs = ∀ x ∈ cs, ∀ y ∈ cs, x.cat = y.cat

def BrueningAlKhalaf2020.Satisfies (check : List Conjunct → List Conjunct) (cats : Finset PhraseStructure.Cat) (cs : List Conjunct) : Prop

A coordination satisfies a selector that c-selects cats and checks its S-features against the conjuncts check cs when every conjunct is of a c-selected category, c-selection persisting and being checked against each (85), and the conjuncts in check cs bear S-features (88).

Equations

• BrueningAlKhalaf2020.Satisfies check cats cs = ((∀ x ∈ cs, x.cat ∈ cats) ∧ ∀ x ∈ check cs, x.Contentful)

def BrueningAlKhalaf2020.checkedOnce (d : HeadDirection) (cs : List Conjunct) : List Conjunct

A selector on side d checks its S-features once, as soon as it can, and they then delete (§4.3). The coordinate phrase stacks its conjuncts' features by recency (92), so a selector that precedes it checks the stack of the first conjunct alone ((87), (90)) and one that follows it the finished stack, whose last conjunct is on top ((92)).

Equations

• BrueningAlKhalaf2020.checkedOnce d cs = (d.nearest cs).toList

@[simp]

theorem BrueningAlKhalaf2020.mem_checkedOnce {d : HeadDirection} {cs : List Conjunct} {x : Conjunct} : x ∈ checkedOnce d cs ↔ x ∈ d.nearest cs

def BrueningAlKhalaf2020.Licensed (check : List Conjunct → List Conjunct) (cats : Finset PhraseStructure.Cat) (cs : List Conjunct) : Prop

A coordinated argument is licensed when its conjuncts share a category and satisfy the selector.

Equations

• BrueningAlKhalaf2020.Licensed check cats cs = (BrueningAlKhalaf2020.Coordinable cs ∧ BrueningAlKhalaf2020.Satisfies check cats cs)

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidablePredListConjunctCoordinable : DecidablePred Coordinable

Equations

• BrueningAlKhalaf2020.instDecidablePredListConjunctCoordinable x✝ = id inferInstance

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidablePredListConjunctSatisfies {check : List Conjunct → List Conjunct} {cats : Finset PhraseStructure.Cat} : DecidablePred (Satisfies check cats)

Equations

• BrueningAlKhalaf2020.instDecidablePredListConjunctSatisfies x✝ = id inferInstance

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidablePredListConjunctLicensed {check : List Conjunct → List Conjunct} {cats : Finset PhraseStructure.Cat} : DecidablePred (Licensed check cats)

Equations

• BrueningAlKhalaf2020.instDecidablePredListConjunctLicensed x✝ = id inferInstance

def BrueningAlKhalaf2020.Admits (L : List Conjunct → Prop) (ps : List PhraseStructure.Cat) : Prop

A coordination of phrases of the categories ps is admitted under L when some choice of conjuncts for them satisfies L.

Equations

• BrueningAlKhalaf2020.Admits L ps = ∃ cs ∈ (List.map BrueningAlKhalaf2020.Conjunct.ofCat ps).sections, L cs

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidableAdmitsOfDecidablePredListConjunct {ps : List PhraseStructure.Cat} {L : List Conjunct → Prop} [DecidablePred L] : Decidable (Admits L ps)

Equations

• BrueningAlKhalaf2020.instDecidableAdmitsOfDecidablePredListConjunct = id inferInstance

theorem BrueningAlKhalaf2020.Admits.mono {ps : List PhraseStructure.Cat} {L L' : List Conjunct → Prop} (h : ∀ (cs : List Conjunct), L cs → L' cs) (hL : Admits L ps) : Admits L' ps

theorem BrueningAlKhalaf2020.Admits.satisfies {check : List Conjunct → List Conjunct} {cats : Finset PhraseStructure.Cat} {ps : List PhraseStructure.Cat} (h : Admits (Licensed check cats) ps) : Admits (Satisfies check cats) ps

theorem BrueningAlKhalaf2020.mem_sections_map_ofCat {ps : List PhraseStructure.Cat} {cs : List Conjunct} : cs ∈ (List.map Conjunct.ofCat ps).sections ↔ List.Forall₂ (fun (x : Conjunct) (c : PhraseStructure.Cat) => x ∈ Conjunct.ofCat c) cs ps

theorem BrueningAlKhalaf2020.Admits.exists_mem {ps : List PhraseStructure.Cat} {L : List Conjunct → Prop} (h : Admits L ps) : ∃ (cs : List Conjunct), L cs ∧ ∀ p ∈ ps, ∃ x ∈ cs, x ∈ Conjunct.ofCat p

An admitted coordination has conjuncts satisfying L among which each phrase is one.

theorem BrueningAlKhalaf2020.mem_cats_or_of_admits {check : List Conjunct → List Conjunct} {cats : Finset PhraseStructure.Cat} {ps : List PhraseStructure.Cat} (h : Admits (Satisfies check cats) ps) (p : PhraseStructure.Cat) : p ∈ ps → p ∈ cats ∨ p = PhraseStructure.Cat.C ∧ PhraseStructure.Cat.N ∈ cats

The only selectional violation is a clause where a noun phrase is selected (§3.2). A phrase of a category the selector does not c-select can only be a clause under the null N, whichever conjunct the S-features are checked against.

theorem BrueningAlKhalaf2020.mem_cats_of_mem_nearest {cats : Finset PhraseStructure.Cat} {d : HeadDirection} {ps : List PhraseStructure.Cat} (h : Admits (Satisfies (checkedOnce d) cats) ps) (p : PhraseStructure.Cat) : p ∈ d.nearest ps → p ∈ cats

The phrase next to the selector is selected in its own category (§3.1). It is the conjunct the S-features are checked against, so it cannot be a clause under the null N.

theorem BrueningAlKhalaf2020.exists_admits_iff_admits_elided {cats : Finset PhraseStructure.Cat} {d : HeadDirection} {p : PhraseStructure.Cat} (hp : p ∉ cats) : (∃ (q : PhraseStructure.Cat), Admits (Licensed (checkedOnce d) cats) [q, p] ∨ Admits (Licensed (checkedOnce d) cats) [p, q]) ↔ Admits (Licensed (fun (x : List Conjunct) => []) cats) [p]

Coordination permits the violation ellipsis does (§3.3). A phrase of a category the selector does not c-select can be coordinated with another just when it can be stranded by ellipsis of the selector, which deletes the selector's S-features at PF along with it, so that none are checked ((80)).

theorem BrueningAlKhalaf2020.mem_cats_of_admits_id {cats : Finset PhraseStructure.Cat} {ps : List PhraseStructure.Cat} (h : Admits (Satisfies id cats) ps) (p : PhraseStructure.Cat) : p ∈ ps → p ∈ cats

Speakers whose S-features persist admit no violation in coordination (fn. 30). For the many speakers who reject (3a), S-features do not delete once checked but are checked against every conjunct, so no conjunct can be a clause under the null N. Ellipsis, which deletes the selector's S-features, still strands one for them.

Adverbs

inductive BrueningAlKhalaf2020.AdvHead : Type

The head that makes an adverb of an adjective (97) is silent in once, soon and now and the suffix -ly elsewhere. Both are semantically empty (98).

• silent : AdvHead

  The silent head of once, soon and now.

• ly : AdvHead

  The suffix -ly.

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidableEqAdvHead : DecidableEq AdvHead

Equations

• BrueningAlKhalaf2020.instDecidableEqAdvHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BrueningAlKhalaf2020.instFintypeAdvHead : Fintype AdvHead

Equations

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

def BrueningAlKhalaf2020.AdvHead.afterDeletion : AdvHead → Option AdvHead

When PF deletes the material after a modifier, by ellipsis of the noun in the first of two coordinated N′s (103) or in the lower copy of a displaced modifier (100), a silent Adv head, empty in sound and meaning, goes with it, and -ly stays.

Equations

• BrueningAlKhalaf2020.AdvHead.silent.afterDeletion = none
• BrueningAlKhalaf2020.AdvHead.ly.afterDeletion = some BrueningAlKhalaf2020.AdvHead.ly

def BrueningAlKhalaf2020.NominalCoordination (m₁ m₂ : Option AdvHead) : Prop

Two prenominal modifiers, each an adjective (none) or an adverb with its head, can be coordinated as N′s with the first noun elided (102) when the PF ban on adverbs modifying N′ (99) finds no Adv head left on either. The ellipsis takes a silent head on the first along with the noun (103).

Equations

• BrueningAlKhalaf2020.NominalCoordination m₁ m₂ = (m₁.bind BrueningAlKhalaf2020.AdvHead.afterDeletion = none ∧ m₂ = none)

def BrueningAlKhalaf2020.Displaced (m : Option AdvHead) : Prop

A displaced prenominal modifier, adjoined to the noun phrase, escapes the ban on adverbs modifying N′ when its lower copy, adjoined to N′, can leave out its Adv head (100).

Equations

• BrueningAlKhalaf2020.Displaced m = (m.bind BrueningAlKhalaf2020.AdvHead.afterDeletion = none)

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidableNominalCoordination (m₁ m₂ : Option AdvHead) : Decidable (NominalCoordination m₁ m₂)

Equations

• BrueningAlKhalaf2020.instDecidableNominalCoordination m₁ m₂ = id inferInstance

@[instance_reducible]

instance BrueningAlKhalaf2020.instDecidablePredOptionAdvHeadDisplaced : DecidablePred Displaced

Equations

• BrueningAlKhalaf2020.instDecidablePredOptionAdvHeadDisplaced x✝ = id inferInstance

theorem BrueningAlKhalaf2020.nominalCoordination_iff {m₁ m₂ : Option AdvHead} : NominalCoordination m₁ m₂ ↔ m₁ ≠ some AdvHead.ly ∧ m₂ = none

A non-ly adverb can be coordinated with an adjective before a noun, if the adjective comes last; an adverb in -ly cannot (p. 15).

theorem BrueningAlKhalaf2020.displaced_iff {m : Option AdvHead} : Displaced m ↔ m ≠ some AdvHead.ly

The adverbs that may be displaced to modify a noun are the non-ly ones ((56), (57)).

The paper's examples

def BrueningAlKhalaf2020.catOf? (s : String) : Option PhraseStructure.Cat

catOf? s is the category the paper's label s names.

Equations

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

def BrueningAlKhalaf2020.phrases? (e : Datum) : Option (List PhraseStructure.Cat)

phrases? e lists the categories of a row's conjuncts, in order.

Equations

• BrueningAlKhalaf2020.phrases? e = List.mapM BrueningAlKhalaf2020.catOf? (e.features "conjunct")

def BrueningAlKhalaf2020.selects? (e : Datum) : Option (Finset PhraseStructure.Cat)

selects? e is the set of categories a row's selector c-selects.

Equations

• BrueningAlKhalaf2020.selects? e = Option.map List.toFinset (List.mapM BrueningAlKhalaf2020.catOf? (e.features "selects"))

def BrueningAlKhalaf2020.side? (e : Datum) : Option HeadDirection

side? e says whether a row's selector precedes or follows what it selects.

Equations

• BrueningAlKhalaf2020.side? e = e.parse? "selector" [("precedes", HeadDirection.headInitial), ("follows", HeadDirection.headFinal)]

def BrueningAlKhalaf2020.modifiers? (e : Datum) : Option (List (Option AdvHead))

modifiers? e lists a row's prenominal modifiers, in order.

Equations

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

theorem BrueningAlKhalaf2020.construction_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" ∈ [some "predicate", some "argument", some "ellipsis", some "prenominal", some "displacement"]

Every row is one of the five constructions below.

theorem BrueningAlKhalaf2020.predicate_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "predicate" → ∃ ps ∈ phrases? e, ∃ cats ∈ selects? e, ∃ d ∈ side? e, Admits (Satisfies (checkedOnce d) cats) ps ↔ e.judgment = Judgment.acceptable

The model decides the coordinated predicates, each of which must meet the selector's restrictions ((20)–(22)).

theorem BrueningAlKhalaf2020.argument_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "argument" → ∃ ps ∈ phrases? e, ∃ cats ∈ selects? e, ∃ d ∈ side? e, Admits (Licensed (checkedOnce d) cats) ps ↔ e.judgment = Judgment.acceptable

The model decides the arguments, alone or coordinated, before or after their selector ((2)–(3), (39)–(43), (49)–(50), (64), (68)–(69), (77)).

theorem BrueningAlKhalaf2020.argument_rows_first (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "argument" → side? e = some HeadDirection.headFinal → 2 ≤ (e.features "conjunct").length → ∃ ps ∈ phrases? e, ∃ cats ∈ selects? e, Admits (Licensed (List.take 1) cats) ps ↔ e.judgment ≠ Judgment.acceptable

The accounts that make the first conjunct prominent get every coordination before its selector backwards ((41)–(43)).

theorem BrueningAlKhalaf2020.ellipsis_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "ellipsis" → ∃ ps ∈ phrases? e, ∃ cats ∈ selects? e, Admits (Licensed (fun (x : List Conjunct) => []) cats) ps ↔ e.judgment = Judgment.acceptable

The model decides the fragment answers and split questions, which strand a phrase by ellipsis of its selector ((54)–(55), (60), (62), (76)).

theorem BrueningAlKhalaf2020.prenominal_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "prenominal" → ∃ ms ∈ modifiers? e, (ms = [none] ∨ ∃ (m₁ : Option AdvHead) (m₂ : Option AdvHead), ms = [m₁, m₂] ∧ NominalCoordination m₁ m₂) ↔ e.judgment = Judgment.acceptable

The model decides the prenominal modifiers, alone or coordinated ((44), p. 15, (56a), (57a)).

theorem BrueningAlKhalaf2020.displacement_rows (e : Datum) : e ∈ Examples.all → e.feature? "construction" = some "displacement" → ∃ ms ∈ modifiers? e, (∃ (m : Option AdvHead), ms = [m] ∧ Displaced m) ↔ e.judgment = Judgment.acceptable

The model decides the displaced prenominal modifiers ((56b)–(57c)).