Domain-Relativized Contiguity #
@cite{moskal-2015a-dissertation} @cite{moskal-2015} @cite{smith-moskal-xu-kang-bobaljik-2019}
A domain partition assigns each cell position in a paradigm to a domain tag — abstractly representing the cell's locality unit (spellout domain / phase / accessibility domain etc.). Within a domain, the *ABA contiguity constraint applies; across domain boundaries, AAB patterns are admitted.
Motivation #
Theories.Morphology.DM.ContainmentVI.Degree.vi_cmpr_eq_sprl (the DM
derivation, @cite{bobaljik-2012}) predicts CMPR-cell = SPRL-cell for
any VI-generable root pattern. Lifted to case (Wardaman 3SG: ABS=
narnaj, ERG=narnaj-(j)i, DAT=gunga; @cite{smith-moskal-xu-kang-bobaljik-2019}
§3.6) and number (Yagua 2: SG=jiy, PL=jiry-éy, DL=sáada;
@cite{smith-moskal-xu-kang-bobaljik-2019} §4.2 Table 46), the
prediction is empirically falsified — AAB patterns are attested in
both case and number suppletion.
@cite{smith-moskal-xu-kang-bobaljik-2019} §3.7 attribute the gap to locality: structural-adjacency (@cite{bobaljik-2012}) and linear- adjacency (@cite{embick-2010}) are too restrictive once AAB is admitted. They endorse the @cite{moskal-2015a-dissertation} 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 can't 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 cell positions: a function Nat → Tag that says, for each cell,
which locality unit it belongs to. The trigger-relative AD theory
(@cite{moskal-2015a-dissertation}: "the first category-defining node
above the root, and one node above that") is more nuanced — it's a
relation between a trigger node and a root node in a tree, not a
labeling of paradigm cells.
The substrate is theory-neutral about how the partition is computed. @cite{moskal-2015a-dissertation}'s AD is one source. @cite{embick-2010}'s linear adjacency is another (every position in its own one-cell domain). @cite{bobaljik-2012}'s structural adjacency is a third. @cite{caha-2009}'s Nanosyntax doesn't fit a domain-partition shape at all — it derives AAB exclusion (or non-exclusion) from phrasal spellout + the Superset Principle, not from locality. Consumers state which projection they want; the substrate doesn't pick.
Design #
ViolatesABAWithin π cells is the Prop predicate "there exist
positions i < j < k in cells.length, all in the same domain under
π, such that cells[i] = cells[k] ≠ cells[j]." Decidability comes
free via Fintype (Fin n) — no Bool-first decision procedure needed.
Why not import Theories/Syntax/Minimalist/Phase.lean? #
Phase.lean operates on SyntacticObject trees with isPhaseHeadOf.
The morphological "domain" is more abstract — it lives at the level
of cell-position projections of paradigm tables, with no syntactic-
tree commitment. A future cross-layer connection (showing that
syntactic phases project to morphological domains under a
DM-with-phase analysis) can be added in Theories/Morphology/ once
a consumer requests it.
A domain partition assigns each cell position to a domain tag. Polymorphic over the tag type so callers (Bobaljik2012, SmithMoskal, Caha …) can use whatever tag type their analysis demands.
abbrev so π i reduces through the type alias — needed by
decide on concrete partitions.
Equations
- Morphology.DomainLocality.DomainPartition Tag = (ℕ → Tag)
Instances For
Two cell positions lie in the same domain. abbrev for the same
decide-reduction reason.
Equations
- Morphology.DomainLocality.SameDomain π i j = (π i = π j)
Instances For
Equations
- Morphology.DomainLocality.instDecidableSameDomain π i j = inst✝ (π i) (π j)
The trivial partition: every position in one domain (Unit tag).
Equations
Instances For
A list violates the domain-relativized *ABA constraint when there exist three positions i < j < k (within the list's length), all in the same domain under π, such that the cells at i and k share a value distinct from the cell at j.
Bounded by Finset.range cells.length so decidability composes
cleanly via Finset.decidableBExists. cells[·]? (returning
Option Nat) is the cell accessor; Option Nat has
DecidableEq. Direct propositional content, no Bool wrapper.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Domain-relativized contiguity: no within-domain *ABA violation.
Equations
Instances For
Under the trivial partition, every same-domain check trivially
holds, so ViolatesABAWithin reduces to the unconstrained
*ABA-pattern existential.
Trivial-partition behavior: same shape as the universal predicate. Across-domain examples illustrate that AAB *ABA-shapes are admitted when the inner cell is in a different domain than the outer cells.