Keenan & Comrie (1977) @cite{keenan-comrie-1977}

Noun Phrase Accessibility and Universal Grammar. Linguistic Inquiry 8(1): 63–99.

Formalizes the three Hierarchy Constraints (HCs) and the derived Primary Relativization Constraint (PRC) from @cite{keenan-comrie-1977}, verified against a subset of the paper's Table 1 data.

Hierarchy Constraints

The paper proposes three constraints on how languages form relative clauses, building on the Accessibility Hierarchy (AH):

SU > DO > IO > OBL > GEN > OCOMP

• HC₁: A language must be able to relativize subjects.
• HC₂ (Continuity): Any RC-forming strategy must apply to a continuous segment of the AH.
• HC₃ (Cut-off): Strategies that apply at one point may cease at any lower point.

From HC₁ + HC₂, the Primary Relativization Constraint follows: if a language's primary strategy (one that covers subjects) can apply to a low position N, it can apply to all positions above N. Non-primary strategies need not satisfy this — they may cover a continuous segment that excludes subjects (e.g., the +case strategy covering IO–OCOMP but not SU–DO in Welsh and Arabic).

Multi-Strategy Profiles

The paper's key empirical contribution is showing that languages typically have multiple relativization strategies, each covering a different contiguous segment of the AH. The ±case distinction (whether the relative element bears case marking) is the primary parameter distinguishing strategies.

Data

Table 1 profiles are derived from fragment data — each language's RelClauseMarker list (encoding actual linguistic markers: particles, pronouns, verbal suffixes) is converted to StrategyEntry records. This ensures the study file stays consistent with the fragment layer by construction. We cover the key patterns: gap-to-resumptive split (Welsh, Hebrew, Arabic, Toba Batak), multi-strategy with prenominal RCs (Korean, Finnish), and single-strategy (Malagasy).

structure Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry : Type

A single relativization strategy from @cite{keenan-comrie-1977} Table 1.

Each language has one or more strategies. A strategy is characterized by the position of the RC (pre/post-nominal), whether the relative element bears case marking (±case), and which AH positions it covers.

• rcPosition : Core.RCPosition

  Position of relative clause with respect to head noun

• plusCase : Bool

  +case: the relative element (pronoun, relative pronoun) bears case marking for its role inside the RC. -case: no case-marked element in NP_rel (gap/deletion).

• su : Bool
• do_ : Bool
• io : Bool
• obl : Bool
• gen : Bool
• ocomp : Bool

instance Phenomena.FillerGap.Studies.KeenanComrie1977.instDecidableEqStrategyEntry : DecidableEq StrategyEntry

Equations

• Phenomena.FillerGap.Studies.KeenanComrie1977.instDecidableEqStrategyEntry = Phenomena.FillerGap.Studies.KeenanComrie1977.instDecidableEqStrategyEntry.decEq

def Phenomena.FillerGap.Studies.KeenanComrie1977.instDecidableEqStrategyEntry.decEq (x✝ x✝¹ : StrategyEntry) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.FillerGap.Studies.KeenanComrie1977.instBEqStrategyEntry : BEq StrategyEntry

Equations

• Phenomena.FillerGap.Studies.KeenanComrie1977.instBEqStrategyEntry = { beq := Phenomena.FillerGap.Studies.KeenanComrie1977.instBEqStrategyEntry.beq }

def Phenomena.FillerGap.Studies.KeenanComrie1977.instBEqStrategyEntry.beq : StrategyEntry → StrategyEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.FillerGap.Studies.KeenanComrie1977.instBEqStrategyEntry.beq x✝¹ x✝ = false

instance Phenomena.FillerGap.Studies.KeenanComrie1977.instReprStrategyEntry : Repr StrategyEntry

Equations

• Phenomena.FillerGap.Studies.KeenanComrie1977.instReprStrategyEntry = { reprPrec := Phenomena.FillerGap.Studies.KeenanComrie1977.instReprStrategyEntry.repr }

def Phenomena.FillerGap.Studies.KeenanComrie1977.instReprStrategyEntry.repr : StrategyEntry → Nat → Std.Format

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry.covers (s : StrategyEntry) : Core.AHPosition → Bool

Which AH position does this strategy cover?

Equations

• s.covers Core.AHPosition.subject = s.su
• s.covers Core.AHPosition.directObject = s.do_
• s.covers Core.AHPosition.indirectObject = s.io
• s.covers Core.AHPosition.oblique = s.obl
• s.covers Core.AHPosition.genitive = s.gen
• s.covers Core.AHPosition.objComparison = s.ocomp

def Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry.coveredPositions (s : StrategyEntry) : List Core.AHPosition

List of AH positions covered by this strategy.

Equations

• s.coveredPositions = List.filter s.covers Core.AHPosition.all

def Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry.isPrimary (s : StrategyEntry) : Bool

Is this a primary strategy? Primary strategies cover subjects. HC₁ requires at least one primary strategy per language.

Equations

• s.isPrimary = s.su

def Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry.isContinuous (s : StrategyEntry) : Bool

HC₂: Does this strategy cover a contiguous segment of the AH? Uses contiguousOnAH from Core.Relativization.Hierarchy, which mirrors the contiguity check in Core.Case.Hierarchy.validInventory.

Equations

• s.isContinuous = Core.contiguousOnAH s.coveredPositions

def Phenomena.FillerGap.Studies.KeenanComrie1977.RelClauseMarker.toStrategyEntry (m : Core.RelClauseMarker) : StrategyEntry

Convert a fragment's RelClauseMarker to a Table 1 StrategyEntry. The marker's bearsCaseMarking maps to ±case, and its positions list determines per-position coverage.

Equations

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

structure Phenomena.FillerGap.Studies.KeenanComrie1977.KCProfile : Type

A language's full relativization profile from Table 1. Each language has one or more strategies covering (potentially overlapping) segments of the AH.

• language : String
• strategies : List StrategyEntry
• notes : String

def Phenomena.FillerGap.Studies.KeenanComrie1977.instReprKCProfile.repr : KCProfile → Nat → Std.Format

Equations

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

instance Phenomena.FillerGap.Studies.KeenanComrie1977.instReprKCProfile : Repr KCProfile

Equations

• Phenomena.FillerGap.Studies.KeenanComrie1977.instReprKCProfile = { reprPrec := Phenomena.FillerGap.Studies.KeenanComrie1977.instReprKCProfile.repr }

def Phenomena.FillerGap.Studies.KeenanComrie1977.KCProfile.satisfiesHC1 (p : KCProfile) : Bool

HC₁: The language can relativize subjects (at least one strategy covers SU).

Equations

• p.satisfiesHC1 = p.strategies.any fun (x : Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry) => x.su

def Phenomena.FillerGap.Studies.KeenanComrie1977.KCProfile.satisfiesHC2 (p : KCProfile) : Bool

HC₂: Every strategy covers a contiguous segment of the AH.

Equations

• p.satisfiesHC2 = p.strategies.all fun (x : Phenomena.FillerGap.Studies.KeenanComrie1977.StrategyEntry) => x.isContinuous

def Phenomena.FillerGap.Studies.KeenanComrie1977.KCProfile.satisfiesPRC (p : KCProfile) : Bool

PRC: Every primary strategy satisfies upward closure — if it covers position N, it covers all positions above N. This follows from HC₂ (contiguity) + isPrimary (covers SU at rank 6): a contiguous segment containing rank 6 and rank N must contain all intermediate ranks.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.mkProfile (name : String) (markers : List Core.RelClauseMarker) (notes : String := "") : KCProfile

Build a KCProfile from a language name and its fragment marker list.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.english : KCProfile

English: two strategies derived from Fragments.English.relMarkers. -case: complementizer that/∅, gap, covers SU/DO. +case: relative pronoun who/whom/which/whose, covers IO–OCOMP.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.welsh : KCProfile

Welsh: two strategies derived from Fragments.Welsh.relMarkers (§1.3.2). -case: particle a, gap, covers SU/DO. +case: particle y, resumptive pronoun, covers IO–OCOMP.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.arabic : KCProfile

Arabic: two strategies derived from Fragments.Arabic.relMarkers (§1.3.2). -case: alladhi, gap, covers SU only. +case: resumptive pronoun, covers DO–OCOMP.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.hebrew : KCProfile

Hebrew: two strategies derived from Fragments.Hebrew.relMarkers (§1.3.2). -case: complementizer she-, gap, covers SU/DO. +case: she- + resumptive pronoun, covers DO–OCOMP. DO is shared between both strategies.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.tobaBatak : KCProfile

Toba Batak: two strategies derived from Fragments.TobaBatak.relMarkers (§1.3.2). -case: gap, covers SU only. +case: resumptive pronoun, covers IO/OBL/GEN. DO cannot be relativized by either strategy — a genuine gap.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.korean : KCProfile

Korean: two strategies derived from Fragments.Korean.relMarkers. -case: adnominal suffix -(n)ɨn, -n, -l, gap, covers SU–OBL. +case: genitive marker -uy, covers GEN only.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.finnish : KCProfile

Finnish: two strategies derived from Fragments.Finnish.relMarkers. +case: relative pronoun joka (declines for case), covers SU–GEN. -case: prenominal participial, covers SU/DO. OCOMP does not exist as a distinct category in Finnish.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.malagasy : KCProfile

Malagasy: one strategy derived from Fragments.Malagasy.relMarkers. -case: gap, covers SU only. Voice alternation required for non-subject relativization.

Equations

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

def Phenomena.FillerGap.Studies.KeenanComrie1977.allProfiles : List KCProfile

All Table 1 profiles in our sample.

Equations

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

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.hc1_verified : (allProfiles.all fun (x : KCProfile) => x.satisfiesHC1) = true

HC₁ holds: every language in our sample can relativize subjects.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.hc2_verified : (allProfiles.all fun (x : KCProfile) => x.satisfiesHC2) = true

HC₂ holds: every strategy covers a contiguous segment of the AH.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.prc_verified : (allProfiles.all fun (x : KCProfile) => x.satisfiesPRC) = true

PRC holds: every primary strategy satisfies upward closure.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.prc_follows_from_hc2_and_primary : (allProfiles.all fun (p : KCProfile) => p.strategies.all fun (s : StrategyEntry) => if (s.isPrimary && s.isContinuous) = true then Core.AHPosition.all.all fun (pos : Core.AHPosition) => if s.covers pos = true then Core.AHPosition.all.all fun (above : Core.AHPosition) => if above.rank > pos.rank then s.covers above else true else true else true) = true

The PRC follows from HC₂ for primary strategies: if a strategy is continuous and covers subjects (rank 6), then for any covered position at rank N, all positions with rank > N are also covered.

We verify this structural implication on all strategies in our sample: isPrimary ∧ isContinuous → upward-closed.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.every_language_has_primary : (allProfiles.all fun (p : KCProfile) => p.strategies.any fun (x : StrategyEntry) => x.isPrimary) = true

Every language has at least one primary strategy (restates HC₁ in terms of the StrategyEntry.isPrimary predicate).

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.minus_case_covers_subjects : (allProfiles.all fun (p : KCProfile) => p.strategies.all fun (s : StrategyEntry) => if (!s.plusCase) = true then s.su else true) = true

In our sample, every -case strategy covers subjects. The -case (gap/deletion) strategy is always primary when present.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.most_have_multiple_strategies : (List.filter (fun (p : KCProfile) => decide (p.strategies.length > 1)) allProfiles).length ≥ 5

Multi-strategy languages: most languages in our sample use more than one strategy, with strategies covering different segments.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.plus_case_secondary_excludes_su : (allProfiles.all fun (p : KCProfile) => p.strategies.all fun (s : StrategyEntry) => if (s.plusCase && !s.isPrimary) = true then !s.su else true) = true

+case strategies that are non-primary (don't cover SU) never cover SU in our sample. This reflects the typological generalization that pronoun retention is used for lower, not higher, AH positions.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.gap_covers_higher_than_resumptive : (allProfiles.all fun (p : KCProfile) => p.strategies.all fun (s : StrategyEntry) => (if (!s.plusCase) = true then s.su else true) && if (s.plusCase && !s.isPrimary) = true then !s.su else true) = true

The gap-to-resumptive split: -case strategies always cover subjects, while +case secondary strategies never do. This means -case always occupies a strictly higher segment of the AH than non-primary +case.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.toba_batak_do_gap : (tobaBatak.strategies.all fun (s : StrategyEntry) => !s.do_) = true

Toba Batak has a genuine gap at DO: neither strategy can relativize direct objects. This is consistent with the HCs because each individual strategy is contiguous — the gap exists between strategies, not within one. The paper notes this explicitly.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.toba_batak_hc2 : tobaBatak.satisfiesHC2 = true

Despite the DO gap, both of Toba Batak's individual strategies are contiguous (SU alone; IO–GEN alone). HC₂ is satisfied.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.english_full_coverage : List.map (fun (x : StrategyEntry) => x.coveredPositions.length) english.strategies = [2, 4]

English covers all 6 AH positions across two strategies: -case (that/∅) covers SU/DO (2), +case (who/whom) covers IO–OCOMP (4).

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.welsh_strategy_split : have s := welsh.strategies; s.length = 2 ∧ List.map (fun (x : StrategyEntry) => x.su) s = [true, false] ∧ List.map (fun (x : StrategyEntry) => x.do_) s = [true, false] ∧ List.map (fun (x : StrategyEntry) => x.io) s = [false, true] ∧ List.map (fun (x : StrategyEntry) => x.ocomp) s = [false, true]

Welsh splits at the DO/IO boundary: -case covers SU–DO, +case covers IO–OCOMP. Verified by checking coverage of each strategy.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.arabic_primary_su_only : have s := arabic.strategies; List.map (fun (x : StrategyEntry) => x.su) s = [true, false] ∧ List.map (fun (x : StrategyEntry) => x.do_) s = [false, true]

Arabic (Classical): -case covers SU only.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.malagasy_su_only : malagasy.strategies.length = 1 ∧ List.map (fun (x : StrategyEntry) => x.su) malagasy.strategies = [true] ∧ List.map (fun (x : StrategyEntry) => x.do_) malagasy.strategies = [false]

Malagasy: single strategy, subject only.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.korean_primary_su_to_obl : have s := korean.strategies; List.map (fun (x : StrategyEntry) => x.su) s = [true, false] ∧ List.map (fun (x : StrategyEntry) => x.obl) s = [true, false] ∧ List.map (fun (x : StrategyEntry) => x.gen) s = [false, true]

Korean: -case strategy covers SU–OBL but not GEN.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.finnish_plus_case_is_primary : have s := finnish.strategies; List.map (fun (x : StrategyEntry) => x.plusCase) s = [true, false] ∧ List.map (fun (x : StrategyEntry) => x.isPrimary) s = [true, true]

Finnish: +case strategy is primary (covers SU) despite being +case. Finnish is an example where the +case strategy is the broader one.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.welsh_covers_ocomp_via_plus_case : ((List.filter (fun (x : StrategyEntry) => x.plusCase) welsh.strategies).any fun (x : StrategyEntry) => x.ocomp) = true

Cross-reference: the Welsh WALS profile in Typology.lean records lowestRelativizable := .oblique, but Table 1 shows the +case strategy covers all the way to OCOMP. The discrepancy reflects that WALS and Table 1 use different data sources and granularity — WALS Ch 123 only asks about obliques, not the full AH.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.sample_size : allProfiles.length = 8

Sample size: 8 languages from Table 1.

def Phenomena.FillerGap.Studies.KeenanComrie1977.KCProfile.lowestCovered (p : KCProfile) : Core.AHPosition

Lowest AH position covered by any strategy in a KCProfile. Returns the position with the smallest rank that is covered by at least one strategy. Returns .subject if nothing else matches.

Equations

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

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.english_kc_matches_wals : english.lowestCovered = Core.AHPosition.objComparison ∧ Typology.english.lowestRelativizable = Core.AHPosition.objComparison

English: KCProfile covers all 6 positions (lowestCovered = OCOMP), matching Typology.english.lowestRelativizable = .objComparison.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.welsh_kc_covers_deeper_than_wals : welsh.lowestCovered = Core.AHPosition.objComparison ∧ Typology.welsh.lowestRelativizable = Core.AHPosition.oblique ∧ Core.AHPosition.oblique.moreAccessible Core.AHPosition.objComparison = true

Welsh: KCProfile covers down to OCOMP (via +case strategy), though WALS records .oblique (Ch 123 only asks about obliques).

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.korean_kc_covers_deeper_than_wals : korean.lowestCovered = Core.AHPosition.genitive ∧ Typology.korean.lowestRelativizable = Core.AHPosition.oblique

Korean: KCProfile covers SU-OBL + GEN, lowest = GEN. WALS records .oblique (doesn't track GEN).

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.malagasy_kc_matches_wals : malagasy.lowestCovered = Core.AHPosition.subject ∧ Typology.malagasy.lowestRelativizable = Core.AHPosition.subject

Malagasy: both systems agree — subjects only.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.finnish_kc_matches_wals : finnish.lowestCovered = Core.AHPosition.genitive ∧ Typology.finnish.lowestRelativizable = Core.AHPosition.oblique

Finnish: KCProfile covers SU-GEN (via joka), WALS records .oblique. Both agree that Finnish covers at least obliques.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.hebrew_kc_covers_deeper_than_wals : hebrew.lowestCovered = Core.AHPosition.objComparison ∧ Typology.hebrew.lowestRelativizable = Core.AHPosition.oblique

Hebrew: KCProfile covers all positions via +case (DO-OCOMP). WALS records .oblique.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.arabic_kc_covers_deeper_than_wals : arabic.lowestCovered = Core.AHPosition.objComparison ∧ Typology.arabic.lowestRelativizable = Core.AHPosition.oblique

Arabic: KCProfile covers all positions (SU via gap, DO-OCOMP via resumptive). WALS records .oblique.

theorem Phenomena.FillerGap.Studies.KeenanComrie1977.kc_at_least_as_detailed_as_wals : english.lowestCovered.rank ≤ Typology.english.lowestRelativizable.rank ∧ welsh.lowestCovered.rank ≤ Typology.welsh.lowestRelativizable.rank ∧ korean.lowestCovered.rank ≤ Typology.korean.lowestRelativizable.rank ∧ malagasy.lowestCovered.rank ≤ Typology.malagasy.lowestRelativizable.rank ∧ finnish.lowestCovered.rank ≤ Typology.finnish.lowestRelativizable.rank ∧ hebrew.lowestCovered.rank ≤ Typology.hebrew.lowestRelativizable.rank ∧ arabic.lowestCovered.rank ≤ Typology.arabic.lowestRelativizable.rank

Systematic coverage agreement: for every language in our sample that also appears in the WALS typology, the KCProfile covers at least as much as the WALS profile indicates. The WALS profile never claims a language can relativize a position that Table 1 doesn't cover — Table 1 is strictly more detailed.