Domain-Relativized Contiguity

[Mos15b] [Mos15a] [SMX+19]

A domain partition assigns each grade of a containment hierarchy a domain tag — abstractly representing the grade's locality unit (spellout domain / phase / accessibility domain). Within a domain, the *ABA contiguity constraint applies; across domain boundaries, ABA-shaped recurrences are admitted.

Motivation

Morphology.Containment.realize_const_of_terminal_adjacent (the structural-adjacency derivation, [Bob12]) predicts CMPR-cell = SPRL-cell for any generable root pattern. Lifted to case (Wardaman 3SG: ABS=narnaj, ERG=narnaj-(j)i, DAT=gunga; [SMX+19] §3.6) and number (Yagua 2: SG=jiy, PL=jiryéy, DL=sááda; [SMX+19] §4.2 Table 46), the prediction is empirically falsified — AAB patterns are attested in both case and number suppletion.

[SMX+19] §3.7 attribute the gap to locality: structural adjacency ([Bob12]) and linear adjacency ([embick-2010]) are too strict once AAB is admitted (Tamil dative suppletion across the plural morpheme is "neither linearly nor structurally adjacent to the root"). They adopt the [Mos15b] theory of accessibility domains (AD): a category-defining node has a delimiting effect that puts more-distant material outside the AD of the root, blocking it from conditioning suppletion. Lexical material has such a node (so case cannot reach the root); pronouns lack it (so case and number can both condition pronominal suppletion).

What this substrate models, and what it doesn't

This file represents the output of an AD computation projected onto the grades of a hierarchy: a DomainPartition saying, for each grade, which locality unit it belongs to. The AD theory itself is trigger-relative — a bound on which heads may condition root suppletion, formalized at rule level as SmithMoskalEtAl2019.DomainLocal on Morphology.Containment.ExponenceRule vocabularies. The substrate is theory-neutral about how the partition is computed: [Mos15b]'s AD is one source, [embick-2010]'s linear adjacency another (every grade its own one-cell domain), [Bob12]'s structural adjacency a third. Consumers state which projection they want; the substrate doesn't pick.

Main declarations

• DomainPartition n Tag — domain tag per grade
• ViolatesABAWithin, IsContiguousWithin — *ABA relativized to same-domain triples, over Morphology.Containment.Pattern
• isContiguousWithin_trivial_iff — under the trivial partition this is exactly Morphology.Containment.IsContiguous

@[reducible, inline]

abbrev Morphology.DomainLocality.DomainPartition (n : ℕ) (Tag : Type u_3) : Type u_3

A domain partition assigns each grade of an n-grade hierarchy a domain tag. Polymorphic over the tag type so consumers can use whatever tag type their analysis demands.

Equations

• Morphology.DomainLocality.DomainPartition n Tag = (Fin n → Tag)

@[reducible, inline]

abbrev Morphology.DomainLocality.SameDomain {n : ℕ} {Tag : Type u_1} (π : DomainPartition n Tag) (i j : Fin n) : Prop

Two grades lie in the same domain.

Equations

• Morphology.DomainLocality.SameDomain π i j = (π i = π j)

@[implicit_reducible]

instance Morphology.DomainLocality.instDecidableSameDomainOfDecidableEq {n : ℕ} {Tag : Type u_1} [DecidableEq Tag] (π : DomainPartition n Tag) (i j : Fin n) : Decidable (SameDomain π i j)

Equations

• Morphology.DomainLocality.instDecidableSameDomainOfDecidableEq π i j = inst✝ (π i) (π j)

@[reducible, inline]

abbrev Morphology.DomainLocality.DomainPartition.trivial (n : ℕ) : DomainPartition n Unit

The trivial partition: every grade in one domain.

Equations

• Morphology.DomainLocality.DomainPartition.trivial n x✝ = ()

def Morphology.DomainLocality.ViolatesABAWithin {n : ℕ} {Tag : Type u_1} {F : Type u_2} (π : DomainPartition n Tag) (p : Containment.Pattern n F) : Prop

A pattern violates the domain-relativized *ABA constraint: some form recurs across a distinct intervening form, with all three grades in the same domain.

Equations

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

@[implicit_reducible]

instance Morphology.DomainLocality.instDecidableViolatesABAWithinOfDecidableEq {n : ℕ} {Tag : Type u_1} {F : Type u_2} [DecidableEq Tag] [DecidableEq F] (π : DomainPartition n Tag) (p : Containment.Pattern n F) : Decidable (ViolatesABAWithin π p)

Equations

• Morphology.DomainLocality.instDecidableViolatesABAWithinOfDecidableEq π p = id inferInstance

def Morphology.DomainLocality.IsContiguousWithin {n : ℕ} {Tag : Type u_1} {F : Type u_2} (π : DomainPartition n Tag) (p : Containment.Pattern n F) : Prop

Domain-relativized contiguity: no within-domain *ABA violation.

Equations

• Morphology.DomainLocality.IsContiguousWithin π p = ¬Morphology.DomainLocality.ViolatesABAWithin π p

@[implicit_reducible]

instance Morphology.DomainLocality.instDecidableIsContiguousWithinOfDecidableEq {n : ℕ} {Tag : Type u_1} {F : Type u_2} [DecidableEq Tag] [DecidableEq F] (π : DomainPartition n Tag) (p : Containment.Pattern n F) : Decidable (IsContiguousWithin π p)

Equations

• Morphology.DomainLocality.instDecidableIsContiguousWithinOfDecidableEq π p = Morphology.DomainLocality.instDecidableIsContiguousWithinOfDecidableEq._aux_1 π p

theorem Morphology.DomainLocality.isContiguousWithin_trivial_iff {n : ℕ} {F : Type u_2} (p : Containment.Pattern n F) : IsContiguousWithin (DomainPartition.trivial n) p ↔ Containment.IsContiguous p

Under the trivial partition, domain-relativized contiguity is exactly the universal contiguity predicate.

Smoke tests

Trivial-partition behavior matches the universal predicate; across-domain examples show ABA-shapes are admitted when the outer grades fall in different domains.