Scoring theories of root suppletion on Bobaljik (2012)

The data are the cognate triples of Bobaljik's Tables 4.1 and 4.2, read from Data/Forms/Bobaljik2012: for each, a source's judgment of which of a word's positive, comparative and superlative share a root, and the root pattern over the grades that the judgment gives (Bobaljik2012.rootPattern). A triple is observed unless a source rejects one of its forms in its cell (Contested), as the 2009 questionnaire rejects Zajkov's Karelian äij-in.

Three theories say which root patterns three synthetic grades can show (Theory.Generates). Elsewhere insertion over the containment 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 grades as independent cells generates every pattern. A theory parses a triple into the grade whose structure its root's word realizes in each cell: every grade itself, or the positive in a superlative that embeds it (Bobaljik2012.positiveEmbedding). A theory fits a triple under a parse when a pattern it generates, read through the parse, classes the grades as the triple does (Theory.Fits). The naive parse reads every triple as synthetic (naive); Bobaljik's parse stipulates the positive-embedding superlative for the Bulgarian and the Armenian 'many' (pp. 127-129), two stipulations (bobaljik).

Triple by triple (triples), a theory is right on an observed triple it fits and wrong on one it does not. Under the naive parse both containment theories are wrong on the Basque doublet and on the Bulgarian and Armenian quantifiers (wrong_naive_elsewhere, wrong_naive_grounded). Bobaljik's parse changes nothing off its stipulations (verdict_bobaljik_of_notMem) and makes both quantifiers right (verdict_bobaljik_stipulated), leaving the Basque doublet, which the book leaves open. Every theory is silent on the contested Karelian triple alone (contested_ids, verdict_eq_silent_iff), and the theory without containment, reading every triple as synthetic, is never wrong (verdict_free_naive_ne_wrong). Pattern by pattern (patterns), the linking hypothesis is asymmetric: a theory predicts that no observed triple shows a pattern it cannot generate on synthetic grades, and nothing about the others. Grounded containment alone is right that no triple is AAB, both containment theories are wrong that none is ABA on the surface, and the theory without containment predicts nothing (verdict_patterns).

Implementation notes

• A theory's generated patterns are compared up to their classes of grades, so Theory.Fits ranges over the five representatives of Morphology.Paradigm.
• The pattern experiment scores theories of synthetic grades; the parses enter only the triple experiment, where Bobaljik's two are stipulations rather than a rule.

References

• [Bob12]

The data

def Eval.Suppletion.Bobaljik2012.Contested (r : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) : Prop

A triple is contested when a source rejects one of its forms in its cell.

Equations

• Eval.Suppletion.Bobaljik2012.Contested r = ∃ g ∈ Bobaljik2012.Forms.marked, ∃ f ∈ r.forms, g.cell = f.cell ∧ g.form = f.form ∧ g.lexeme.id = r.lexeme.id

@[instance_reducible]

instance Eval.Suppletion.Bobaljik2012.instDecidablePredRootClassesCellContested : DecidablePred Contested

Equations

• Eval.Suppletion.Bobaljik2012.instDecidablePredRootClassesCellContested x✝ = Eval.Suppletion.Bobaljik2012.instDecidablePredRootClassesCellContested._aux_1 x✝

The theories

inductive Eval.Suppletion.Bobaljik2012.Theory : Type

Three theories of the root patterns of the grades.

• 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 grades as independent cells, without containment.

@[instance_reducible]

instance Eval.Suppletion.Bobaljik2012.instDecidableEqTheory : DecidableEq Theory

Equations

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

@[instance_reducible]

instance Eval.Suppletion.Bobaljik2012.instReprTheory : Repr Theory

Equations

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

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

Equations

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

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

A theory generates a root pattern on three synthetic grades.

Equations

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

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.
• Eval.Suppletion.Bobaljik2012.instDecidablePredParadigmOfNatNatGenerates Eval.Suppletion.Bobaljik2012.Theory.free = fun (x : Morphology.Paradigm 3 ℕ) => isTrue trivial

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

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

Equations

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

def Eval.Suppletion.Bobaljik2012.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.Bobaljik2012.shapes, T.Generates q ∧ Setoid.ker (q ∘ e) = Setoid.ker p

@[instance_reducible]

instance Eval.Suppletion.Bobaljik2012.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.

The parses

@[reducible, inline]

abbrev Eval.Suppletion.Bobaljik2012.TripleParser : Type

How a theory parses a triple, from the root pattern every theory shares, into the grade whose structure the root's word realizes in each cell.

Equations

• Eval.Suppletion.Bobaljik2012.TripleParser = Eval.Parser (Data.Forms.RootClasses Bobaljik2012.Forms.Cell) (Morphology.Paradigm 3 ℕ) (Fin 3 → Fin 3)

def Eval.Suppletion.Bobaljik2012.naive : TripleParser

Every triple read as synthetic.

Equations

• Eval.Suppletion.Bobaljik2012.naive = Eval.Parser.ofRule fun (x : Morphology.Paradigm 3 ℕ) => some id

def Eval.Suppletion.Bobaljik2012.bobaljik : TripleParser

Bobaljik's parse reads every triple as synthetic, except the Bulgarian and the Armenian 'many', whose superlatives embed the positive (pp. 127-129).

Equations

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

theorem Eval.Suppletion.Bobaljik2012.stipulations_naive : Parser.stipulations naive = ∅

theorem Eval.Suppletion.Bobaljik2012.card_stipulations_bobaljik : (Parser.stipulations bobaljik).card = 2

Triple by triple

def Eval.Suppletion.Bobaljik2012.triples : Experiment (Theory × TripleParser) (Data.Forms.RootClasses Bobaljik2012.Forms.Cell) Bool

Each triple scored by whether a theory, under its parse, fits it.

Equations

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

theorem Eval.Suppletion.Bobaljik2012.wrong_naive_elsewhere : List.map (fun (x : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) => x.id) (List.filter (fun (x : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) => decide (triples.verdict (Theory.elsewhere, naive) x = Verdict.wrong)) Bobaljik2012.Forms.rootClasses) = [Bobaljik2012.Forms.eus_good_on.roots.id, Bobaljik2012.Forms.bul_many.roots.id, Bobaljik2012.Forms.hye_many.roots.id]

Read as synthetic, the Basque doublet and the Bulgarian and Armenian quantifiers refute Elsewhere insertion.

theorem Eval.Suppletion.Bobaljik2012.wrong_naive_grounded : List.map (fun (x : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) => x.id) (List.filter (fun (x : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) => decide (triples.verdict (Theory.grounded, naive) x = Verdict.wrong)) Bobaljik2012.Forms.rootClasses) = [Bobaljik2012.Forms.eus_good_on.roots.id, Bobaljik2012.Forms.bul_many.roots.id, Bobaljik2012.Forms.hye_many.roots.id]

Read as synthetic, the same three triples refute grounded containment.

theorem Eval.Suppletion.Bobaljik2012.verdict_bobaljik_of_notMem {T : Theory} {r : Data.Forms.RootClasses Bobaljik2012.Forms.Cell} (hr : r ∉ Parser.stipulations bobaljik) : triples.verdict (T, bobaljik) r = triples.verdict (T, naive) r

Bobaljik's parse agrees with the naive one off its stipulations.

theorem Eval.Suppletion.Bobaljik2012.verdict_bobaljik_stipulated (T : Theory) : triples.verdict (T, bobaljik) Bobaljik2012.Forms.bul_many.roots = Verdict.correct ∧ triples.verdict (T, bobaljik) Bobaljik2012.Forms.hye_many.roots = Verdict.correct

Bobaljik's parse makes every theory right on the Bulgarian and Armenian quantifiers, so under it the containment theories are wrong on the Basque doublet alone.

theorem Eval.Suppletion.Bobaljik2012.contested_ids : List.map (fun (x : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) => x.id) (List.filter (fun (b : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) => decide (Contested b)) Bobaljik2012.Forms.rootClasses) = [Bobaljik2012.Forms.krl_many.roots.id]

The only contested triple is Zajkov's Karelian one.

theorem Eval.Suppletion.Bobaljik2012.verdict_eq_silent_iff {T : Theory} {π : TripleParser} (hπ : ∀ (p : Morphology.Paradigm 3 ℕ), π.rule p = some id) (r : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) : triples.verdict (T, π) r = Verdict.silent ↔ Contested r

Under a parse whose rule covers every triple, a theory is silent exactly on the contested triples.

theorem Eval.Suppletion.Bobaljik2012.free_fits_id (p : Morphology.Paradigm 3 ℕ) : Theory.free.Fits id p

Read as synthetic, every root pattern fits the theory without containment.

theorem Eval.Suppletion.Bobaljik2012.verdict_free_naive_ne_wrong (r : Data.Forms.RootClasses Bobaljik2012.Forms.Cell) : triples.verdict (Theory.free, naive) r ≠ Verdict.wrong

Read as synthetic, the theory without containment is never wrong.

Pattern by pattern

def Eval.Suppletion.Bobaljik2012.patterns : Experiment Theory (Morphology.Paradigm 3 ℕ) Bool

Each root pattern scored by whether an observed triple shows it, with the asymmetric linking hypothesis: a theory predicts the absence of each pattern it cannot generate.

Equations

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

theorem Eval.Suppletion.Bobaljik2012.verdict_patterns : patterns.verdict Theory.grounded Morphology.Paradigm.aab = Verdict.correct ∧ patterns.verdict Theory.elsewhere Morphology.Paradigm.aab = Verdict.silent ∧ patterns.verdict Theory.grounded Morphology.Paradigm.aba = Verdict.wrong ∧ patterns.verdict Theory.elsewhere Morphology.Paradigm.aba = Verdict.wrong ∧ ∀ (c : Morphology.Paradigm 3 ℕ), patterns.verdict Theory.free c = Verdict.silent

Grounded containment is right that no triple is AAB, where Elsewhere insertion predicts nothing; both are wrong that none is ABA; the theory without containment predicts nothing.