Neo-Gricean markedness and M-alternatives

[Hor84] [Lev00] [Ret15]

Markedness computation for the M-principle / division of pragmatic labor ([Hor84]; [Lev00]): which member of an antonym pair is the marked (costlier) form, computed from objective properties rather than stipulated in the lexicon.

Two distinct markedness notions feed the computation and should not be conflated: form markedness (morphological complexity, negative prefixation — the notion [Hor84]'s division of labor ranges over) and pole markedness (the negative pole of a scalar dimension — [Bie89]; [Ken07]). The criteria below keep them separate; computeMarked resolves them in a fixed priority order (morphological complexity, then negative prefix, then scale direction). The priority ordering is this formalization's resolution policy — the sources motivate the individual criteria, not the ordering.

M-alternatives ([Ret15]) differ in form cost, not truth conditions: they exist only in polar-invariant constructions, where antonyms are truth-conditionally equivalent (equatives, degree questions) — not in polar-variant ones (positives, comparatives, measure phrases).

English worked entries (tall_with_morphology, …) live in Fragments/English/Predicates/Adjectival.lean; the studies exercising them are Studies/Horn1984.lean, Studies/Krifka2007.lean, and Studies/Rett2015.lean.

structure NeoGricean.Markedness.Morphology : Type

Morphological structure of an adjective form: morpheme count, negative prefixation, and derivational status.

• 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")

@[implicit_reducible]

instance NeoGricean.Markedness.instReprMorphology : Repr Morphology

Equations

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

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

Equations

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

@[implicit_reducible]

instance NeoGricean.Markedness.instDecidableEqMorphology : DecidableEq Morphology

Equations

• NeoGricean.Markedness.instDecidableEqMorphology = NeoGricean.Markedness.instDecidableEqMorphology.decEq

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

Equations

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

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

Morphology of a monomorphemic adjective.

Equations

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

def NeoGricean.Markedness.prefixedMorphology (form : String) : Morphology

Morphology of a negative-prefixed adjective (prefix + base).

Equations

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

structure NeoGricean.Markedness.GradableAdjWithMorphologyextends Degree.GradableAdjective : Type

A gradable adjective entry extended with morphological structure and scale-pole information, the inputs to markedness computation.

• form : String
• script : Option String
• dimension : Option Features.ScalarDimension
• isLowerEndpoint : Bool
• comparison : ComparisonFacet
• antonymForm : Option String
• standardOverride : Option PositiveStandard
• antonymRelation : Option AntonymRelation
• spatialConfigType : Option SpatialConfigType
• evaluativeValence : Option Features.EvaluativeValence
• morphology : Morphology

  Morphological structure

• isPositivePole : Bool

  Is this the positive pole of the scale?

@[implicit_reducible]

instance NeoGricean.Markedness.instReprGradableAdjWithMorphology : Repr GradableAdjWithMorphology

Equations

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

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

Equations

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

@[reducible, inline]

abbrev NeoGricean.Markedness.MarkednessCriterion : Type

A markedness criterion: given an antonym pair, return the marked (costlier) form, or none when the criterion cannot decide.

Equations

• NeoGricean.Markedness.MarkednessCriterion = (NeoGricean.Markedness.GradableAdjWithMorphology → NeoGricean.Markedness.GradableAdjWithMorphology → Option String)

def NeoGricean.Markedness.morphologicalCriterion : MarkednessCriterion

Morphological-complexity criterion ([Hor84]): the form with more morphemes is marked (un-happy over happy).

Equations

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

def NeoGricean.Markedness.negativePrefixCriterion : MarkednessCriterion

Negative-prefix criterion ([Cru86]): a form with a negative prefix (un-, in-, dis-) is marked. A special case of morphological complexity that tracks derivational direction.

Equations

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

def NeoGricean.Markedness.scaleDirectionCriterion : MarkednessCriterion

Scale-direction criterion ([Bie89]; [Ken07]): the negative pole is marked (short against tall).

Equations

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

def NeoGricean.Markedness.defaultCriteria : List MarkednessCriterion

The default criterion priority: morphological complexity, then negative prefix, then scale direction as the fallback for morphologically-equal pairs.

Equations

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

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

Resolve markedness by the first criterion that decides.

Equations

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

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

Resolve markedness by the default criteria.

Equations

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

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

Is form the marked member of the pair?

Equations

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

def NeoGricean.Markedness.costDifference : ℚ

The marked–unmarked production-cost differential licensing manner implicatures: using the costlier form when a cheaper equivalent exists signals something extra ([Hor84]'s division of pragmatic labor).

Equations

• NeoGricean.Markedness.costDifference = 1

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

Production cost: baseline 1 for unmarked forms, 1 + costDifference for marked forms.

Equations

• NeoGricean.Markedness.productionCost form adj1 adj2 = if NeoGricean.Markedness.isMarkedForm form adj1 adj2 = true then 1 + NeoGricean.Markedness.costDifference else 1

M-alternatives

M-alternatives differ in form cost, not truth conditions, so they exist only where antonyms are truth-conditionally equivalent: polar-invariant constructions ([Ret15]).

inductive NeoGricean.Markedness.PolarVariance : Type

Polar variance: whether antonyms differ in truth conditions in a given construction ("taller than" vs "shorter than") or coincide ("as tall as" vs "as short as").

• variant : PolarVariance
• invariant : PolarVariance

@[implicit_reducible]

instance NeoGricean.Markedness.instReprPolarVariance : Repr PolarVariance

Equations

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

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

Equations

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

@[implicit_reducible]

instance NeoGricean.Markedness.instDecidableEqPolarVariance : DecidableEq PolarVariance

Equations

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

def NeoGricean.Markedness.polarVariance : Degree.Construction → PolarVariance

Polar variance by adjectival construction ([Ret15]): positives, comparatives, and measure phrases are polar-variant; equatives and degree questions are polar-invariant.

Equations

• NeoGricean.Markedness.polarVariance Degree.Construction.positive = NeoGricean.Markedness.PolarVariance.variant
• NeoGricean.Markedness.polarVariance Degree.Construction.comparative = NeoGricean.Markedness.PolarVariance.variant
• NeoGricean.Markedness.polarVariance Degree.Construction.equative = NeoGricean.Markedness.PolarVariance.invariant
• NeoGricean.Markedness.polarVariance Degree.Construction.degreeQuestion = NeoGricean.Markedness.PolarVariance.invariant
• NeoGricean.Markedness.polarVariance Degree.Construction.measurePhrase = NeoGricean.Markedness.PolarVariance.variant

structure NeoGricean.Markedness.MAlternativeSet : Type

An M-alternative set: two forms differing in cost but not truth conditions, in a polar-invariant construction.

• marked : String

  The marked (costlier) form

• unmarked : String

  The unmarked (cheaper) form

• dimension : Features.ScalarDimension

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

• costDifference : ℚ

  The cost difference between forms

• construction : Degree.Construction

  Construction where they're equivalent

@[implicit_reducible]

instance NeoGricean.Markedness.instReprMAlternativeSet : Repr MAlternativeSet

Equations

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

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

Equations

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

@[implicit_reducible]

instance NeoGricean.Markedness.instBEqMAlternativeSet : BEq MAlternativeSet

Equations

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

def NeoGricean.Markedness.generateMAlternatives (adj1 adj2 : GradableAdjWithMorphology) (construction : Degree.Construction) : Option MAlternativeSet

Generate the M-alternative set for an antonym pair: defined exactly when the construction is polar-invariant and markedness is decidable for the pair.

Equations

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

def NeoGricean.Markedness.isMarkedInMAlternatives (form : String) (adj1 adj2 : GradableAdjWithMorphology) (construction : Degree.Construction) : Bool

Is form the marked member of the pair's M-alternative set?

Equations

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

def NeoGricean.Markedness.getMAlternative (form : String) (adj1 adj2 : GradableAdjWithMorphology) (construction : Degree.Construction) : Option String

The M-alternative of form in the pair, if any.

Equations

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