Documentation

Linglib.Theories.Semantics.Lexical.Adjective.Aggregation

Adjective–Aggregation Bridge #

Re-exports general aggregation mechanisms from Semantics.Degree.Aggregation and proves that @cite{sassoon-2013}'s binding types (conjunctive, disjunctive, mixed) are all counting aggregation — a single escape route from Arrow's impossibility theorem (@cite{dambrosio-hedden-2024}).

source
theorem Semantics.Lexical.Adjective.Aggregation.conjunctive_is_countAll {α : Type} (dims : List (α → Bool)) (x : α) :
conjunctiveBinding dims x = countBinding dims.length dims x

Conjunctive binding = counting with threshold k = dims.length. @cite{sassoon-2013}'s ∀-binding is a special case of counting.

source
theorem Semantics.Lexical.Adjective.Aggregation.disjunctive_is_countOne {α : Type} (dims : List (α → Bool)) (x : α) :
disjunctiveBinding dims x = countBinding 1 dims x

Disjunctive binding = counting with threshold k = 1. @cite{sassoon-2013}'s ∃-binding is a special case of counting.

source
def Semantics.Lexical.Adjective.Aggregation.toAggregationType :
DimensionBindingType → AggregationType

@cite{sassoon-2013}'s binding types all map to counting aggregation. The key gap: Sassoon has no utilitarian or Cobb-Douglas mechanism.

Equations
Instances For
    source
    theorem Semantics.Lexical.Adjective.Aggregation.sassoon_all_counting (b : DimensionBindingType) :
    toAggregationType b = Degree.Aggregation.AggregationType.counting

    All of Sassoon 2013's binding types are counting aggregation.