Scales #
@cite{fox-hackl-2006} @cite{holliday-icard-2013} @cite{kennedy-2007} @cite{krantz-1971} @cite{krifka-1989} @cite{rouillard-2026} @cite{link-1983} @cite{rett-2026} @cite{rullmann-1995}
Root algebraic infrastructure for all scale-based reasoning in linglib.
Categorical Structure #
The file defines a category of scales with two levels of enrichment:
ComparativeScale (α, ≤, boundedness)
╱ ╲
(+ join, ⊥, FA) (linear, μ, direction)
╱ ╲
AdditiveScale DirectedMeasure
╱ ╲ │
MereoScale EpistemicScale (†) │
│ │ │
│ additive │ additive │ μ
│ representation representation │
▼ ▼ ▼
(ℚ, ≤)
(†) See `Core/EpistemicScale.lean` for the epistemic arm.
Objects: ComparativeScale α — a preorder with boundedness classification.
Morphisms: Monotone (from Mathlib) — the categorical morphisms are just
monotone maps between preorders. MereoDim (= StrictMono) is the injective
subcategory.
Enriched subcategory: AdditiveScale α — comparative scale with join and
finite additivity (FA). Two independent instances:
- Mereological:
ExtMeasure.additive - Epistemic:
EpistemicSystemFA+FinAddMeasure(@cite{holliday-icard-2013}, §7)
Linear specialization: DirectedMeasure — comparative scale with a linear
order, measure function, and direction. Instances: Kennedy adjectives,
Rouillard TIAs, epistemic vocabulary.
The commutative diagram: both additive arms (mereological, epistemic) land in
(ℚ, ≤) via additive representation morphisms. The MIP arm also lands in (ℚ, ≤)
via measure functions. All three paths factor through ComparativeScale.
Measurement Scales #
Below the root structures, the file provides measurement scale infrastructure shared by degree semantics and temporal measurement:
| Kennedy (Adjectives) | Rouillard (TIAs) |
|---|---|
| Degree scale | Duration measurement domain |
| Open scale (tall, expensive) | Atelic VP / DIV predicate |
| → "??completely tall" | → "*was sick in three days" |
| Closed scale (full, empty) | Telic VP / QUA predicate |
| → "completely full" ✓ | → "wrote a paper in three days" ✓ |
| Interpretive Economy | MIP |
Both domains use Boundedness to classify scales, and Boundedness.isLicensed
derives the licensing prediction. Actual scale types encode boundedness via
Mathlib typeclasses (OrderTop, OrderBot, NoMaxOrder, NoMinOrder).
Classification of scale boundedness. @cite{kennedy-2007}: four scale types based on which endpoints exist. @cite{rouillard-2026}: temporal domains have similar boundary structure (closed intervals have both bounds, open intervals lack them).
This enum is the lexical data tag for classifying scales in fragment
entries and phenomena files. The actual order-theoretic properties of
concrete scale types are encoded via Mathlib typeclasses (OrderTop,
OrderBot, NoMaxOrder, NoMinOrder).
- open_ : Boundedness
- lowerBounded : Boundedness
- upperBounded : Boundedness
- closed : Boundedness
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
- Core.Scale.instBEqBoundedness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Does this scale have an inherent maximum?
Equations
Instances For
Does this scale have an inherent minimum?
Equations
Instances For
Licensing prediction: a bounded scale (any endpoint exists) admits a maximally informative element, licensing degree modifiers (Kennedy) or TIA numerals (Rouillard). An open scale does not. @cite{kennedy-2007}: Interpretive Economy requires non-trivial scale contribution. @cite{rouillard-2026}: MIP requires the numeral to be maximally informative.
Equations
Instances For
Derive a Boundedness tag from order-theoretic properties of a type.
Useful when you have a concrete type and want to classify it for
compatibility with lexical data.
Equations
Instances For
A rational number in the unit interval [0, 1].
Wraps Mathlib's Set.Icc subtype for gradient linguistic properties
(at-issueness, projectivity, etc.) and their contextual thresholds.
Using Set.Icc gives us standard interval infrastructure from Mathlib
(order, membership, etc.) without custom boilerplate.
Access: r.val for the rational value, r.prop.1 for 0 ≤ r,
r.prop.2 for r ≤ 1.
Equations
- Core.Scale.Rat01 = ↑(Set.Icc 0 1)
Instances For
Equations
- Core.Scale.Rat01.instRepr = { reprPrec := fun (r : Core.Scale.Rat01) (x : ℕ) => repr ↑r }
The midpoint ½, the standard default threshold.
Equations
Instances For
Closed-bounded: both 0 and 1 are attained.
Instances For
Binary mereological classification: the shared abstraction underlying all four licensing frameworks (Kennedy, Rouillard, Krifka, Zwarts).
Instances For
Equations
Equations
- Core.Scale.instBEqMereoTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
- Core.Scale.instReprMereoTag = { reprPrec := Core.Scale.instReprMereoTag.repr }
Equations
- Core.Scale.instReprMereoTag.repr Core.Scale.MereoTag.qua prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Scale.MereoTag.qua")).group prec✝
- Core.Scale.instReprMereoTag.repr Core.Scale.MereoTag.cum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Scale.MereoTag.cum")).group prec✝
Instances For
A licensing pipeline: any type whose elements can be classified into scale boundedness. Kennedy, Rouillard, Krifka, and Zwarts all instantiate this with different source types but the same target.
Core instances (Boundedness, MereoTag) live here. Domain-specific
instances (Telicity, VendlerClass, PathShape, BoundaryType)
live in their respective theory/bridge files.
- toBoundedness : α → Boundedness
Instances
Equations
Instances For
Equations
- Core.Scale.LicensingPipeline.instBoundedness = { toBoundedness := id }
Equations
- Core.Scale.LicensingPipeline.instMereoTag = { toBoundedness := Core.Scale.MereoTag.toBoundedness }
The universal licensing theorem: any two pipeline inputs that map to the same Boundedness yield the same licensing prediction, regardless of which framework they come.
A comparative scale: a boundedness classification on a preorder. This is the root object in the category of scales. All scale-based reasoning in linglib (degree semantics, mereological measurement, epistemic comparison) factors through this structure.
The ordering comes from the ambient [Preorder α] — no redundant
le/le_refl/le_trans fields. Morphisms are Mathlib's Monotone.
@cite{krantz-1971}: a comparative scale is an ordered set with enough structure to support qualitative comparison.
- boundedness : Boundedness
Scale boundedness classification
Instances For
An additive scale: a comparative scale enriched with join and finite additivity (FA). Two independent instances exist in linglib:
- Mereological:
ExtMeasure.additive - Epistemic: probability FA
The FA axiom says disjoint augmentation preserves order: if z is disjoint from both x and y, then x ≤ y ↔ x ⊔ z ≤ y ⊔ z. This is the qualitative content of additive representation.
- disjoint : α → α → Prop
Disjointness predicate
Finite additivity: disjoint augmentation preserves order. Both
≤and⊔come from the ambientSemilatticeSup.
Instances For
Licensing prediction from the underlying boundedness.
Equations
Instances For
An additive scale is representable if there exists a monotone additive function into (ℚ, ≤).
Equations
Instances For
Intrinsic polarity of a scale dimension.
positive: the unmarked direction (tall, hot, confident).
negative: the marked/inverted direction (short, cold, doubtful).
- positive : ScalePolarity
- negative : ScalePolarity
Instances For
Equations
- Core.Scale.instBEqScalePolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
A positive region on an ordered type: the abstract interface for "when does a gradable predicate hold?" Kennedy: compare to a threshold. CSW: qualitative background ordering. Both instantiate this.
- inRegion : α → θ → Bool
Is value
xin the positive region given parameterp?
Instances
A representation of a qualitative ordering by a quantitative measure. @cite{krantz-1971}: the fundamental bridge from comparative to numerical. Instances: AdditiveScale.IsRepresentable, Kennedy's μ, CSW's g(μ).
Krantz, D. et al. (1971). Foundations of measurement, Vol. 1.
- μ : S → D
The measure/representation function
Order-preservation
Instances For
A directed measurement on a bounded scale: the algebraic primitive underlying degree semantics, modal semantics, and epistemic scales.
A DirectedMeasure D E packages:
- A degree type
Dwith a linear order (the scale) - An entity type
E(what gets measured) - A measure function
μ : E → D(the measurement) - Boundedness classification (from
ComparativeScale) - A direction/polarity (positive or negative)
This is the common algebraic core of GradablePredicate (degree
semantics), MIP domain constructors (maximal informativity), and
epistemicAsGradable (epistemic threshold semantics). Each of
these extends or instantiates DirectedMeasure:
GradablePredicate E DextendsDirectedMeasure D EwithformkennedyNumeral,rouillardETIA, etc. produceDirectedMeasureinstances- Epistemic vocabulary:
DirectedMeasure ℚ (E × BProp W)
The degree property (atLeastDeg for positive, atMostDeg for
negative) is derived from direction, not stored. This captures
the insight from @cite{lassiter-goodman-2017} that the binary direction choice
(which side of the threshold counts as "satisfying the predicate")
is the fundamental parameter, and the degree property follows.
References:
- Kennedy, C. (2007). Vagueness and grammar.
- Lassiter, D. (2017). Graded modality. OUP.
- Rouillard, V. (2026). Maximal informativity and temporal in-adverbials.
- Krantz, D. et al. (1971). Foundations of measurement, Vol. 1.
- μ : E → D
Measure function: maps entities to degrees on the scale
- direction : ScalePolarity
Scale direction: positive (μ(x) ≥ θ) or negative (μ(x) ≤ θ). Determines which side of a threshold counts as satisfying the predicate. Positive: tall, likely, full. Negative: short, unlikely, empty.
Instances For
The degree property derived from direction:
- positive → μ(x) ≥ d (upward: meets threshold)
- negative → μ(x) ≤ d (downward: at most threshold)
This replaces a stored degProp field with a derived one.
The degree property is not independent data — it is determined by
the direction choice. Definitionally equal to atLeastDeg dm.μ
(positive) and atMostDeg dm.μ (negative), proved in §8b.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Licensing: licensed iff the bounded scale admits an optimum.
Equations
- dm.licensed = dm.boundedness.isLicensed
Instances For
Blocking: blocked iff open scale → information collapse.
Instances For
Licensing is determined solely by boundedness, regardless of domain, measure function, or direction.
Scale types as Mathlib typeclass combinations #
A measurement scale is just a LinearOrder. Density is DenselyOrdered,
and boundedness is OrderTop/OrderBot/NoMaxOrder/NoMinOrder.
No wrapper classes needed — use Mathlib directly:
- Measurement scale:
[LinearOrder α] - Dense measurement scale (@cite{fox-2007} UDM):
[LinearOrder α] [DenselyOrdered α] - Upper-bounded scale:
[LinearOrder α] [OrderTop α] - Lower-bounded scale:
[LinearOrder α] [OrderBot α] - Open scale:
[LinearOrder α] [NoMaxOrder α] [NoMinOrder α]
Instances:
- Degree scales for gradable adjectives
- Duration measurement for temporal adverbials
- Numeral scales for number words
@cite{fox-2007} UDM: all natural language scales satisfy DenselyOrdered.
Use [DenselyOrdered α] when density matters for the derivation.
A family of propositions indexed by scale values is upward monotone (entailments go from smaller to larger values). Kennedy: "tall" — if x is tall, x is tall-or-more. Rouillard: E-TIA with telic VP — if event fits in n days, it fits in m ≥ n days.
Equations
- Core.Scale.IsUpwardMonotone P = ∀ (x y : α), x ≤ y → ∀ (w : W), P x w → P y w
Instances For
A family is downward monotone: entailments go from larger to smaller. Rouillard: E-TIA with atelic VP — if sick during n-day time, sick during m ≤ n day time.
Equations
- Core.Scale.IsDownwardMonotone P = ∀ (x y : α), x ≤ y → ∀ (w : W), P y w → P x w
Instances For
A family is constant: every value yields the same proposition. This is information collapse — no value is more informative than another. Occurs when a family is both upward and downward monotone.
Equations
- Core.Scale.IsConstant P = ∀ (x y : α) (w : W), P x w ↔ P y w
Instances For
If P is both upward and downward monotone, it is constant.
Informativity licensing: a scale admits a well-defined optimum iff it is NOT constant. When the family is constant (information collapse), no grammatical element operating on that scale is felicitous.
This is the abstract pattern shared by:
- Kennedy's Interpretive Economy: degree modifiers require non-trivial scale contribution
- Rouillard's MIP: TIA numerals require maximally informative values
Equations
Instances For
Bimonotone families do not admit an optimum: if a family is both upward and downward monotone, it collapses to a constant and no element is maximally informative. This is the abstract core of why open-scale degree modification and atelic-VP E-TIAs are both blocked.
A scale value x is maximally informative in a degree property P
at world w iff P x w is true and P x entails P y for every
other true P y w.
@cite{fox-2007} §4: the unified exhaustivity requirement underlying implicatures (only), degree questions, and definite descriptions.
@cite{rouillard-2026} eq. (75): max⊨(w, P) specializes this to temporal domains. This definition is domain-general.
Equations
- Core.Scale.IsMaxInf P x w = (P x w ∧ ∀ (y : α), P y w → ∀ (w' : W), P x w' → P y w')
Instances For
A degree property has a maximally informative element at world w.
Equations
- Core.Scale.HasMaxInf P w = ∃ (x : α), Core.Scale.IsMaxInf P x w
Instances For
Information collapse: no element is maximally informative at any world. Fox & Hackl: this is why degree questions fail over dense complements, why only + "more than n" is contradictory, and why definite descriptions over dense open sets lack a presupposition-satisfying referent.
Equations
- Core.Scale.InformationCollapse P = ∀ (w : W), ¬Core.Scale.HasMaxInf P w
Instances For
On a scale with no maximum (NoMaxOrder), any upward monotone family
that is nontrivial (i.e., some value yields a different set of worlds
than another) cannot have a ceiling: for any candidate optimum, a
strictly larger value exists.
This is the typeclass-level counterpart of the data-level prediction
Boundedness.open_.isLicensed = false: open scales block degree
modification and TIA licensing because no element is maximal.
Proof sketch: For any x, NoMaxOrder gives y > x. If P is
upward monotone, P x w → P y w, so x is never the unique optimum.
On a scale with a top element (OrderTop), the predicate · = ⊤ is
upward monotone (vacuously — only ⊤ satisfies it) and nonconstant
(on nontrivial types). This witnesses that upper-bounded scales admit
an optimum.
Proof sketch: ⊤ satisfies · = ⊤, and for any x < ⊤, x does not.
So the family is not constant → AdmitsOptimum holds.
On a scale with a bottom element (OrderBot), the predicate · = ⊥ is
downward monotone and nonconstant (on nontrivial types). This witnesses
that lower-bounded scales admit an optimum.
Boundedness is necessary for licensing: on a scale with no upper bound and no lower bound, there exists a monotone family with no optimum. Contrapositive: if every monotone family admits an optimum, the scale has a bound.
Closed scales predict licensing (Kennedy: "completely full" ✓; Rouillard: telic VP E-TIA ✓).
Open scales predict blocking (Kennedy: "??completely tall"; Rouillard: atelic VP E-TIA ✗).
Degree properties for comparison relations #
Five degree properties covering all comparison relations, parameterized by
a measure function μ : W → α. These are the building blocks for numeral
semantics (Numeral.Semantics.maxMeaning) and degree questions
(DegreeQuestion).
atLeastDeg: closed≥, always has max⊨moreThanDeg: open>, fails on dense scaleseqDeg: equality=, trivially has max⊨atMostDeg: closed≤lessThanDeg: open<
The key divergence: on ℕ, > collapses to ≥ with successor, so both
have HasMaxInf. On dense scales, > yields an open set with no max⊨.
This is the UDM prediction (@cite{fox-2007} §2).
Degree property for "exactly d": the measure at w equals d.
Equations
- Core.Scale.eqDeg μ d w = (μ w = d)
Instances For
Degree property for "at least d": the measure at w meets or exceeds d.
Equations
- Core.Scale.atLeastDeg μ d w = (μ w ≥ d)
Instances For
Degree property for "more than d": the measure strictly exceeds d.
Equations
- Core.Scale.moreThanDeg μ d w = (μ w > d)
Instances For
Degree property for "at most d": the measure at w is at most d.
Equations
- Core.Scale.atMostDeg μ d w = (μ w ≤ d)
Instances For
Degree property for "less than d": the measure is strictly less than d.
Equations
- Core.Scale.lessThanDeg μ d w = (μ w < d)
Instances For
"At least" is downward monotone: weaker thresholds are easier to satisfy.
"More than" is downward monotone: weaker thresholds are easier to satisfy.
"At least d" always has a maximally informative element: d₀ = μ(w).
This holds on ANY scale — dense or discrete — because the actual value μ(w) is always in the domain and "at least μ(w)" entails "at least d" for all d ≤ μ(w) by transitivity.
This is why bare numerals generate scalar implicatures regardless
of scale density: the ≥ relation creates a closed set with a
natural maximum at the true value.
Implicature asymmetry (@cite{fox-2007} §2): on a dense scale, "more than n" has NO maximally informative element.
For any candidate d₀ < μ(w), density gives d' ∈ (d₀, μ(w)). A witness world w₁ with μ(w₁) ∈ (d₀, d') has "more than d₀" true but "more than d'" false — so d₀ does not entail d'.
The hSurj hypothesis says every degree value is realized by some
possible world.
Kennedy–F&H bridge: IsMaxInf of the "at least" degree property
at value m and world w holds iff the measure at w equals m.
On ℕ, > collapses to ≥ with successor: "more than m" ↔ "at least m+1".
This is the discrete equivalence that density breaks.
On ℕ, "more than m" has HasMaxInf: the discrete collapse rescues maximality.
Contrast with moreThan_noMaxInf: on dense scales, HasMaxInf fails.
Scale-sensitive maximality operator #
@cite{rett-2026}: MAX_R(X) picks the element(s)
of X that R-dominate all other members. For the < scale this is the GLB
(earliest / smallest), for > the LUB (latest / largest). The same operator
underlies both temporal connectives (before/after) and degree comparatives.
- Rett, J. (2026). Semantic ambivalence and expletive negation. Ms.
Order-sensitive maximality (@cite{rett-2026}, def. 1): MAX_R(X) = { x ∈ X | ∀ x' ∈ X, x' ≠ x → R x x' }. Domain-general over any relation R and set X.
Instances For
MAX on a singleton is that singleton: MAX_R({x}) = {x}. The universal quantifier is vacuously satisfied.
MAX₍<₎ on a closed interval {x | s ≤ x ∧ x ≤ f} is the singleton {s}.
The minimum element s R-dominates all others on the < scale.
Dual: MAX₍>₎ on the same interval is {f}.
MAX₍>₎ on a closed interval {x | s ≤ x ∧ x ≤ f} is the singleton {f}.
The maximum element R-dominates all others on the > scale.
A scalar construction f is ambidirectional iff applying f to a set B and to its complement Bᶜ yields the same result, because MAX picks the same informative boundary from both. This is the mechanism behind expletive negation licensing: when f(B) ↔ f(Bᶜ), negating B is truth-conditionally vacuous.
Equations
- Core.Scale.isAmbidirectional f B = (f B ↔ f Bᶜ)
Instances For
Bridge: maxOnScale (· ≥ ·) applied to the "at least" degree set
{d | d ≤ μ(w)} yields {μ(w)} — the singleton containing the true
value. This connects the relational MAX to IsMaxInf.
The convention: maxOnScale R X picks elements x ∈ X with R x x' for
all other x'. With R = (· ≥ ·), this picks elements ≥ all others,
i.e., the maximum.
MAX₍≥₎ on {d | d ≤ b} is {b}. Corollary of maxOnScale_atLeast_singleton
with μ = id. Used by the comparative boundary theorems.
"At most" is upward monotone: larger thresholds are easier to satisfy.
"At most d" always has a maximally informative element: d₀ = μ(w).
Symmetric to atLeast_hasMaxInf.
Kennedy–Rouillard bridge: IsMaxInf of "at most d" at value m and
world w holds iff the measure at w equals m. Symmetric to
isMaxInf_atLeast_iff_eq: the MIP derives exact meaning from "at most"
just as it does from "at least".
The Maximal Informativity Principle as a universal mechanism #
@cite{kennedy-2015} proposes a de-Fregean type-shift that maps lower-bound numeral meanings to exact meanings for Class B items (closed scales). @cite{rouillard-2026} proposes the MIP as the licensing condition for temporal in-adverbials.
These are the SAME mechanism: given a measure function μ and a monotone degree property P, the maximally informative value is always μ(w) — the true value. The MIP derives exactness from monotone degree properties regardless of domain:
| Domain | μ | Degree prop | Direction | MIP result |
|---|---|---|---|---|
| Kennedy numerals | cardinality | atLeastDeg | down mono | max⊨ = μ(w) |
| Kennedy adjectives | degree | atLeastDeg | down mono | max⊨ = μ(w) |
| Rouillard E-TIAs | runtime | atMostDeg | up mono | max⊨ = μ(w) |
The isMaxInf_atLeast_iff_eq and isMaxInf_atMost_iff_eq theorems prove this
for both monotonicity directions. The Kennedy type-shift is not a separate
mechanism — it IS the MIP applied to "at least n".
@cite{kennedy-2015} numeral domain: "at least n" over cardinality. Closed scale (ℕ well-ordered) → always licensed. Type-shift to exact = MIP applied to atLeastDeg.
Equations
- Core.Scale.DirectedMeasure.kennedyNumeral μ = { boundedness := Core.Scale.Boundedness.closed, μ := μ }
Instances For
@cite{kennedy-2007} gradable adjective domain. Boundedness varies by adjective class (tall: open, full: closed).
Equations
- Core.Scale.DirectedMeasure.kennedyAdjective μ b = { boundedness := b, μ := μ }
Instances For
@cite{rouillard-2026} E-TIA domain: event runtime ≤ interval size. Boundedness determined by Vendler class (telic → closed, atelic → open).
Equations
- Core.Scale.DirectedMeasure.rouillardETIA μ b = { boundedness := b, μ := μ, direction := Core.Scale.ScalePolarity.negative }
Instances For
@cite{rouillard-2026} G-TIA domain: PTS extent on open intervals. Always open → always blocked (information collapse).
Equations
- Core.Scale.DirectedMeasure.rouillardGTIA μ = { boundedness := Core.Scale.Boundedness.open_, μ := μ, direction := Core.Scale.ScalePolarity.negative }
Instances For
Kennedy numeral domains are always licensed (closed scale).
Kennedy Class B adjectives (closed scale) are licensed.
Kennedy Class A adjectives (open scale) are blocked.
Rouillard telic E-TIAs are licensed (closed runtime scale).
Rouillard atelic E-TIAs are blocked (open runtime scale).
Rouillard G-TIAs are always blocked (open PTS).
The deep isomorphism: a Kennedy numeral domain and a Rouillard E-TIA domain on a closed scale have identical licensing, despite using opposite directions (positive vs negative).
All four frameworks agree: licensing depends solely on boundedness. @cite{kennedy-2007}: closed-scale adjectives license degree modifiers. @cite{rouillard-2026}: closed-runtime VPs license E-TIAs. @cite{krifka-1989}: QUA predicates yield telic (bounded) VPs. @cite{zwarts-2005}: bounded paths yield telic VPs. All four route through Boundedness.isLicensed.
The punchline: Kennedy's de-Fregean type-shift is not a separate mechanism. It IS the MIP applied to a monotone degree property. For both "at least" (Kennedy) and "at most" (Rouillard), max⊨ at world w = μ(w), the true value. So the MIP universally derives exact meaning from monotone degree properties, regardless of monotonicity direction.
`isMaxInf_atLeast_iff_eq`: max⊨(atLeastDeg μ, m, w) ↔ μ(w) = m
`isMaxInf_atMost_iff_eq`: max⊨(atMostDeg μ, m, w) ↔ μ(w) = m
Both directions yield `eqDeg μ m w` — exact meaning.
MIP derives exact meaning from "at least" (Kennedy's direction).
MIP derives exact meaning from "at most" (Rouillard's direction).
The MIP is direction-invariant: "at least" and "at most" yield the same exact meaning under maximal informativity. Kennedy's type-shift and Rouillard's MIP are literally the same operation.
Degree and Threshold types for finite scales #
Discretized scale types for gradable adjective RSA computations.
Degree max wraps Fin (max + 1) with LinearOrder, BoundedOrder, Fintype.
Threshold max wraps Fin max with coercion to Degree max.
These participate in the abstract DirectedMeasure infrastructure above via their
LinearOrder and BoundedOrder instances.
Equations
- Core.Scale.instReprDegree = { reprPrec := Core.Scale.instReprDegree.repr }
Equations
- Core.Scale.instReprDegree.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"
Instances For
Equations
All degrees from 0 to max
Equations
- Core.Scale.allDegrees max = List.map (fun (x : Fin (max + 1)) => { value := x }) (List.finRange (max + 1))
Instances For
A threshold for a gradable adjective. x is "tall" iff degree(x) > threshold.
- value : Fin max
Instances For
Equations
- Core.Scale.instReprThreshold.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"
Instances For
Equations
- Core.Scale.instReprThreshold = { reprPrec := Core.Scale.instReprThreshold.repr }
Equations
All thresholds from 0 to max-1
Equations
- Core.Scale.allThresholds max x✝ = List.map (fun (x : Fin max) => { value := x }) (List.finRange max)
Instances For
Equations
- Core.Scale.instFintypeDegree = Fintype.ofEquiv (Fin (max + 1)) { toFun := Core.Scale.Degree.mk, invFun := Core.Scale.Degree.value, left_inv := ⋯, right_inv := ⋯ }
Equations
- Core.Scale.instFintypeThresholdOfNeZeroNat = Fintype.ofEquiv (Fin max) { toFun := Core.Scale.Threshold.mk, invFun := Core.Scale.Threshold.value, left_inv := ⋯, right_inv := ⋯ }
Coercion: Threshold embeds into Degree via Fin.castSucc
Equations
- Core.Scale.instCoeThresholdDegree = { coe := fun (t : Core.Scale.Threshold max) => { value := t.value.castSucc } }
Kennedy positive region: degree d is in the positive region given
threshold θ iff θ < d (i.e., the degree exceeds the threshold).
Equations
- Core.Scale.instPositiveRegionDegreeThreshold = { inRegion := fun (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) => decide ({ value := θ.value.castSucc } < d) }
Typeclass for entities that have a degree/magnitude on some scale. This is the formal semantics "measure function" μ : Entity → Degree.
- degree : E → ℚ