Documentation

Linglib.Theories.Semantics.Alternatives.Source

Alternative Sources #

A common abstraction over the many "alternative-generation" mechanisms in formal pragmatics. Different theories generate different competitor sets for the same expression:

All of these are functions S → Set S. We give that function type a name so that pragmatic competition operators (violatesMP, violatesMaximize, violatesMCIs, violatesAvoidAmbiguity) can be parameterized over the alternative source rather than hardcoding any single one.

This follows mathlib's pattern of bundling a function-shaped abstraction under a structural alias (cf. Filter, Order.Hom) rather than as a typeclass — there is no canonical alternative source per carrier type, since different theories supply different sources for the same parse.

@[reducible, inline]

An alternative source assigns to each expression a set of competitors.

Theory-specific instances of this signature live elsewhere: Alternatives.Structural.katzirSource (Katzir 2007), Alternatives.Indirect.indirectFrom (Jeretič et al. 2025), etc.

Equations
Instances For