Keenan and Comrie (1977): Noun Phrase Accessibility and Universal Grammar

This file formalizes the Hierarchy Constraints of [KC77] on the Accessibility Hierarchy of grammatical positions, subject > direct object > indirect object > oblique > genitive > object of comparison: a language must relativize subjects, every relative-clause strategy applies to a continuous segment of the hierarchy, and a strategy may cease at any lower point (Section 1.2). A strategy is primary when it relativizes subjects, and the paper's Primary Relativization Constraint, that a primary strategy reaching a low position reaches every higher one, follows from continuity: the positions a continuous primary strategy covers form an upper set of the hierarchy order (prc_of_hc2).

The paper's strategies are derived, not recorded. Two relative clauses are formed by different strategies when their heads are placed differently or when one is case-coding, presenting an element that expresses which position is relativized, and the other not (p. 65); a retained personal pronoun codes case as a relative pronoun does (p. 66). So a strategy is a placement and a case-coding value (Strategy), and the positions it covers in a language are those some relativizer of the language realizes with an element of that value (Strategy.positions). Table 1's rows follow from the fragments' relativizers: Hebrew's direct object is covered by both of its strategies (hebrew_table1), and Arabic's row is the gap at the subject and pronoun retention below it (arabic_table1).

The constraints are then checked on the seventeen languages of Table 1 whose relativizers the fragments record (hc1_verified, hc2_verified), so every primary strategy of the sample covers the interval from its cut-off up to the subject (primary_positions_eq_Icc_top); each position from subject to genitive is attested as the cut-off of a primary strategy, the paper's Section 1.3 argument for the third constraint (each_upper_cutoff_attested); and Toba Batak's gap at direct object between two continuous strategies shows why the constraints are stated per strategy rather than per language (toba_batak_do_gap). The pattern of pronoun retention (Section 2.2.2, Table 2) is derived the same way: once a language retains a pronoun at a position it retains one at every lower position it relativizes (retention_verified).

Implementation notes

The hierarchy order is the substrate's Position bounded linear order, the subject its top, and a strategy's continuity is order-connectedness of the positions it covers. A relative pronoun agreeing with the head, such as English who (p. 65), leaves the relativized position a gap (Relativization.NPRel), so case coding is a property of what occupies that position (IsCaseCoding). Table 1 records Classical Arabic and the fragment Modern Standard Arabic, whose relativizer covers the row's positions; since the paper considers only definite relative clauses (p. 64), the sample takes the relativizer of a definite antecedent. The languages the fragments add after 1977 are not consulted.

References

• [KC77]

Strategies (Section 1.1)

def KeenanComrie1977.IsCaseCoding (x : Relativization.NPRel) : Prop

Case coding (p. 65): the element at the relativized position expresses which position it is, as a relative pronoun marked for it or a retained personal pronoun does (p. 66); a gap expresses none.

Equations

• KeenanComrie1977.IsCaseCoding x = (x ≠ Relativization.NPRel.gap)

@[instance_reducible]

instance KeenanComrie1977.instDecidablePredNPRelIsCaseCoding : DecidablePred IsCaseCoding

Equations

• KeenanComrie1977.instDecidablePredNPRelIsCaseCoding x✝ = { decide := !decide (x✝ = Relativization.NPRel.gap), reflects_decide := ⋯ }

structure KeenanComrie1977.Strategy : Type

An RC-forming strategy (p. 65): relative clauses are formed by different strategies when their heads are placed differently or one is case-coding and the other not.

• placement : Relativization.Placement

  The placement of the clause relative to its head.

• caseCoding : Bool

  Whether the strategy is case-coding, the paper's ±case.

@[instance_reducible]

instance KeenanComrie1977.instDecidableEqStrategy : DecidableEq Strategy

Equations

• KeenanComrie1977.instDecidableEqStrategy = KeenanComrie1977.instDecidableEqStrategy.decEq

def KeenanComrie1977.instDecidableEqStrategy.decEq (x✝ x✝¹ : Strategy) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance KeenanComrie1977.instFintypeStrategy : Fintype Strategy

Equations

• KeenanComrie1977.instFintypeStrategy = Fintype.ofEquiv ((_ : Relativization.Placement) × Bool) KeenanComrie1977.Strategy.proxyTypeEquiv

def KeenanComrie1977.Strategy.positions (s : Strategy) (L : List Relativizer) : Finset Relativization.Position

The positions a language relativizes by a strategy: those some relativizer with its placement realizes with an element of its case coding.

Equations

• s.positions L = {p : Relativization.Position | ∃ r ∈ L, r.placement = s.placement ∧ ∃ x ∈ r.realize p, decide (KeenanComrie1977.IsCaseCoding x) = s.caseCoding}

def KeenanComrie1977.Strategy.IsPrimary (s : Strategy) (L : List Relativizer) : Prop

A strategy is primary when it relativizes subjects.

Equations

• s.IsPrimary L = (⊤ ∈ s.positions L)

@[instance_reducible]

instance KeenanComrie1977.Strategy.instDecidableIsPrimary (s : Strategy) (L : List Relativizer) : Decidable (s.IsPrimary L)

Equations

• s.instDecidableIsPrimary L = KeenanComrie1977.Strategy.instDecidableIsPrimary._aux_1 s L

The Hierarchy Constraints (Section 1.2)

def KeenanComrie1977.SatisfiesHC1 (L : List Relativizer) : Prop

HC₁: some strategy relativizes subjects.

Equations

• KeenanComrie1977.SatisfiesHC1 L = ∃ (s : KeenanComrie1977.Strategy), s.IsPrimary L

@[instance_reducible]

instance KeenanComrie1977.instDecidableSatisfiesHC1 (L : List Relativizer) : Decidable (SatisfiesHC1 L)

Equations

• KeenanComrie1977.instDecidableSatisfiesHC1 L = { decide := decide (∃ a ∈ Finset.univ, (fun (x : KeenanComrie1977.Strategy) => x.IsPrimary L) a), reflects_decide := ⋯ }

def KeenanComrie1977.SatisfiesHC2 (L : List Relativizer) : Prop

HC₂: every strategy covers a continuous segment of the hierarchy.

Equations

• KeenanComrie1977.SatisfiesHC2 L = ∀ (s : KeenanComrie1977.Strategy), (↑(s.positions L)).OrdConnected

@[instance_reducible]

instance KeenanComrie1977.instDecidableSatisfiesHC2 (L : List Relativizer) : Decidable (SatisfiesHC2 L)

Equations

• KeenanComrie1977.instDecidableSatisfiesHC2 L = { decide := decide (∀ a ∈ Finset.univ, (fun (x : KeenanComrie1977.Strategy) => (↑(x.positions L)).OrdConnected) a), reflects_decide := ⋯ }

def KeenanComrie1977.SatisfiesPRC (L : List Relativizer) : Prop

The Primary Relativization Constraint: a primary strategy covers an upper set of the hierarchy, every position above one it reaches.

Equations

• KeenanComrie1977.SatisfiesPRC L = ∀ (s : KeenanComrie1977.Strategy), s.IsPrimary L → IsUpperSet ↑(s.positions L)

theorem KeenanComrie1977.prc_of_hc2 {L : List Relativizer} (h : SatisfiesHC2 L) : SatisfiesPRC L

The Primary Relativization Constraint follows from HC₂ and the definition of primary, as the paper derives it: a continuous strategy that relativizes subjects covers an upper set.

The sample (Table 1)

The seventeen languages of Table 1 whose relativizers the fragments record.

@[reducible, inline]

abbrev KeenanComrie1977.english : List Relativizer

Equations

• KeenanComrie1977.english = English.Relativization.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.welsh : List Relativizer

Equations

• KeenanComrie1977.welsh = Welsh.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.arabic : List Relativizer

Table 1's Classical Arabic, by the Modern Standard Arabic relativizer of a definite antecedent, the paper considering only definite restrictive relative clauses (p. 64).

Equations

• KeenanComrie1977.arabic = [Arabic.ModernStandard.relativizer Reference.Definiteness.definite]

@[reducible, inline]

abbrev KeenanComrie1977.hebrew : List Relativizer

Equations

• KeenanComrie1977.hebrew = Hebrew.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.tobaBatak : List Relativizer

Equations

• KeenanComrie1977.tobaBatak = TobaBatak.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.korean : List Relativizer

Equations

• KeenanComrie1977.korean = Korean.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.finnish : List Relativizer

Equations

• KeenanComrie1977.finnish = Finnish.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.malagasy : List Relativizer

Equations

• KeenanComrie1977.malagasy = Malagasy.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.mandarin : List Relativizer

Table 1's Chinese, spoken Pekingese.

Equations

• KeenanComrie1977.mandarin = Mandarin.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.basque : List Relativizer

Equations

• KeenanComrie1977.basque = Basque.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.french : List Relativizer

Equations

• KeenanComrie1977.french = French.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.german : List Relativizer

Equations

• KeenanComrie1977.german = German.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.hindi : List Relativizer

Table 1's Hindi.

Equations

• KeenanComrie1977.hindi = HindiUrdu.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.japanese : List Relativizer

Equations

• KeenanComrie1977.japanese = Japanese.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.russian : List Relativizer

Equations

• KeenanComrie1977.russian = Russian.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.tagalog : List Relativizer

Equations

• KeenanComrie1977.tagalog = Tagalog.relativizers

@[reducible, inline]

abbrev KeenanComrie1977.turkish : List Relativizer

Equations

• KeenanComrie1977.turkish = Turkish.relativizers

def KeenanComrie1977.sample : List (List Relativizer)

The sample.

Equations

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

theorem KeenanComrie1977.hebrew_table1 : { placement := Relativization.Placement.postNominal, caseCoding := false }.positions hebrew = {Relativization.Position.subject, Relativization.Position.directObject} ∧ { placement := Relativization.Placement.postNominal, caseCoding := true }.positions hebrew = Finset.Iic Relativization.Position.directObject

Table 1's Hebrew (p. 77): the −case strategy covers subjects and direct objects and the +case strategy everything from direct objects down, the direct object shared between them.

theorem KeenanComrie1977.arabic_table1 : { placement := Relativization.Placement.postNominal, caseCoding := false }.positions arabic = {⊤} ∧ { placement := Relativization.Placement.postNominal, caseCoding := true }.positions arabic = {⊤}ᶜ

Table 1's Arabic (p. 76): the −case strategy covers the subject alone and the +case strategy every other position.

theorem KeenanComrie1977.hc1_verified (L : List Relativizer) : L ∈ sample → SatisfiesHC1 L

HC₁ holds of every language in the sample.

theorem KeenanComrie1977.hc2_verified (L : List Relativizer) : L ∈ sample → SatisfiesHC2 L

HC₂ holds of every strategy in the sample.

theorem KeenanComrie1977.prc_verified (L : List Relativizer) : L ∈ sample → SatisfiesPRC L

Hence so does the Primary Relativization Constraint.

theorem KeenanComrie1977.primary_positions_eq_Icc_top (L : List Relativizer) : L ∈ sample → ∀ (s : Strategy) (hp : s.IsPrimary L), s.positions L = Finset.Icc ((s.positions L).min' ⋯) ⊤

In the sample every primary strategy covers exactly the closed interval from its cut-off up to the subject, by HC₂ and Finset.eq_Icc_top_of_ordConnected_coe: what Table 1 records as a run of + entries ending at the subject.

theorem KeenanComrie1977.each_upper_cutoff_attested (p : Relativization.Position) : p ∈ [Relativization.Position.subject, Relativization.Position.directObject, Relativization.Position.indirectObject, Relativization.Position.oblique, Relativization.Position.genitive] → ∃ L ∈ sample, ∃ (s : Strategy), s.positions L = Finset.Icc p ⊤

Every position from subject to genitive is the cut-off of some primary strategy in the sample, which covers exactly the interval from there up to the subject: the Section 1.3 argument that each point of the hierarchy is a possible cut-off. The paper's witnesses for the object of comparison are not among the fragments.

Toba Batak (Section 1.2.2)

theorem KeenanComrie1977.toba_batak_do_gap (r : Relativizer) : r ∈ tobaBatak → r.realize Relativization.Position.directObject = ∅

Toba Batak relativizes subjects by one strategy and indirect objects through genitives by another, but direct objects by neither: the gap lies between two continuous strategies, which is why the constraints govern strategies rather than languages.

Strategies by their relativized position (Section 1.3)

theorem KeenanComrie1977.korean_genitive_retention : { placement := Relativization.Placement.preNominal, caseCoding := false }.positions korean = Finset.Icc Relativization.Position.oblique ⊤ ∧ ∀ r ∈ korean, r.realize Relativization.Position.genitive = {Relativization.NPRel.resumptive}

Korean (Section 1.3.4, Table 1 p. 78): the −case strategy stops at obliques and a genitive requires a retained pronoun.

theorem KeenanComrie1977.finnish_plus_case_is_primary : { placement := Relativization.Placement.preNominal, caseCoding := false }.positions finnish ⊂ { placement := Relativization.Placement.postNominal, caseCoding := true }.positions finnish ∧ { placement := Relativization.Placement.preNominal, caseCoding := false }.IsPrimary finnish ∧ { placement := Relativization.Placement.postNominal, caseCoding := true }.IsPrimary finnish

Finnish (Section 1.3.2): the case-coding strategy of joka is the broader one, the participle covering subject and direct object only, both primary.

Pronoun retention (Section 2.2.2)

def KeenanComrie1977.IsPronoun (x : Relativization.NPRel) : Prop

A personal pronoun at the relativized position; pronouns of verb agreement are excluded (p. 92).

Equations

• KeenanComrie1977.IsPronoun x = (x = Relativization.NPRel.resumptive ∨ x = Relativization.NPRel.resumptiveMovement ∨ x = Relativization.NPRel.resumptiveBound)

@[instance_reducible]

instance KeenanComrie1977.instDecidablePredNPRelIsPronoun : DecidablePred IsPronoun

Equations

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

def KeenanComrie1977.relativizable (L : List Relativizer) : Finset Relativization.Position

The positions a language relativizes.

Equations

• KeenanComrie1977.relativizable L = {p : Relativization.Position | ∃ r ∈ L, (r.realize p).Nonempty}

def KeenanComrie1977.retention (L : List Relativizer) : Finset Relativization.Position

The positions at which a language retains a pronoun, its row of Table 2 (p. 93).

Equations

• KeenanComrie1977.retention L = {p : Relativization.Position | ∃ r ∈ L, ∃ x ∈ r.realize p, KeenanComrie1977.IsPronoun x}

def KeenanComrie1977.RetainsDownward (L : List Relativizer) : Prop

"Once a language begins to retain pronouns it must do so for as long as relativization is possible at all" (p. 92).

Equations

• KeenanComrie1977.RetainsDownward L = ∀ p ∈ KeenanComrie1977.retention L, ∀ q ∈ KeenanComrie1977.relativizable L, q ≤ p → q ∈ KeenanComrie1977.retention L

@[instance_reducible]

instance KeenanComrie1977.instDecidableRetainsDownward (L : List Relativizer) : Decidable (RetainsDownward L)

Equations

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

theorem KeenanComrie1977.arabic_table2 : retention arabic = {⊤}ᶜ

Table 2's Arabic (p. 93): pronouns are retained everywhere but the subject.

theorem KeenanComrie1977.retention_verified (L : List Relativizer) : L ∈ sample → RetainsDownward L

Every language of the sample retains pronouns downward.