Case Containment and the *ABA Constraint

@cite{caha-2009} @cite{mcfadden-2018} @cite{bobaljik-2012}

Containment

@cite{caha-2009} proposes that the morphosyntactic representation of each case on the hierarchy literally contains the representations of all cases below it:

[[[[[ NOM ] ACC ] GEN ] DAT ] P ]

This means ACC's representation includes NOM's; GEN's includes both ACC's and NOM's; etc. A Vocabulary Insertion rule conditioned on feature F therefore matches every case whose representation contains F. A rule conditioned on ACC matches ACC, GEN, DAT, and P — the set of all nonnominative cases — explaining the widespread NOM vs. oblique split in stem allomorphy (@cite{mcfadden-2018}).

The *ABA Constraint

@cite{bobaljik-2012} and @cite{caha-2009} observe that case-conditioned suppletion obeys a contiguity restriction: if two cases X and Z (with X ⊂ Y ⊂ Z on the hierarchy) share a suppletive form A, then the case Y between them must also have form A. The pattern A–B–A (with B ≠ A) is systematically unattested. This is the *ABA constraint.

The constraint falls out from containment: if a VI rule inserts form B in the context of feature F, and Y's representation contains F, then so does Z's (since Z ⊃ Y ⊃ X). There is no way for Z to "skip" B and revert to A.

Connection to Blake

Core.Case.Hierarchy formalizes Blake's typological hierarchy — an implicational tendency about which cases languages tend to have. Caha's containment hierarchy is a different object: a syntactic claim about the internal structure of case representations. The two are complementary, not competing.

def Core.Case.containmentRank : Case → Option Nat

Caha's containment rank (@cite{caha-2009}). Cases higher on the containment hierarchy have representations that include all lower cases.

[[[[[ NOM ] ACC ] GEN ] DAT ] P ]

The P(ostpositional) layer includes LOC and other spatial cases whose representations contain the full case spine.

Returns none for cases not on the containment hierarchy (e.g., ERG/ABS in ergative systems, or minor cases whose containment structure is less well established).

Equations

• Core.Case.nom.containmentRank = some 0
• Core.Case.acc.containmentRank = some 1
• Core.Case.gen.containmentRank = some 2
• Core.Case.dat.containmentRank = some 3
• Core.Case.loc.containmentRank = some 4
• x✝.containmentRank = none

def Core.Case.containedIn (inner outer : Case) : Bool

Does case inner have a representation contained within case outer? True when inner.containmentRank ≤ outer.containmentRank.

Equations

• inner.containedIn outer = match inner.containmentRank, outer.containmentRank with | some ri, some ro => decide (ri ≤ ro) | x, x_1 => false

theorem Core.nom_contained_in_acc : Case.nom.containedIn Case.acc = true

NOM is contained in every case on the hierarchy.

theorem Core.nom_contained_in_gen : Case.nom.containedIn Case.gen = true

theorem Core.nom_contained_in_dat : Case.nom.containedIn Case.dat = true

theorem Core.nom_contained_in_loc : Case.nom.containedIn Case.loc = true

NOM is contained in LOC (postpositional layer).

theorem Core.acc_contained_in_gen : Case.acc.containedIn Case.gen = true

ACC is contained in GEN, DAT, and LOC but not NOM.

theorem Core.acc_contained_in_dat : Case.acc.containedIn Case.dat = true

theorem Core.acc_contained_in_loc : Case.acc.containedIn Case.loc = true

theorem Core.acc_not_in_nom : Case.acc.containedIn Case.nom = false

theorem Core.containment_reflexive (c : Case) (h : c.containmentRank.isSome = true) : c.containedIn c = true

Every case contains itself.

theorem Core.containment_transitive (a b c : Case) (hab : a.containedIn b = true) (hbc : b.containedIn c = true) : a.containedIn c = true

Containment is transitive.

def Core.Case.isNonnom (c : Case) : Bool

The set of nonnominative cases on the containment hierarchy: those whose representation contains ACC.

@cite{mcfadden-2018} argues this is the key natural class for stem allomorphy: a VI rule conditioned on [ACC] captures the NOM-vs-oblique split found cross-linguistically.

Equations

• c.isNonnom = Core.Case.acc.containedIn c

theorem Core.acc_is_nonnom : Case.acc.isNonnom = true

theorem Core.gen_is_nonnom : Case.gen.isNonnom = true

theorem Core.dat_is_nonnom : Case.dat.isNonnom = true

theorem Core.loc_is_nonnom : Case.loc.isNonnom = true

theorem Core.nom_not_nonnom : Case.nom.isNonnom = false

structure Core.AllomorphyPattern : Type

An allomorphy pattern over the four core cases (NOM, ACC, GEN, DAT), represented as a form-class index for each case.

• nom : Nat
• acc : Nat
• gen : Nat
• dat : Nat

instance Core.instDecidableEqAllomorphyPattern : DecidableEq AllomorphyPattern

Equations

• Core.instDecidableEqAllomorphyPattern = Core.instDecidableEqAllomorphyPattern.decEq

def Core.instDecidableEqAllomorphyPattern.decEq (x✝ x✝¹ : AllomorphyPattern) : Decidable (x✝ = x✝¹)

Equations

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

def Core.instBEqAllomorphyPattern.beq : AllomorphyPattern → AllomorphyPattern → Bool

Equations

• Core.instBEqAllomorphyPattern.beq { nom := a, acc := a_1, gen := a_2, dat := a_3 } { nom := b, acc := b_1, gen := b_2, dat := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• Core.instBEqAllomorphyPattern.beq x✝¹ x✝ = false

instance Core.instBEqAllomorphyPattern : BEq AllomorphyPattern

Equations

• Core.instBEqAllomorphyPattern = { beq := Core.instBEqAllomorphyPattern.beq }

def Core.instReprAllomorphyPattern.repr : AllomorphyPattern → Nat → Std.Format

Equations

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

instance Core.instReprAllomorphyPattern : Repr AllomorphyPattern

Equations

• Core.instReprAllomorphyPattern = { reprPrec := Core.instReprAllomorphyPattern.repr }

def Core.AllomorphyPattern.violatesABA (p : AllomorphyPattern) : Bool

Does a pattern contain an ABA subsequence? An ABA violation occurs when two non-adjacent cases on the containment hierarchy share a form that the intervening case does not.

We check all triples (i, j, k) where i < j < k on the hierarchy NOM(0) < ACC(1) < GEN(2) < DAT(3): if pattern(i) = pattern(k) ≠ pattern(j), the pattern is ABA.

Equations

• p.violatesABA = (p.nom == p.gen && p.nom != p.acc || p.nom == p.dat && p.nom != p.acc || p.nom == p.dat && p.nom != p.gen || p.acc == p.dat && p.acc != p.gen)

def Core.AllomorphyPattern.isContiguous (p : AllomorphyPattern) : Bool

Is a pattern contiguous? Each form class occupies a contiguous span on the containment hierarchy. Equivalent to ¬violatesABA.

Equations

• p.isContiguous = !p.violatesABA

def Core.abbPattern : AllomorphyPattern

ABB pattern (NOM vs oblique): the Telugu strong alternation. NOM gets form 0, all oblique cases get form 1. Contiguous.

Equations

• Core.abbPattern = { nom := 0, acc := 1, gen := 1, dat := 1 }

theorem Core.abb_contiguous : abbPattern.isContiguous = true

theorem Core.abb_no_aba : abbPattern.violatesABA = false

def Core.aabPattern : AllomorphyPattern

AAB pattern (core vs dative): contiguous.

Equations

• Core.aabPattern = { nom := 0, acc := 0, gen := 0, dat := 1 }

theorem Core.aab_contiguous : aabPattern.isContiguous = true

def Core.aabbPattern : AllomorphyPattern

AABB pattern: contiguous (NOM+ACC share form 0, GEN+DAT share form 1).

Equations

• Core.aabbPattern = { nom := 0, acc := 0, gen := 1, dat := 1 }

theorem Core.aabb_contiguous : aabbPattern.isContiguous = true

def Core.ababPattern : AllomorphyPattern

ABAB pattern: the Telugu weak alternation. NOM = short (0), ACC = long (1), GEN = short (0), DAT = long (1). Violates *ABA — this is the pattern @cite{aitha-2026} argues cannot be case-conditioned contextual allomorphy.

Equations

• Core.ababPattern = { nom := 0, acc := 1, gen := 0, dat := 1 }

theorem Core.abab_violates_aba : ababPattern.violatesABA = true

theorem Core.abab_not_contiguous : ababPattern.isContiguous = false

def Core.abaPattern : AllomorphyPattern

ABA pattern (NOM=GEN, ACC different): violates *ABA.

Equations

• Core.abaPattern = { nom := 0, acc := 1, gen := 0, dat := 0 }

theorem Core.aba_violates : abaPattern.violatesABA = true

def Core.babPattern : AllomorphyPattern

BAB pattern: violates *ABA.

Equations

• Core.babPattern = { nom := 1, acc := 0, gen := 1, dat := 0 }

theorem Core.bab_violates : babPattern.violatesABA = true

def Core.uniformPattern : AllomorphyPattern

Uniform pattern (all same form): trivially contiguous.

Equations

• Core.uniformPattern = { nom := 0, acc := 0, gen := 0, dat := 0 }

theorem Core.uniform_contiguous : uniformPattern.isContiguous = true

theorem Core.containment_refines_blake : Case.nom.hierarchyRank ≥ Case.acc.hierarchyRank ∧ Case.acc.hierarchyRank ≥ Case.gen.hierarchyRank ∧ Case.gen.hierarchyRank ≥ Case.dat.hierarchyRank

Containment rank preserves Blake's typological ordering on the core cases (NOM, ACC, GEN, DAT): the containment hierarchy is a refinement of the typological hierarchy's ordering on these cases.

Blake's hierarchy: NOM(6) > GEN(5) > DAT(4) > LOC(3) > ... Containment: NOM(0) < ACC(1) < GEN(2) < DAT(3)

The orderings are inverses on the shared cases: Blake ranks by "how likely a language is to have it" (NOM most common → highest), while containment ranks by "how much structure it contains" (NOM least complex → lowest).

For any two cases with containment ranks r₁ < r₂, their Blake ranks satisfy h₁ ≥ h₂ (weakly, since NOM and ACC share Blake rank 6).