Two-Dimensional Alternative Meanings

@cite{rooth-1985} @cite{rooth-1992} @cite{kratzer-selkirk-2020}

The O-value / A-value pair from Rooth-style alternative semantics. Every expression has an ordinary denotation (oValue) and an alternatives set (aValue); focus features and operators manipulate the latter while typically preserving the former.

This file isolates the bare data structure. Categorical refinements (@cite{fox-katzir-2011}) live in Categorical.lean; structural alternatives (@cite{katzir-2007}) live in Structural.lean; [FoC]/[G] feature semantics live in Theories/Semantics/Focus/.

structure Semantics.Alternatives.AltMeaning (α : Type) : Type

Two-dimensional meaning in @cite{rooth-1992}-style alternative semantics. Every expression has an O-value and an A-value.

@cite{kratzer-selkirk-2020} §3, §8.

• oValue : α

  O(rdinary)-value: the actual denotation

• aValue : List α

  A(lternatives)-value: the set of alternatives (including oValue)

def Semantics.Alternatives.AltMeaning.unfeatured {α : Type} (x : α) : AltMeaning α

The O-value of a non-featured expression equals its ordinary denotation. The A-value of a non-featured expression is a singleton containing its O-value (no alternatives evoked).

Equations

• Semantics.Alternatives.AltMeaning.unfeatured x = { oValue := x, aValue := [x] }

@[simp]

theorem Semantics.Alternatives.AltMeaning.unfeatured_oValue {α : Type} (x : α) : (unfeatured x).oValue = x

@[simp]

theorem Semantics.Alternatives.AltMeaning.unfeatured_aValue {α : Type} (x : α) : (unfeatured x).aValue = [x]