Traditional HAB Operator and Threshold Semantics

@cite{carlson-1977} @cite{krifka-etal-1995} @cite{bhatt-1999}

Traditional HAB operator and frequency-based threshold semantics for habituals. HAB quantifies over "characteristic" occasions; threshold semantics replaces this with observable frequency > θ, where θ is pragmatically inferred.

HAB is an instance of the shared covert quantifier infrastructure in CovertQuantifier.lean: traditionalHAB = covertQ with D = Occasion, restriction = characteristic, scope = activity.

structure Semantics.Lexical.Verb.Habituals.Occasion : Type

A time interval or occasion for habitual quantification.

• id : ℕ

def Semantics.Lexical.Verb.Habituals.instDecidableEqOccasion.decEq (x✝ x✝¹ : Occasion) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Lexical.Verb.Habituals.instDecidableEqOccasion.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Verb.Habituals.instDecidableEqOccasion : DecidableEq Occasion

Equations

• Semantics.Lexical.Verb.Habituals.instDecidableEqOccasion = Semantics.Lexical.Verb.Habituals.instDecidableEqOccasion.decEq

instance Semantics.Lexical.Verb.Habituals.instReprOccasion : Repr Occasion

Equations

• Semantics.Lexical.Verb.Habituals.instReprOccasion = { reprPrec := Semantics.Lexical.Verb.Habituals.instReprOccasion.repr }

def Semantics.Lexical.Verb.Habituals.instReprOccasion.repr : Occasion → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.Habituals.instInhabitedOccasion : Inhabited Occasion

Equations

• Semantics.Lexical.Verb.Habituals.instInhabitedOccasion = { default := { id := 0 } }

@[reducible, inline]

abbrev Semantics.Lexical.Verb.Habituals.Activity : Type

An activity predicate (what John does at an occasion).

Equations

• Semantics.Lexical.Verb.Habituals.Activity = (Semantics.Lexical.Verb.Habituals.Occasion → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Verb.Habituals.Characteristic : Type

A characteristicness predicate (which occasions are "typical").

Equations

• Semantics.Lexical.Verb.Habituals.Characteristic = (Semantics.Lexical.Verb.Habituals.Occasion → Bool)

def Semantics.Lexical.Verb.Habituals.traditionalHAB (occasions : List Occasion) (characteristic : Characteristic) (activity : Activity) : Bool

Traditional HAB: ∀t. characteristic(t) → activity(t).

This is definitionally equal to covertQ occasions characteristic activity.

Equations

• Semantics.Lexical.Verb.Habituals.traditionalHAB occasions characteristic activity = occasions.all fun (t : Semantics.Lexical.Verb.Habituals.Occasion) => !characteristic t || activity t

theorem Semantics.Lexical.Verb.Habituals.hab_is_covertQ (occasions : List Occasion) (characteristic : Characteristic) (activity : Activity) : traditionalHAB occasions characteristic activity = CovertQuantifier.covertQ occasions characteristic activity

HAB is an instance of the shared covert quantifier.

def Semantics.Lexical.Verb.Habituals.traditionalHAB_existential (occasions : List Occasion) (characteristic : Characteristic) (activity : Activity) : Bool

Alternative: existential characterization of non-habitual.

Equations

• Semantics.Lexical.Verb.Habituals.traditionalHAB_existential occasions characteristic activity = !occasions.any fun (t : Semantics.Lexical.Verb.Habituals.Occasion) => characteristic t && !activity t

theorem Semantics.Lexical.Verb.Habituals.hab_formulations_equiv (occasions : List Occasion) (characteristic : Characteristic) (activity : Activity) : traditionalHAB occasions characteristic activity = traditionalHAB_existential occasions characteristic activity

The two formulations are equivalent (derived from shared De Morgan proof).

def Semantics.Lexical.Verb.Habituals.frequency (occasions : List Occasion) (activity : Activity) : ℚ

Frequency of an activity: proportion of occasions where it occurs.

Defined as measure with trivial restriction (all occasions count).

Equations

• Semantics.Lexical.Verb.Habituals.frequency occasions activity = Semantics.Lexical.CovertQuantifier.measure occasions (fun (x : Semantics.Lexical.Verb.Habituals.Occasion) => true) activity

def Semantics.Lexical.Verb.Habituals.thresholdHabitual (occasions : List Occasion) (activity : Activity) (threshold : ℚ) : Bool

Threshold-based habitual: true iff frequency exceeds threshold.

Equations

• Semantics.Lexical.Verb.Habituals.thresholdHabitual occasions activity threshold = decide (Semantics.Lexical.Verb.Habituals.frequency occasions activity > threshold)

theorem Semantics.Lexical.Verb.Habituals.hab_reduces_to_threshold (occasions : List Occasion) (characteristic : Characteristic) (activity : Activity) (_hNonEmpty : occasions.length > 0) : ∃ (θ : ℚ), traditionalHAB occasions characteristic activity = thresholdHabitual occasions activity θ

For any HAB configuration, there exists a matching threshold giving the same truth value.

Proof sketch: both sides are Bool, so we case-split. When HAB = true, pick θ = frequency − 1 (any value beats its predecessor); when HAB = false, pick θ = frequency (strict self-comparison is false). This is an expressiveness result: threshold semantics can simulate any HAB outcome, though not vice versa (it loses the characteristic-occasion structure).

inductive Semantics.Lexical.Verb.Habituals.ActivityType : Type

Activity types with different frequency expectations.

• neutral : ActivityType
• occupation : ActivityType
• striking : ActivityType
• achievement : ActivityType

instance Semantics.Lexical.Verb.Habituals.instDecidableEqActivityType : DecidableEq ActivityType

Equations

• Semantics.Lexical.Verb.Habituals.instDecidableEqActivityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.Habituals.instReprActivityType.repr : ActivityType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.Habituals.instReprActivityType : Repr ActivityType

Equations

• Semantics.Lexical.Verb.Habituals.instReprActivityType = { reprPrec := Semantics.Lexical.Verb.Habituals.instReprActivityType.repr }

def Semantics.Lexical.Verb.Habituals.expectedThreshold : ActivityType → ℚ

Expected frequency threshold by activity type.

Equations

• Semantics.Lexical.Verb.Habituals.expectedThreshold Semantics.Lexical.Verb.Habituals.ActivityType.neutral = 8 / 10
• Semantics.Lexical.Verb.Habituals.expectedThreshold Semantics.Lexical.Verb.Habituals.ActivityType.occupation = 5 / 10
• Semantics.Lexical.Verb.Habituals.expectedThreshold Semantics.Lexical.Verb.Habituals.ActivityType.striking = 1 / 100
• Semantics.Lexical.Verb.Habituals.expectedThreshold Semantics.Lexical.Verb.Habituals.ActivityType.achievement = 0

def Semantics.Lexical.Verb.Habituals.occasions : List Occasion

Equations

• Semantics.Lexical.Verb.Habituals.occasions = [{ id := 0 }, { id := 1 }, { id := 2 }, { id := 3 }, { id := 4 }, { id := 5 }, { id := 6 }, { id := 7 }, { id := 8 }, { id := 9 }]

def Semantics.Lexical.Verb.Habituals.johnSmokesActivity : Activity

Equations

• Semantics.Lexical.Verb.Habituals.johnSmokesActivity t = decide (t.id ∈ [0, 1, 2, 4, 5, 8])

def Semantics.Lexical.Verb.Habituals.normalOccasions : Characteristic

Equations

• Semantics.Lexical.Verb.Habituals.normalOccasions t = decide (t.id ∈ [0, 1, 2, 3, 4, 5, 6, 7])