Degree paradigms

Framework-neutral substrate for the three-grade degree hierarchy (positive, comparative, superlative) and the *ABA generalization over it: the n = 3 specialization of Morphology.Paradigm, mirroring Morphology.Case.Allomorphy for case. DegreePattern is the ergonomic record form; DegreePattern.toParadigm 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/Exponence/Containment/Contiguity.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.

DegreePattern

structure Morphology.Degree.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 : ℕ

@[implicit_reducible]

instance Morphology.Degree.instDecidableEqDegreePattern : DecidableEq DegreePattern

Equations

• Morphology.Degree.instDecidableEqDegreePattern = Morphology.Degree.instDecidableEqDegreePattern.decEq

def Morphology.Degree.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.Degree.instReprDegreePattern : Repr DegreePattern

Equations

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

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

Equations

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

def Morphology.Degree.DegreePattern.toParadigm (p : DegreePattern) : Paradigm 3 ℕ

The general-substrate form of a degree pattern.

Equations

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

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

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

Equations

• p.IsContiguous = Morphology.IsContiguous p.toParadigm

@[implicit_reducible]

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

Equations

• Morphology.Degree.instDecidableIsContiguous p = Morphology.Degree.instDecidableIsContiguous._aux_1 p

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

A pattern violates the *ABA constraint.

Equations

• p.ViolatesABA = ¬p.IsContiguous

@[implicit_reducible]

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

Equations

• Morphology.Degree.instDecidableViolatesABA p = Morphology.Degree.instDecidableViolatesABA._aux_1 p

Paradigm classification

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

Comparative is suppletive (root differs from positive).

Equations

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

@[implicit_reducible]

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

Equations

• Morphology.Degree.instDecidableCmprSuppletive p = Morphology.Degree.instDecidableCmprSuppletive._aux_1 p

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

Superlative is suppletive (root differs from positive).

Equations

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

@[implicit_reducible]

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

Equations

• Morphology.Degree.instDecidableSprlSuppletive p = Morphology.Degree.instDecidableSprlSuppletive._aux_1 p

Paradigm constants

def Morphology.Degree.aaa : DegreePattern

AAA: regular throughout.

Equations

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

def Morphology.Degree.abb : DegreePattern

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

Equations

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

def Morphology.Degree.abc : DegreePattern

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

Equations

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

def Morphology.Degree.aba : DegreePattern

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

Equations

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

def Morphology.Degree.aab : DegreePattern

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

Equations

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

Smoke tests confirming each named pattern resolves correctly.

CSG Part I from contiguity alone

theorem Morphology.Degree.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.Degree.degreeShape {F : Type u_1} [DecidableEq F] (p : Paradigm 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, in Morphology/Exponence/Containment/Selection.lean) to the fragment-level pattern vocabulary; see Studies/Bobaljik2012.lean for the worked instances. 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 orthographic form triples.

Equations

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

Smoke tests for degreeShape covering the attested pattern types.