Theories of root suppletion

Three theories say which root patterns a three-cell containment hierarchy can show, whether its cells are the grades of an adjective or the cases or numbers of a pronoun (Theory.Generates). Elsewhere insertion over the hierarchy generates the contiguous patterns, Bobaljik's containment with an antihomophonous and grounded vocabulary generates AAA, ABB and ABC (groundedGenerable_iff), and a theory of the cells as independent generates every pattern. A theory fits a pattern under a parse, which gives the cell whose structure each cell's word realizes, when a pattern it generates, read through the parse, classes the cells as the pattern does (Theory.Fits).

TODO

The domain locality of Smith, Moskal, Xu, Kang and Bobaljik (SmithMoskalEtAl2019.DomainLocal) is not registered. Its no-AAB plateau over degree is proved for terminal vocabularies, while an ABC triple needs a portmanteau, so its predictions over degree wait on the paper's treatment of portmanteaus.

References

• [Bob12]
• [SMX+19]

inductive Eval.Suppletion.Theory : Type

Three theories of the root patterns of a three-cell hierarchy.

• elsewhere : Theory

  Elsewhere insertion over the containment hierarchy, from terminal antihomophonous rules.

• grounded : Theory

  Bobaljik's containment, with an antihomophonous and grounded vocabulary.

• free : Theory

  The cells as independent, without containment.

@[instance_reducible]

instance Eval.Suppletion.instDecidableEqTheory : DecidableEq Theory

Equations

• Eval.Suppletion.instDecidableEqTheory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Eval.Suppletion.instReprTheory.repr : Theory → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Eval.Suppletion.instReprTheory : Repr Theory

Equations

• Eval.Suppletion.instReprTheory = { reprPrec := Eval.Suppletion.instReprTheory.repr }

def Eval.Suppletion.Theory.Generates : Theory → Morphology.Paradigm 3 ℕ → Prop

A theory generates a root pattern on the three cells of a hierarchy, for degree the three synthetic grades.

Equations

• Eval.Suppletion.Theory.elsewhere.Generates x✝ = Morphology.Containment.ElsewhereGenerable x✝
• Eval.Suppletion.Theory.grounded.Generates x✝ = Morphology.Containment.GroundedGenerable x✝
• Eval.Suppletion.Theory.free.Generates x✝ = True

@[instance_reducible]

instance Eval.Suppletion.instDecidablePredParadigmOfNatNatGenerates (T : Theory) : DecidablePred T.Generates

Equations

• One or more equations did not get rendered due to their size.
• Eval.Suppletion.instDecidablePredParadigmOfNatNatGenerates Eval.Suppletion.Theory.elsewhere = fun (p : Morphology.Paradigm 3 ℕ) => decidable_of_iff (p 0 = p 2 → p 0 = p 1) ⋯
• Eval.Suppletion.instDecidablePredParadigmOfNatNatGenerates Eval.Suppletion.Theory.free = fun (x : Morphology.Paradigm 3 ℕ) => isTrue trivial

def Eval.Suppletion.Theory.Containment : Theory → Prop

The theories that rest on containment, under which Merger reaches the comparative before the superlative.

Equations

• Eval.Suppletion.Theory.elsewhere.Containment = True
• Eval.Suppletion.Theory.grounded.Containment = True
• Eval.Suppletion.Theory.free.Containment = False

@[instance_reducible]

instance Eval.Suppletion.instDecidablePredTheoryContainment : DecidablePred Theory.Containment

Equations

• Eval.Suppletion.instDecidablePredTheoryContainment Eval.Suppletion.Theory.elsewhere = isTrue trivial
• Eval.Suppletion.instDecidablePredTheoryContainment Eval.Suppletion.Theory.grounded = isTrue trivial
• Eval.Suppletion.instDecidablePredTheoryContainment Eval.Suppletion.Theory.free = isFalse Eval.Suppletion.instDecidablePredTheoryContainment._proof_1

def Eval.Suppletion.shapes : List (Morphology.Paradigm 3 ℕ)

The five root patterns over three cells, one of each class.

Equations

• Eval.Suppletion.shapes = [Morphology.Paradigm.aaa, Morphology.Paradigm.abb, Morphology.Paradigm.abc, Morphology.Paradigm.aba, Morphology.Paradigm.aab]

def Eval.Suppletion.Theory.Fits (T : Theory) (e : Fin 3 → Fin 3) (p : Morphology.Paradigm 3 ℕ) : Prop

A theory fits a root pattern under a parse e, giving the grade whose structure the root's word realizes in each cell, when a pattern it generates, read through e, classes the grades as the root pattern does.

Equations

• T.Fits e p = ∃ q ∈ Eval.Suppletion.shapes, T.Generates q ∧ Setoid.ker (q ∘ e) = Setoid.ker p

@[instance_reducible]

instance Eval.Suppletion.instDecidableFits (T : Theory) (e : Fin 3 → Fin 3) (p : Morphology.Paradigm 3 ℕ) : Decidable (T.Fits e p)

Equations

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