Morphological Exponence Rules

@cite{bybee-1985} @cite{kennedy-2007} @cite{lakoff-1970} @cite{link-1983}

Concrete instantiations of MorphRule for functional categories.

All rules that are purely formal (no semantic contribution) have isVacuous := true. Number marking on nouns is the exception: singular restricts to atoms, plural applies algebraic closure.

inductive Core.Morphology.Tense.TenseFormType : Type

Whether a tense form is realized synthetically (inflectional suffix) or periphrastically (auxiliary + verb). Lakoff's key diagnostic: periphrastic forms block "false" tense interpretations.

• synthetic : TenseFormType
• periphrastic : TenseFormType

instance Core.Morphology.Tense.instDecidableEqTenseFormType : DecidableEq TenseFormType

Equations

• Core.Morphology.Tense.instDecidableEqTenseFormType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Morphology.Tense.instReprTenseFormType.repr : TenseFormType → Nat → Std.Format

Equations

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

instance Core.Morphology.Tense.instReprTenseFormType : Repr TenseFormType

Equations

• Core.Morphology.Tense.instReprTenseFormType = { reprPrec := Core.Morphology.Tense.instReprTenseFormType.repr }

def Core.Morphology.Tense.instBEqTenseFormType.beq : TenseFormType → TenseFormType → Bool

Equations

• Core.Morphology.Tense.instBEqTenseFormType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Morphology.Tense.instBEqTenseFormType : BEq TenseFormType

Equations

• Core.Morphology.Tense.instBEqTenseFormType = { beq := Core.Morphology.Tense.instBEqTenseFormType.beq }

def Core.Morphology.Tense.pastRule (σ : Type) (irregularForm : Option String := none) : MorphRule σ

Synthetic past tense rule: appends "-ed" to the lemma.

Irregular forms (e.g., "went", "was") are supplied via irregularForm. Semantically vacuous — temporal semantics is handled by PAST.

Equations

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

def Core.Morphology.Tense.presentRule (σ : Type) (irregularForm : Option String := none) : MorphRule σ

Synthetic present tense rule: appends "-s" for 3sg default.

Semantically vacuous — temporal semantics is handled by PRES.

Equations

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

def Core.Morphology.Tense.futureRule (σ : Type) : MorphRule σ

Synthetic future marker rule: prepends "will".

English future is borderline periphrastic, but Lakoff treats bare will as allowing false-tense interpretations (§5), so we classify it as synthetic for the false-tense diagnostic.

Equations

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

def Core.Morphology.Tense.periphrasticPastRule (σ : Type) : MorphRule σ

Periphrastic past rule: "used to V".

Cannot express false past (Lakoff §1, ex. 8a).

Equations

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

def Core.Morphology.Tense.periphrasticFutureRule (σ : Type) : MorphRule σ

Periphrastic future rule: "going to V".

Cannot express false future (Lakoff §1).

Equations

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

def Core.Morphology.Tense.pastPartRule (σ : Type) (irregularForm : Option String := none) : MorphRule σ

Past participle rule: appends "-ed" to the lemma.

Irregular forms (e.g., "eaten", "slept") are supplied via irregularForm. Semantically vacuous — participial semantics lives in the Theory layer.

Equations

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

theorem Core.Morphology.Tense.past_vacuous (σ : Type) (irr : Option String) : (pastRule σ irr).isVacuous = true

All tense rules are semantically vacuous.

theorem Core.Morphology.Tense.present_vacuous (σ : Type) (irr : Option String) : (presentRule σ irr).isVacuous = true

theorem Core.Morphology.Tense.future_vacuous (σ : Type) : (futureRule σ).isVacuous = true

theorem Core.Morphology.Tense.periphrasticPast_vacuous (σ : Type) : (periphrasticPastRule σ).isVacuous = true

theorem Core.Morphology.Tense.periphrasticFuture_vacuous (σ : Type) : (periphrasticFutureRule σ).isVacuous = true

theorem Core.Morphology.Tense.pastPart_vacuous (σ : Type) (irr : Option String) : (pastPartRule σ irr).isVacuous = true

theorem Core.Morphology.Tense.past_category (σ : Type) (irr : Option String) : (pastRule σ irr).category = MorphCategory.tense

All tense rules have category .tense.

theorem Core.Morphology.Tense.present_category (σ : Type) (irr : Option String) : (presentRule σ irr).category = MorphCategory.tense

theorem Core.Morphology.Tense.future_category (σ : Type) : (futureRule σ).category = MorphCategory.tense

theorem Core.Morphology.Tense.periphrasticPast_category (σ : Type) : (periphrasticPastRule σ).category = MorphCategory.tense

theorem Core.Morphology.Tense.periphrasticFuture_category (σ : Type) : (periphrasticFutureRule σ).category = MorphCategory.tense

theorem Core.Morphology.Tense.pastPart_category (σ : Type) (irr : Option String) : (pastPartRule σ irr).category = MorphCategory.tense

def Core.Morphology.Aspect.presPartRule (σ : Type) (irregularForm : Option String := none) : MorphRule σ

Present participle rule: appends "-ing" to the lemma.

Irregular forms (e.g., "running", "lying") are supplied via irregularForm. Semantically vacuous — progressive/gerundive semantics is handled in Theory.

Equations

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

theorem Core.Morphology.Aspect.presPart_vacuous (σ : Type) (irr : Option String) : (presPartRule σ irr).isVacuous = true

theorem Core.Morphology.Aspect.presPart_category (σ : Type) (irr : Option String) : (presPartRule σ irr).category = MorphCategory.aspect

def Core.Morphology.Number.singularNounRule {α : Type} (atomPred : α → Bool) : MorphRule (α → Bool)

Singular rule for nouns: adds atomicity condition.

Semantics: pred ↦ (λ x => pred x ∧ Atom x) This implements @cite{link-1983}: singular nouns denote atomic individuals.

Equations

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

def Core.Morphology.Number.pluralNounRule {α : Type} (closurePred : (α → Bool) → α → Bool) (atomPred : α → Bool) (irregularForm : Option String := none) : MorphRule (α → Bool)

Plural rule for nouns (regular: append -s).

Semantics: pred ↦ closurePred pred ∧ ¬Atom where closurePred is Link's algebraic closure (from Core/Mereology.lean).

This makes "dogs" true of plural individuals (sums of dogs).

Equations

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

def Core.Morphology.Number.pluralNounRuleFlat {α : Type} (irregularForm : Option String := none) : MorphRule (α → Bool)

Plural rule with identity semantics, for models without mereological structure (e.g., toy models with only atomic individuals).

Equations

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

def Core.Morphology.Number.verbAgreement3sg (σ : Type) : MorphRule σ

Verb agreement -s: formal change only, semantically vacuous.

Equations

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

theorem Core.Morphology.Number.verbAgreement_preserves_meaning (σ : Type) (meaning : σ) : (verbAgreement3sg σ).semEffect meaning = meaning

Verb agreement is semantically vacuous.

def Core.Morphology.Degree.comparativeRule (σ : Type) (irregularForm : Option String := none) : MorphRule σ

Comparative degree rule: generates the comparative form of an adjective.

Regular formation appends "-er" to the lemma; irregular forms (e.g., "better", "more expensive") are supplied via irregularForm.

Semantically vacuous at the morphological level — comparative semantics (degree quantification) is handled compositionally by Semantics.Lexical.Adjective.Comparative.

Equations

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

def Core.Morphology.Degree.superlativeRule (σ : Type) (irregularForm : Option String := none) : MorphRule σ

Superlative degree rule: generates the superlative form of an adjective.

Regular formation appends "-est" to the lemma; irregular forms (e.g., "best", "most expensive") are supplied via irregularForm.

Semantically vacuous at the morphological level — superlative semantics (MAX operator) is handled compositionally.

Equations

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

theorem Core.Morphology.Degree.comparative_vacuous (σ : Type) (irr : Option String) : (comparativeRule σ irr).isVacuous = true

Both degree rules are semantically vacuous.

theorem Core.Morphology.Degree.superlative_vacuous (σ : Type) (irr : Option String) : (superlativeRule σ irr).isVacuous = true

theorem Core.Morphology.Degree.comparative_category (σ : Type) (irr : Option String) : (comparativeRule σ irr).category = MorphCategory.degree

Both degree rules have category .degree.

theorem Core.Morphology.Degree.superlative_category (σ : Type) (irr : Option String) : (superlativeRule σ irr).category = MorphCategory.degree