structure Implicature.Markedness.Morphology : Type

Morphological structure of an adjective form.

Tracks properties relevant to markedness computation:

• Morpheme count (un-happy = 2, happy = 1)
• Presence of negative prefix (un-, in-, dis-)
• Derivational complexity

• form : String

  The surface form

• morphemeCount : ℕ

  Number of morphemes

• hasNegativePrefix : Bool

  Has a negative prefix (un-, in-, dis-, etc.)

• isDerived : Bool

  Is derived from the antonym (e.g., "unhappy" from "happy")

def Implicature.Markedness.instReprMorphology.repr : Morphology → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Implicature.Markedness.instReprMorphology : Repr Morphology

Equations

• Implicature.Markedness.instReprMorphology = { reprPrec := Implicature.Markedness.instReprMorphology.repr }

def Implicature.Markedness.instDecidableEqMorphology.decEq (x✝ x✝¹ : Morphology) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Implicature.Markedness.instDecidableEqMorphology : DecidableEq Morphology

Equations

• Implicature.Markedness.instDecidableEqMorphology = Implicature.Markedness.instDecidableEqMorphology.decEq

def Implicature.Markedness.simpleMorphology (form : String) : Morphology

Simple morphology for a monomorphemic adjective

Equations

• Implicature.Markedness.simpleMorphology form = { form := form, morphemeCount := 1, hasNegativePrefix := false, isDerived := false }

def Implicature.Markedness.prefixedMorphology (form : String) (pfx : String := "un") : Morphology

Morphology for a prefixed negative adjective

Equations

• Implicature.Markedness.prefixedMorphology form pfx = { form := form, morphemeCount := 2, hasNegativePrefix := true, isDerived := true }

structure Implicature.Markedness.GradableAdjWithMorphologyextends Semantics.Gradability.GradableAdjEntry : Type

Extended gradable adjective entry with morphological information.

Extends GradableAdjEntry with:

• Morphological structure for markedness computation
• Polarity indicator (positive vs negative pole)

• form : String
• scaleType : Core.Scale.Boundedness
• dimension : Features.Dimension
• antonymForm : Option String
• antonymRelation : Option AntonymRelation
• spatialConfigType : Option SpatialConfigType
• evaluativeValence : Option Features.EvaluativeValence
• morphology : Morphology

  Morphological structure

• isPositivePole : Bool

  Is this the positive pole of the scale?

def Implicature.Markedness.instReprGradableAdjWithMorphology.repr : GradableAdjWithMorphology → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Implicature.Markedness.instReprGradableAdjWithMorphology : Repr GradableAdjWithMorphology

Equations

• Implicature.Markedness.instReprGradableAdjWithMorphology = { reprPrec := Implicature.Markedness.instReprGradableAdjWithMorphology.repr }

structure Implicature.Markedness.MarkednessCriterion : Type

A markedness criterion computes which member of an antonym pair is marked.

Given two adjective entries (typically an antonym pair), the criterion returns the form that is MARKED (more costly, requiring more justification).

Returns none if the criterion cannot determine markedness (e.g., both have equal morphological complexity).

• name : String

  Name of this criterion

• citation : String

  Academic source

• computeMarked : GradableAdjWithMorphology → GradableAdjWithMorphology → Option String

  Compute which form is marked; returns the marked form

def Implicature.Markedness.morphologicalCriterion : MarkednessCriterion

Morphological complexity criterion.

The form with MORE morphemes is marked. This captures cases like un-happy > happy.

From @cite{horn-1984}: "Toward a new taxonomy for pragmatic inference"

Equations

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

def Implicature.Markedness.scaleDirectionCriterion : MarkednessCriterion

Scale direction criterion.

The NEGATIVE pole is marked. This captures cases like short (negative pole) vs tall (positive pole).

From @cite{bierwisch-1989}, @cite{kennedy-2007}

Equations

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

def Implicature.Markedness.negativePrefixCriterion : MarkednessCriterion

Negative prefix criterion.

Forms with negative prefixes (un-, in-, dis-) are marked. This is a specific case of morphological complexity that tracks derivational direction.

From @cite{cruse-1986}

Equations

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

def Implicature.Markedness.defaultCriteria : List MarkednessCriterion

Default priority ordering for markedness criteria.

Following @cite{rett-2015} and @cite{horn-1984}:

1. Morphological complexity (most reliable)
2. Negative prefix (specific morphological indicator)
3. Scale direction (fallback for equal morphology)

Equations

• Implicature.Markedness.defaultCriteria = [Implicature.Markedness.morphologicalCriterion, Implicature.Markedness.negativePrefixCriterion, Implicature.Markedness.scaleDirectionCriterion]

def Implicature.Markedness.computeMarkedWithCriteria (criteria : List MarkednessCriterion) (adj1 adj2 : GradableAdjWithMorphology) : Option String

Compute markedness using a list of criteria in priority order.

Returns the first successful determination.

Equations

• Implicature.Markedness.computeMarkedWithCriteria criteria adj1 adj2 = List.findSome? (fun (x : Implicature.Markedness.MarkednessCriterion) => x.computeMarked adj1 adj2) criteria

def Implicature.Markedness.computeMarked (adj1 adj2 : GradableAdjWithMorphology) : Option String

Compute markedness using default criteria.

Equations

• Implicature.Markedness.computeMarked adj1 adj2 = Implicature.Markedness.computeMarkedWithCriteria Implicature.Markedness.defaultCriteria adj1 adj2

def Implicature.Markedness.isMarkedForm (form : String) (adj1 adj2 : GradableAdjWithMorphology) : Bool

Check if a specific form is the marked one in a pair.

Equations

• Implicature.Markedness.isMarkedForm form adj1 adj2 = (Implicature.Markedness.computeMarked adj1 adj2 == some form)

def Implicature.Markedness.productionCost (form : String) (adj1 adj2 : GradableAdjWithMorphology) : ℚ

Production cost based on markedness.

Following Horn's Division of Pragmatic Labor:

• Unmarked forms have baseline cost (1)
• Marked forms have higher cost (2)

This cost differential licenses manner implicatures: using the more costly form when a cheaper equivalent exists signals something extra.

Equations

• Implicature.Markedness.productionCost form adj1 adj2 = if Implicature.Markedness.isMarkedForm form adj1 adj2 = true then 2 else 1

def Implicature.Markedness.costDifference : ℚ

Cost difference between marked and unmarked forms.

Equations

• Implicature.Markedness.costDifference = 1

def Implicature.Markedness.tall_with_morphology : GradableAdjWithMorphology

"tall" with morphology: simple, positive pole

Equations

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

def Implicature.Markedness.short_with_morphology : GradableAdjWithMorphology

"short" with morphology: simple, negative pole

Equations

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

def Implicature.Markedness.happy_with_morphology : GradableAdjWithMorphology

"happy" with morphology: simple, positive pole

Equations

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

def Implicature.Markedness.unhappy_with_morphology : GradableAdjWithMorphology

"unhappy" with morphology: prefixed, negative pole

Equations

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

theorem Implicature.Markedness.morphological_determines_markedness : morphologicalCriterion.computeMarked happy_with_morphology unhappy_with_morphology = some "unhappy"

Morphological complexity determines markedness: more morphemes = marked.

theorem Implicature.Markedness.scale_direction_for_equal_morphology : scaleDirectionCriterion.computeMarked tall_with_morphology short_with_morphology = some "short"

Scale direction determines markedness for equal morphology pairs.

theorem Implicature.Markedness.default_finds_short_marked : computeMarked tall_with_morphology short_with_morphology = some "short"

Default criteria successfully find "short" as marked in tall/short pair.

theorem Implicature.Markedness.default_finds_unhappy_marked : computeMarked happy_with_morphology unhappy_with_morphology = some "unhappy"

Default criteria successfully find "unhappy" as marked in happy/unhappy pair.

theorem Implicature.Markedness.marked_costs_more : productionCost "short" tall_with_morphology short_with_morphology > productionCost "tall" tall_with_morphology short_with_morphology

Marked form has higher cost than unmarked.

M-Alternatives

M-alternatives differ in FORM COST (markedness), not truth conditions. They only exist in polar-invariant constructions where antonyms have the same truth conditions (@cite{rett-2015} Chapter 5).

Polar Variance

Whether antonyms have the same truth conditions depends on the construction:

• Polar-VARIANT: "taller than" ≠ "shorter than" → no M-alternatives
• Polar-INVARIANT: "as tall as" = "as short as" → M-alternatives exist

inductive Implicature.Markedness.PolarVariance : Type

Polar variance: do antonyms have the same truth conditions in this construction?

• variant : PolarVariance
• invariant : PolarVariance

@[implicit_reducible]

instance Implicature.Markedness.instReprPolarVariance : Repr PolarVariance

Equations

• Implicature.Markedness.instReprPolarVariance = { reprPrec := Implicature.Markedness.instReprPolarVariance.repr }

def Implicature.Markedness.instReprPolarVariance.repr : PolarVariance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Implicature.Markedness.instDecidableEqPolarVariance : DecidableEq PolarVariance

Equations

• Implicature.Markedness.instDecidableEqPolarVariance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Implicature.Markedness.polarVariance : Semantics.Degree.AdjectivalConstruction → PolarVariance

Polar variance by adjectival construction type. @cite{rett-2015} Table 3.1/5.1.

Equations

• Implicature.Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.positive = Implicature.Markedness.PolarVariance.variant
• Implicature.Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.comparative = Implicature.Markedness.PolarVariance.variant
• Implicature.Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant
• Implicature.Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.degreeQuestion = Implicature.Markedness.PolarVariance.invariant
• Implicature.Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.measurePhrase = Implicature.Markedness.PolarVariance.variant

structure Implicature.Markedness.MAlternativeSet : Type

An M-alternative set: forms differing in cost but not truth conditions.

• marked : String

  The marked (costlier) form

• unmarked : String

  The unmarked (cheaper) form

• dimension : Features.Dimension

  The dimension they share (e.g., .height)

• costDifference : ℚ

  The cost difference between forms

• construction : Semantics.Degree.AdjectivalConstruction

  Construction where they're equivalent

@[implicit_reducible]

instance Implicature.Markedness.instReprMAlternativeSet : Repr MAlternativeSet

Equations

• Implicature.Markedness.instReprMAlternativeSet = { reprPrec := Implicature.Markedness.instReprMAlternativeSet.repr }

def Implicature.Markedness.instReprMAlternativeSet.repr : MAlternativeSet → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Implicature.Markedness.instBEqMAlternativeSet : BEq MAlternativeSet

Equations

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

def Implicature.Markedness.generateMAlternatives (adj1 adj2 : GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) : Option MAlternativeSet

Generate M-alternatives from an antonym pair.

M-alternatives are generated when:

1. The construction is polar-invariant (antonyms semantically equivalent)
2. Markedness can be determined for the pair

Equations

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

def Implicature.Markedness.isMarkedInMAlternatives (form : String) (adj1 adj2 : GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) : Bool

Check if a form is the marked member of an M-alternative pair.

Equations

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

def Implicature.Markedness.getMAlternative (form : String) (adj1 adj2 : GradableAdjWithMorphology) (construction : Semantics.Degree.AdjectivalConstruction) : Option String

Get the M-alternative for a form (if any).

Equations

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