Documentation

Linglib.Core.Morphology.Containment

Generic Containment and the *ABA Pattern #

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

Overview #

A widely-discussed cross-linguistic generalization across several domains of inflectional morphology: when a list of form-class indices along an ordered hierarchy of paradigm positions is read off a suppletion pattern, the configuration A–B–A — outer positions sharing a form that the intervening position lacks — is systematically unattested. Contiguity (A–A–B, A–B–B, A–B–C) is the modal pattern.

This module supplies framework-neutral substrate: a contiguity predicate over List Nat (a list of form-class indices), with both a computable Bool decision procedure and a Prop wrapper carrying a Decidable instance. Domain-specific instantiations live elsewhere:

What explains the gap is theory-laden and contested. The DM tradition (@cite{bobaljik-2012}) derives it from post-syntactic Vocabulary Insertion + Elsewhere ordering on a containment hierarchy. The Nanosyntax tradition (@cite{caha-2009}, @cite{starke-2009}) derives it from phrasal spellout + the Superset Principle on the same containment hierarchy interpreted as syntactic structure. The two disagree on whether the locus of explanation is morphology or syntax; this module takes no position.

source
def Morphology.Containment.violatesABA :
List Nat → Bool

Does a list of form-class indices contain an ABA violation? An ABA violation occurs at positions i < j < k when pattern[i] = pattern[k] ≠ pattern[j] — the same form class appears at two non-adjacent positions while the intervening position has a different form.

Works for any hierarchy length: 3-position (degree), 4-position (case), or longer.

Equations
Instances For
    source
    def Morphology.Containment.isContiguous (pattern : List Nat) :
    Bool

    Is a pattern contiguous (Bool)? Each form class occupies a contiguous span of positions on the hierarchy. Equivalent to ¬violatesABA.

    Equations
    Instances For
      source
      def Morphology.Containment.ViolatesABA (l : List Nat) :
      Prop

      A list violates the *ABA pattern (Prop). Bridge to the Bool decision procedure; downstream files that prefer Prop+Decidable over = true boilerplate use this.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Morphology.Containment.instDecidableViolatesABA (l : List Nat) :
        Decidable (ViolatesABA l)
        Equations
        source
        def Morphology.Containment.IsContiguous (l : List Nat) :
        Prop

        A list is contiguous (Prop).

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Morphology.Containment.instDecidableIsContiguous (l : List Nat) :
          Decidable (IsContiguous l)
          Equations
          source
          theorem Morphology.Containment.isContiguous_iff_not_violatesABA (l : List Nat) :
          isContiguous l = true ↔ ¬ViolatesABA l

          The Bool and Prop forms of contiguity agree.

          source
          theorem Morphology.Containment.violatesABA_three (a b c : Nat) :
          violatesABA [a, b, c] = (a == c && a != b)

          *ABA on a 3-position hierarchy (degree: POS, CMPR, SPRL). The only possible violation is positions (0,1,2): a = c ∧ a ≠ b.

          source
          theorem Morphology.Containment.violatesABA_four (a b c d : Nat) :
          violatesABA [a, b, c, d] = (a == c && a != b || a == d && a != b || a == d && a != c || b == d && b != c)

          *ABA on a 4-position hierarchy (case: NOM, ACC, GEN, DAT). Four possible triples: (0,1,2), (0,1,3), (0,2,3), (1,2,3).

          Smoke tests: every cell-pattern shape this substrate's downstream consumers care about resolves correctly under the predicates above. These are examples rather than named theorems because nothing in the codebase references them by name; the named-theorem shape would pollute the public API surface of Morphology.Containment.