Alternative sources

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

• [Kat07] structural alternatives — substitution/deletion/ contraction over a parse tree, using items in the lexicon ∪ subtrees
• [BKC18] conceptual alternatives — including competitors not realizable by linguistic material
• [SA20] Meaning First — alternatives drawn at the thought-structure level, prior to compression
• [JBG+25] indirect alternatives — pronounceable expressions equivalent in meaning to an unpronounceable Katzir alternative

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

This follows mathlib's pattern of naming a function-shaped abstraction under a structural alias (cf. Set α := α → Prop, Rel α β := α → β → Prop) rather than as a typeclass — there is no canonical alternative source per carrier type, since different theories supply different sources for the same parse. The alias also inherits the pointwise CompleteLattice on S → Set S for free, so source subsumption is just ≤ (pointwise ⊆) and source union is ⊔.

Main definitions

• Source — the alternative-source abbreviation S → Set S.
• indirectFrom — the indirect-alternative combinator: pronounceable expressions meaning-equivalent to an unpronounceable alternative of the original, at most as complex ([JBG+25]).

Main results

• mem_indirectFrom — membership characterization of indirectFrom.
• size_le_of_mem — indirect alternatives are at most as complex as the original.
• indirectFrom_eq_empty_of_forall_pron — indirectFrom is empty when the base has no unpronounceable witness.

@[reducible, inline]

abbrev Alternatives.Source (S : Type u_1) : Type u_1

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

Theory-specific base sources live elsewhere: Alternatives.Structural.katzirSource (Katzir 2007), Alternatives.HornScale.toSource (Horn scales), etc. The combinator indirectFrom below transforms any base source.

Equations

• Alternatives.Source S = (S → Set S)

def Alternatives.indirectFrom {S : Type u_1} {M : Type u_2} (base : Source S) (pron : S → Prop) (meaning : S → M) (size : S → ℕ) : Source S

The indirect-alternative combinator (eq. 43, [JBG+25]).

indirectFrom base pron meaning size s is the set of pronounceable expressions s' such that size s' ≤ size s and there is some unpronounceable sₓ ∈ base s with meaning s' = meaning sₓ.

Parameters:

• base: the underlying alternative source (typically Katzir).
• pron: the pronounceability predicate; an expression is silent when ¬ pron s holds.
• meaning: the semantic interpretation function.
• size: complexity measure (e.g. Tree.size).

Both the surrogate s' (the indirect alternative I) and the witness sₓ are constrained by pron: I must be pronounceable while sₓ — the silent structural alternative it stands in for — must not be, per the paper's definition.

Equations

• Alternatives.indirectFrom base pron meaning size s = {s' : S | pron s' ∧ size s' ≤ size s ∧ ∃ (sₓ : S), sₓ ∈ base s ∧ ¬pron sₓ ∧ meaning s' = meaning sₓ}

@[simp]

theorem Alternatives.mem_indirectFrom {S : Type u_1} {M : Type u_2} {base : Source S} {pron : S → Prop} {meaning : S → M} {size : S → ℕ} {s' s : S} : s' ∈ indirectFrom base pron meaning size s ↔ pron s' ∧ size s' ≤ size s ∧ ∃ (sₓ : S), sₓ ∈ base s ∧ ¬pron sₓ ∧ meaning s' = meaning sₓ

Membership in the indirect-alternative source.

theorem Alternatives.size_le_of_mem {S : Type u_1} {M : Type u_2} {base : Source S} {pron : S → Prop} {meaning : S → M} {size : S → ℕ} {s' s : S} (h : s' ∈ indirectFrom base pron meaning size s) : size s' ≤ size s

Indirect alternatives are at most as complex as the original.

theorem Alternatives.indirectFrom_eq_empty_of_forall_pron {S : Type u_1} {M : Type u_2} {base : Source S} {pron : S → Prop} {meaning : S → M} {size : S → ℕ} {s : S} (allPron : ∀ (x : S), x ∈ base s → pron x) : indirectFrom base pron meaning size s = ∅

The indirect-alternative set is empty when the base source contains no unpronounceable witnesses — the genuine refinement: an indirect alternative requires a silent witness in the base.