Degree Containment — Substrate

[Bob12]

Framework-neutral substrate for the three-grade degree hierarchy (positive, comparative, superlative) and the *ABA generalization over it: the n = 3 specialization of Morphology.Containment.Pattern, mirroring Morphology.Case.Allomorphy for case. DegreePattern is the ergonomic record form; DegreePattern.toPattern connects it to the general substrate, and all predicates are defined through that projection, so the generic theory applies by construction.

The empirical generalization [Bob12] surveys: across languages, suppletion in adjectival comparison patterns as tall – taller – tallest (AAA), good – better – best (ABB), or bonus – melior – optimus (ABC); both *good – better – goodest (ABA) and *good – gooder – best (AAB) are unattested. Contiguity excludes only ABA; the AAB exclusion and the derivations live in the realizational engine (Morphology/Containment/Vocabulary.lean) and are instantiated in Studies/Bobaljik2012.lean.

Scope restriction (cf. [Bob12] pp. 2, 28): the contiguity claim concerns relative superlatives. Absolute / elatival superlatives (e.g., Italian bellissimo) lack the comparative meaning component and hence the containment structure.

Degree grades

inductive Morphology.DegreeContainment.DegreeGrade : Type

The three morphological grades of adjectival degree. Structural layers: each higher grade's morphosyntactic representation contains the lower ones.

• pos : DegreeGrade
• cmpr : DegreeGrade
• sprl : DegreeGrade

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableEqDegreeGrade : DecidableEq DegreeGrade

Equations

• Morphology.DegreeContainment.instDecidableEqDegreeGrade x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.DegreeContainment.instReprDegreeGrade.repr : DegreeGrade → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Morphology.DegreeContainment.instReprDegreeGrade : Repr DegreeGrade

Equations

• Morphology.DegreeContainment.instReprDegreeGrade = { reprPrec := Morphology.DegreeContainment.instReprDegreeGrade.repr }

def Morphology.DegreeContainment.DegreeGrade.toFin : DegreeGrade → Fin 3

The degree grade as a position in the 3-grade hierarchy, for indexing Morphology.Containment machinery.

Equations

• Morphology.DegreeContainment.DegreeGrade.pos.toFin = 0
• Morphology.DegreeContainment.DegreeGrade.cmpr.toFin = 1
• Morphology.DegreeContainment.DegreeGrade.sprl.toFin = 2

def Morphology.DegreeContainment.DegreeGrade.rank (g : DegreeGrade) : ℕ

Containment rank: POS < CMPR < SPRL. Derived from toFin.

Equations

• g.rank = ↑g.toFin

DegreePattern

structure Morphology.DegreeContainment.DegreePattern : Type

A suppletive pattern over the three grades, indexed by form-class. Two grades share a root iff they have the same index.

Examples:

• AAA (0,0,0): tall – taller – tallest
• ABB (0,1,1): good – better – best
• ABC (0,1,2): bonus – melior – optimus
• *ABA (0,1,0): unattested.

• pos : ℕ
• cmpr : ℕ
• sprl : ℕ

def Morphology.DegreeContainment.instDecidableEqDegreePattern.decEq (x✝ x✝¹ : DegreePattern) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableEqDegreePattern : DecidableEq DegreePattern

Equations

• Morphology.DegreeContainment.instDecidableEqDegreePattern = Morphology.DegreeContainment.instDecidableEqDegreePattern.decEq

@[implicit_reducible]

instance Morphology.DegreeContainment.instReprDegreePattern : Repr DegreePattern

Equations

• Morphology.DegreeContainment.instReprDegreePattern = { reprPrec := Morphology.DegreeContainment.instReprDegreePattern.repr }

def Morphology.DegreeContainment.instReprDegreePattern.repr : DegreePattern → ℕ → Std.Format

Equations

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

def Morphology.DegreeContainment.DegreePattern.toPattern (p : DegreePattern) : Containment.Pattern 3 ℕ

The general-substrate form of a degree pattern.

Equations

• p.toPattern = ![p.pos, p.cmpr, p.sprl]

@[simp]

theorem Morphology.DegreeContainment.DegreePattern.toPattern_zero (p : DegreePattern) : p.toPattern 0 = p.pos

@[simp]

theorem Morphology.DegreeContainment.DegreePattern.toPattern_one (p : DegreePattern) : p.toPattern 1 = p.cmpr

@[simp]

theorem Morphology.DegreeContainment.DegreePattern.toPattern_two (p : DegreePattern) : p.toPattern 2 = p.sprl

def Morphology.DegreeContainment.DegreePattern.IsContiguous (p : DegreePattern) : Prop

A pattern is contiguous: each form class occupies an interval of grades. The generic Morphology.Containment.IsContiguous, by construction.

Equations

• p.IsContiguous = Morphology.Containment.IsContiguous p.toPattern

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableIsContiguous (p : DegreePattern) : Decidable p.IsContiguous

Equations

• Morphology.DegreeContainment.instDecidableIsContiguous p = Morphology.DegreeContainment.instDecidableIsContiguous._aux_1 p

def Morphology.DegreeContainment.DegreePattern.ViolatesABA (p : DegreePattern) : Prop

A pattern violates the *ABA constraint.

Equations

• p.ViolatesABA = ¬p.IsContiguous

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableViolatesABA (p : DegreePattern) : Decidable p.ViolatesABA

Equations

• Morphology.DegreeContainment.instDecidableViolatesABA p = Morphology.DegreeContainment.instDecidableViolatesABA._aux_1 p

Pattern classification

def Morphology.DegreeContainment.DegreePattern.IsRegular (p : DegreePattern) : Prop

All three grades share the same root (regular paradigm).

Equations

• p.IsRegular = (p.pos = p.cmpr ∧ p.cmpr = p.sprl)

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableIsRegular (p : DegreePattern) : Decidable p.IsRegular

Equations

• Morphology.DegreeContainment.instDecidableIsRegular p = Morphology.DegreeContainment.instDecidableIsRegular._aux_1 p

def Morphology.DegreeContainment.DegreePattern.CmprSuppletive (p : DegreePattern) : Prop

Comparative is suppletive (root differs from positive).

Equations

• p.CmprSuppletive = (p.pos ≠ p.cmpr)

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableCmprSuppletive (p : DegreePattern) : Decidable p.CmprSuppletive

Equations

• Morphology.DegreeContainment.instDecidableCmprSuppletive p = Morphology.DegreeContainment.instDecidableCmprSuppletive._aux_1 p

def Morphology.DegreeContainment.DegreePattern.SprlSuppletive (p : DegreePattern) : Prop

Superlative is suppletive (root differs from positive).

Equations

• p.SprlSuppletive = (p.pos ≠ p.sprl)

@[implicit_reducible]

instance Morphology.DegreeContainment.instDecidableSprlSuppletive (p : DegreePattern) : Decidable p.SprlSuppletive

Equations

• Morphology.DegreeContainment.instDecidableSprlSuppletive p = Morphology.DegreeContainment.instDecidableSprlSuppletive._aux_1 p

Pattern constants

def Morphology.DegreeContainment.aaa : DegreePattern

AAA: regular throughout.

Equations

• Morphology.DegreeContainment.aaa = { pos := 0, cmpr := 0, sprl := 0 }

def Morphology.DegreeContainment.abb : DegreePattern

ABB: suppletive comparative; superlative shares comparative root. English good – better – best.

Equations

• Morphology.DegreeContainment.abb = { pos := 0, cmpr := 1, sprl := 1 }

def Morphology.DegreeContainment.abc : DegreePattern

ABC: three distinct roots. Latin bonus – melior – optimus.

Equations

• Morphology.DegreeContainment.abc = { pos := 0, cmpr := 1, sprl := 2 }

def Morphology.DegreeContainment.aba : DegreePattern

*ABA: the unattested pattern (*good – better – goodest).

Equations

• Morphology.DegreeContainment.aba = { pos := 0, cmpr := 1, sprl := 0 }

def Morphology.DegreeContainment.aab : DegreePattern

*AAB: contiguous, but unattested — excluded by the vocabulary-level conditions of Morphology/Containment/Vocabulary.lean (csg2), not by contiguity.

Equations

• Morphology.DegreeContainment.aab = { pos := 0, cmpr := 0, sprl := 1 }

Smoke tests confirming each named pattern resolves correctly.

CSG Part I from contiguity alone

theorem Morphology.DegreeContainment.csg_part1 (p : DegreePattern) (h_contig : p.IsContiguous) (h_cmpr_suppl : p.CmprSuppletive) : p.SprlSuppletive

Comparative-Superlative Generalization, Part I ([Bob12]): if the comparative is suppletive, the superlative is also suppletive (with respect to the positive). Follows from contiguity alone — if POS ≠ CMPR, a contiguous pattern cannot have POS = SPRL (that would be ABA).

Reading a pattern off realized cells

def Morphology.DegreeContainment.degreeShape {F : Type u_1} [DecidableEq F] (p : Containment.Pattern 3 F) : DegreePattern

Classify a 3-grade realization into a DegreePattern by grouping identical cells: positive root is index 0, fresh roots get fresh indices. Connects the realizational engine's output (Morphology.Containment.realize) to the fragment-level pattern vocabulary; see Studies/Bobaljik2012.lean for the worked instances.

Equations

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

def Morphology.DegreeContainment.patternFromForms (pos cmpr sprl : String) : DegreePattern

Derive a DegreePattern from three surface forms — degreeShape on the form triple. Caveat ([Bob12] ch. 5 fn. 4): surface-form identity cannot distinguish suppletion from readjustment (German hoch – höher – höchst would misread as ABA), so fragment entries record curated patterns rather than applying this to orthography.

Equations

• Morphology.DegreeContainment.patternFromForms pos cmpr sprl = Morphology.DegreeContainment.degreeShape ![pos, cmpr, sprl]

Smoke tests for degreeShape and patternFromForms covering the attested pattern types.