inductive Phenomena.Imprecision.Numerals.RoundnessLevel : Type

Roundness level of a numeral.

More round = more potential for imprecision.

Source: @cite{krifka-2007}, @cite{sauerland-stateva-2007}

• exact : RoundnessLevel
• round1 : RoundnessLevel
• round2 : RoundnessLevel
• round3 : RoundnessLevel

def Phenomena.Imprecision.Numerals.instReprRoundnessLevel.repr : RoundnessLevel → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.Numerals.instReprRoundnessLevel : Repr RoundnessLevel

Equations

• Phenomena.Imprecision.Numerals.instReprRoundnessLevel = { reprPrec := Phenomena.Imprecision.Numerals.instReprRoundnessLevel.repr }

instance Phenomena.Imprecision.Numerals.instDecidableEqRoundnessLevel : DecidableEq RoundnessLevel

Equations

• Phenomena.Imprecision.Numerals.instDecidableEqRoundnessLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Imprecision.Numerals.classifyRoundness (n : Nat) : RoundnessLevel

Classify numeral roundness (simplified).

Equations

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

structure Phenomena.Imprecision.Numerals.NumeralImprecisionDatum : Type

Numeral imprecision datum: context-dependent exactness.

• numeral : Nat

  The numeral

• roundness : RoundnessLevel

  Roundness level

• sentenceFrame : String

  Sentence frame

• exactContext : String

  Context favoring exact reading

• inexactContext : String

  Context favoring inexact reading

• actualValue : Nat

  Actual value in scenario

• acceptableExact : Bool

  Acceptable in exact context?

• acceptableInexact : Bool

  Acceptable in inexact context?

def Phenomena.Imprecision.Numerals.instReprNumeralImprecisionDatum.repr : NumeralImprecisionDatum → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.Numerals.instReprNumeralImprecisionDatum : Repr NumeralImprecisionDatum

Equations

• Phenomena.Imprecision.Numerals.instReprNumeralImprecisionDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprNumeralImprecisionDatum.repr }

def Phenomena.Imprecision.Numerals.carsExact : NumeralImprecisionDatum

The cars scenario from the dissertation.

Source: dissertation (19), (20)

Equations

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

def Phenomena.Imprecision.Numerals.carsNonRound : NumeralImprecisionDatum

Equations

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

structure Phenomena.Imprecision.Numerals.RoundnessAsymmetryDatum : Type

Minimal pair showing round/non-round asymmetry.

• roundNumeral : Nat

  Round numeral

• nonRoundNumeral : Nat

  Non-round numeral

• context : String

  Context (same for both)

• actualValue : Nat

  Actual value

• roundAcceptable : Bool

  Round numeral acceptable?

• nonRoundAcceptable : Bool

  Non-round acceptable?

instance Phenomena.Imprecision.Numerals.instReprRoundnessAsymmetryDatum : Repr RoundnessAsymmetryDatum

Equations

• Phenomena.Imprecision.Numerals.instReprRoundnessAsymmetryDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprRoundnessAsymmetryDatum.repr }

def Phenomena.Imprecision.Numerals.instReprRoundnessAsymmetryDatum.repr : RoundnessAsymmetryDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.Numerals.hundredVsNinetyNine : RoundnessAsymmetryDatum

Equations

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

def Phenomena.Imprecision.Numerals.fiftyVsFortyNine : RoundnessAsymmetryDatum

Equations

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

structure Phenomena.Imprecision.Numerals.NegationConstraintDatum : Type

Numerals under negation require polar questions.

Source: @cite{solt-waldon-2019}

• positiveSentence : String

  Positive sentence

• negativeSentence : String

  Negative sentence

• howManyContext : String

  "How many" question context

• polarContext : String

  Polar question context

• negativeOkHowMany : Bool

  Negative OK in how-many context?

• negativeOkPolar : Bool

  Negative OK in polar context?

instance Phenomena.Imprecision.Numerals.instReprNegationConstraintDatum : Repr NegationConstraintDatum

Equations

• Phenomena.Imprecision.Numerals.instReprNegationConstraintDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprNegationConstraintDatum.repr }

def Phenomena.Imprecision.Numerals.instReprNegationConstraintDatum.repr : NegationConstraintDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.Numerals.sheepNegation : NegationConstraintDatum

Equations

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

structure Phenomena.Imprecision.Numerals.GameShowDatum : Type

The game show scenario tests for homogeneity gaps.

Context makes both exact and inexact readings relevant. If numerals had gaps like plurals, neither sentence should be clearly true.

Source: dissertation (164)

• sentence : String

  The sentence

• scenario : String

  Scenario description

• exactReadingTrue : Bool

  Exact reading true?

• inexactReadingTrue : Bool

  Inexact reading true?

• acceptable : Bool

  Judgment: is sentence acceptable?

• speakersAgree : Bool

  Do speakers agree?

• notes : String

  Notes

def Phenomena.Imprecision.Numerals.instReprGameShowDatum.repr : GameShowDatum → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.Numerals.instReprGameShowDatum : Repr GameShowDatum

Equations

• Phenomena.Imprecision.Numerals.instReprGameShowDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprGameShowDatum.repr }

def Phenomena.Imprecision.Numerals.gameShowPositive : GameShowDatum

Equations

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

def Phenomena.Imprecision.Numerals.gameShowNegative : GameShowDatum

Equations

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

structure Phenomena.Imprecision.Numerals.ExactlyModifierDatum : Type

"Exactly" removes imprecision, parallel to "all" for plurals.

Source: dissertation (4)

• bareSentence : String

  Bare numeral sentence

• exactlySentence : String

  Modified sentence

• context : String

  Context

• actualValue : Nat

  Actual value

• bareAcceptable : Bool

  Bare acceptable?

• exactlyAcceptable : Bool

  Exactly acceptable?

def Phenomena.Imprecision.Numerals.instReprExactlyModifierDatum.repr : ExactlyModifierDatum → Nat → Std.Format

Equations

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

instance Phenomena.Imprecision.Numerals.instReprExactlyModifierDatum : Repr ExactlyModifierDatum

Equations

• Phenomena.Imprecision.Numerals.instReprExactlyModifierDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprExactlyModifierDatum.repr }

def Phenomena.Imprecision.Numerals.exactlyRemovesImprecision : ExactlyModifierDatum

Equations

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

structure Phenomena.Imprecision.Numerals.ApproximatelyDatum : Type

"Approximately" explicitly marks imprecision.

Interestingly, "approximately" doesn't add imprecision to a precise expression; it makes imprecision explicit on an already-imprecise expression.

Source: dissertation (4)

• bareSentence : String

  Bare sentence

• approxSentence : String

  Approximately sentence

• roundness : RoundnessLevel

  Roundness of numeral

• approxNatural : Bool

  Is approximately acceptable with this numeral?

• notes : String

  Notes

instance Phenomena.Imprecision.Numerals.instReprApproximatelyDatum : Repr ApproximatelyDatum

Equations

• Phenomena.Imprecision.Numerals.instReprApproximatelyDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprApproximatelyDatum.repr }

def Phenomena.Imprecision.Numerals.instReprApproximatelyDatum.repr : ApproximatelyDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.Numerals.approximatelyWithRound : ApproximatelyDatum

Equations

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

def Phenomena.Imprecision.Numerals.approximatelyWithNonRound : ApproximatelyDatum

Equations

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

structure Phenomena.Imprecision.Numerals.TimeExpressionDatum : Type

Time expressions show similar round/non-round patterns.

Source: dissertation (163)

• sentence : String

  The sentence

• timeExpression : String

  Time expression

• round : Bool

  Is it round?

• scenario : String

  Scenario

• actualTime : String

  Exact arrival time

• acceptable : Bool

  Sentence acceptable?

instance Phenomena.Imprecision.Numerals.instReprTimeExpressionDatum : Repr TimeExpressionDatum

Equations

• Phenomena.Imprecision.Numerals.instReprTimeExpressionDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprTimeExpressionDatum.repr }

def Phenomena.Imprecision.Numerals.instReprTimeExpressionDatum.repr : TimeExpressionDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.Numerals.arriveAt3 : TimeExpressionDatum

Equations

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

def Phenomena.Imprecision.Numerals.arriveAt258 : TimeExpressionDatum

Equations

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

structure Phenomena.Imprecision.Numerals.GranularityDatum : Type

Granularity affects which numerals count as "round."

E.g., on a scale of dozens, 48 might be "round" (4 dozen).

Source: @cite{krifka-2007}

• numeral : Nat

  The numeral

• coarseScale : String

  Coarse scale description

• roundOnCoarse : Bool

  Is numeral round on this scale?

• fineScale : String

  Fine scale description

• roundOnFine : Bool

  Is numeral round on this scale?

instance Phenomena.Imprecision.Numerals.instReprGranularityDatum : Repr GranularityDatum

Equations

• Phenomena.Imprecision.Numerals.instReprGranularityDatum = { reprPrec := Phenomena.Imprecision.Numerals.instReprGranularityDatum.repr }

def Phenomena.Imprecision.Numerals.instReprGranularityDatum.repr : GranularityDatum → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.Numerals.granularityExample : GranularityDatum

Equations

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

structure Phenomena.Imprecision.Numerals.NumeralImprecisionGeneralizations : Type

Core empirical generalizations about numeral imprecision.

• roundPermitsImprecision : Bool

  Round numerals permit imprecision

• nonRoundRequiresExact : Bool

  Non-round require exactness

• exactlyRemoves : Bool

  "Exactly" removes imprecision

• negationRequiresPolar : Bool

  Negation requires polar questions

• noHomogeneityGaps : Bool

  No clear homogeneity gaps (unlike plurals)

• contextSensitive : Bool

  Imprecision is context-sensitive

instance Phenomena.Imprecision.Numerals.instReprNumeralImprecisionGeneralizations : Repr NumeralImprecisionGeneralizations

Equations

• Phenomena.Imprecision.Numerals.instReprNumeralImprecisionGeneralizations = { reprPrec := Phenomena.Imprecision.Numerals.instReprNumeralImprecisionGeneralizations.repr }

def Phenomena.Imprecision.Numerals.instReprNumeralImprecisionGeneralizations.repr : NumeralImprecisionGeneralizations → Nat → Std.Format

Equations

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

def Phenomena.Imprecision.Numerals.mainGeneralizations : NumeralImprecisionGeneralizations

Equations

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

def Phenomena.Imprecision.Numerals.carsExamples : List NumeralImprecisionDatum

Equations

• Phenomena.Imprecision.Numerals.carsExamples = [Phenomena.Imprecision.Numerals.carsExact, Phenomena.Imprecision.Numerals.carsNonRound]

def Phenomena.Imprecision.Numerals.roundnessAsymmetryExamples : List RoundnessAsymmetryDatum

Equations

• Phenomena.Imprecision.Numerals.roundnessAsymmetryExamples = [Phenomena.Imprecision.Numerals.hundredVsNinetyNine, Phenomena.Imprecision.Numerals.fiftyVsFortyNine]

def Phenomena.Imprecision.Numerals.gameShowExamples : List GameShowDatum

Equations

• Phenomena.Imprecision.Numerals.gameShowExamples = [Phenomena.Imprecision.Numerals.gameShowPositive, Phenomena.Imprecision.Numerals.gameShowNegative]

theorem Phenomena.Imprecision.Numerals.coarse_implies_kness (n : Nat) (h : n > 0) (hc : classifyRoundness n ≠ RoundnessLevel.exact) : Core.Roundness.roundnessScore n > 0

Coarse round → positive k-ness score. If classifyRoundness n ≠.exact, then n % 10 = 0, giving at least multipleOf5 and multipleOf10, so roundnessScore ≥ 2.