Docs / Morphology / Exponence / Containment / Contiguity

Containment hierarchies: contiguity and the suppletion generalizations

import Linglib.Morphology.Exponence.Containment.Contiguity · namespace Morphology.Containment

This file proves the *ABA generalization and its refinements for the two realizational engines over a containment hierarchy. Over antihomophonous rule sets both engines realize contiguous patterns, since applicability is closed upward for rules of exponence and downward for lexical entries, and each engine generates every contiguous pattern, so Elsewhere insertion from terminal rule sets and Superset spellout generate the same fully realized patterns. Over the three-grade degree hierarchy, terminal adjacent rule sets realize the comparative and the superlative alike, grounded rule sets exclude AAB, and so do rule sets meeting the markedness condition with adjacent contexts, and a superlative root distinct from the comparative one needs a portmanteau.

Main definitions

ElsewhereGenerable, SupersetSpellable: the patterns each engine realizes in full.
GroundedGenerable: the patterns a grounded antihomophonous rule set realizes in full.

Main results

isContiguous_realize, isContiguous_spellout: *ABA for both engines.
isContiguous_iff_generable, isContiguous_iff_spelloutGenerable, spelloutGenerable_iff_generable: both engines generate exactly the contiguous patterns.
realize_const_of_terminal_adjacent, realize_const_of_grounded, realize_const_of_markedness, exists_portmanteau_of_ne: the AAA/ABB plateau, *AAB under grounding and under markedness with adjacency, and the portmanteau prediction.
groundedGenerable_iff: grounded rule sets generate exactly AAA, ABB and ABC.

References

Bobaljik 2012, Universals in comparative morphology: Suppletion, superlatives, and the structure of words formalized
Caha 2009, The Nanosyntax of Case formalized
De Clercq & Vanden Wyngaerd 2017, *ABA revisited: Evidence from Czech and Latin degree morphology

*ABA

Elsewhere insertion over an antihomophonous rule set is contiguous (Bobaljik 2012 ch. 2).

theorem isContiguous_realize L52–56

{n : ℕ} {F : Type u_1} {v : Exponence.RuleSet (SpanRule n F)} (hv : v.Antihomophonous) :

IsContiguous (realize v)

Superset spellout over an antihomophonous lexicon is contiguous (Caha 2009).

theorem isContiguous_spellout L58–61

{n : ℕ} {F : Type u_1} {v : Exponence.RuleSet (SupersetRule n F)} (hv : v.Antihomophonous) :

IsContiguous (spellout v)

The plateau: terminal adjacency generates only AAA and ABB

L65–69

Terminal rules with adjacent contexts have thresholds at most the first head, so the comparative and superlative cells coincide and only AAA and ABB root patterns are generable.

theorem realize_const_of_terminal_adjacent L78–83

{F : Type u_1} {v : Exponence.RuleSet (SpanRule 3 F)} (hT : Terminal v) (hA : Adjacent v) :

realize v 1 = realize v 2

Completeness: Elsewhere-generable = contiguous

A pattern is Elsewhere-generable when some terminal antihomophonous rule set realizes it in full.

def ElsewhereGenerable L151–155

{n : ℕ} {F : Type u_1} (p : Paradigm n F) :

Prop

The definition is too large to print here; read it in the source.

Used by isContiguous_iff_generable, spelloutGenerable_iff_generable

Used in Suppletion/Theory, Graf2019, SmithMoskalEtAl2019

A fully realized pattern arises from Elsewhere insertion over a terminal antihomophonous rule set iff it is contiguous.

theorem isContiguous_iff_generable L157–166

{n : ℕ} {F : Type u_1} (p : Paradigm n F) :

IsContiguous p ↔ ElsewhereGenerable p

Built from

Three-grade hierarchies: *AAB and the portmanteau prediction

Over the three-grade degree hierarchy, a grounded antihomophonous rule set that realizes the positive and the comparative alike and realizes the superlative realizes all three alike, so good – gooder – best is not generable. Grounding alone does the work that Bobaljik 2012 ch. 5 assigns to the markedness condition and adjacency together (realize_const_of_markedness).

theorem realize_const_of_grounded L170–192

{F : Type u_1} {v : Exponence.RuleSet (SpanRule 3 F)} (hv : v.Antihomophonous) (hG : Grounded v) (h01 : realize v 0 = realize v 1) (h2 : (realize v 2).isSome = true) :

realize v 1 = realize v 2

*AAB (Bobaljik 2012 ch. 5): over the three-grade degree hierarchy, an antihomophonous rule set meeting the markedness condition with adjacent contexts that realizes the positive and the comparative alike and realizes the superlative realizes all three alike.

theorem realize_const_of_markedness L194–201

{F : Type u_1} {v : Exponence.RuleSet (SpanRule 3 F)} (hv : v.Antihomophonous) (hM : Markedness v) (hA : Adjacent v) (h01 : realize v 0 = realize v 1) (h2 : (realize v 2).isSome = true) :

realize v 1 = realize v 2

Under adjacency, ABC requires a portmanteau, as with Latin opt- and Welsh gor- (Bobaljik 2012 §5.3.1).

theorem exists_portmanteau_of_ne L203–214

{F : Type u_1} {v : Exponence.RuleSet (SpanRule 3 F)} (hA : Adjacent v) (h12 : realize v 1 ≠ realize v 2) :

∃ it ∈ v, v.selectBy SpanRule.threshold 2 = some it ∧ 0 < ↑it.spans

A pattern is groundedly generable when some grounded antihomophonous rule set realizes it in full.

def GroundedGenerable L216–219

{n : ℕ} {F : Type u_1} (p : Paradigm n F) :

Prop

The definition is too large to print here; read it in the source.

Used by groundedGenerable_iff

Used in Suppletion/Theory

Over the three-grade hierarchy the groundedly generable patterns are the contiguous ones but AAB, that is AAA, ABB and ABC: the canonical rule set of such a pattern is grounded.

theorem groundedGenerable_iff L221–250

{F : Type u_1} [DecidableEq F] (p : Paradigm 3 F) :

GroundedGenerable p ↔ IsContiguous p ∧ ¬(p 0 = p 1 ∧ p 1 ≠ p 2)

Built from

Completeness: Superset-spellable = contiguous

A pattern is Superset-spellable when some antihomophonous lexicon spells it out in full.

def SupersetSpellable L305–308

{n : ℕ} {F : Type u_1} (p : Paradigm n F) :

Prop

The definition is too large to print here; read it in the source.

Used by isContiguous_iff_spelloutGenerable, spelloutGenerable_iff_generable

Used in Caha2009, Graf2019

A fully realized pattern arises from Superset spellout over an antihomophonous lexicon iff it is contiguous, Caha 2009's Universal Contiguity sharpened to exact generative capacity.

theorem isContiguous_iff_spelloutGenerable L310–319

{n : ℕ} {F : Type u_1} (p : Paradigm n F) :

IsContiguous p ↔ SupersetSpellable p

Built from

DM and nanosyntax are equigenerative over linear containment hierarchies. Superset spellout and Elsewhere insertion from terminal rule sets generate exactly the same fully realized patterns, the contiguous ones.

theorem spelloutGenerable_iff_generable L321–326

{n : ℕ} {F : Type u_1} (p : Paradigm n F) :

SupersetSpellable p ↔ ElsewhereGenerable p

Built from ,

Where the engines diverge

On partial rule sets the selection directions come apart: an entry storing more structure spells out smaller structures under the Superset Principle, while the corresponding rule leaves a gap under Elsewhere insertion, nanosyntax's characteristic prediction (De Clercq & Vanden Wyngaerd 2017).

Antihomophony is necessary for *ABA

Two entries sharing an exponent generate ABA. Caha 2009 separates such accidental homophony from syncretism, one entry over a contiguous span, and RuleSet.Antihomophonous is that separation.