Core.InformationStructure

@cite{fox-katzir-2011} @cite{rooth-1992} @cite{steedman-2000} @cite{roberts-2012}

Theory-neutral types for Information Structure, alternative semantics, and discourse status.

Overview

Information Structure partitions utterances along two orthogonal dimensions:

1. Theme/Rheme (topic/comment): What's being talked about vs. what's said about it
2. Focus/Background: What's contrasted vs. what's given

This module provides descriptive types and basic data structures. Theory-specific operations (K&S's [FoC]/[G] features, their semantic effects) live in Theories/Semantics/Focus/KratzerSelkirk2020.lean.

structure Core.InformationStructure.AltMeaning (α : Type) : Type

Two-dimensional meaning in Alternatives 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 Core.InformationStructure.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

• Core.InformationStructure.AltMeaning.unfeatured x = { oValue := x, aValue := [x] }

structure Core.InformationStructure.CatItem (α : Type) : Type

A denotation tagged with its UPOS category. Pairs a semantic value with a UD part-of-speech tag, enabling category-gated alternative computation.

Fox & Katzir argue that @cite{rooth-1985} type-theoretic alternative computation (D_τ) over-generates: any expression of the same semantic type counts as an alternative. Category match restricts alternatives to expressions sharing the same UPOS tag.

• cat : UD.UPOS

  The UPOS category of this lexical item

• den : α

  The semantic denotation

instance Core.InformationStructure.instReprCatItem {α✝ : Type} [Repr α✝] : Repr (CatItem α✝)

Equations

• Core.InformationStructure.instReprCatItem = { reprPrec := Core.InformationStructure.instReprCatItem.repr }

def Core.InformationStructure.instReprCatItem.repr {α✝ : Type} [Repr α✝] : CatItem α✝ → ℕ → Std.Format

Equations

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

def Core.InformationStructure.categoryMatchAlts {α : Type} (target : UD.UPOS) (lexicon : List (CatItem α)) : List α

Category-match alternatives: only denotations with the same UPOS tag count as alternatives.

This is strictly more restrictive than Rooth's D_τ computation.

Equations

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

def Core.InformationStructure.typeTheoAlts {α : Type} (lexicon : List (CatItem α)) : List α

Type-theoretic alternatives: all denotations regardless of category (@cite{rooth-1985}/1992 D_τ computation).

Equations

• Core.InformationStructure.typeTheoAlts lexicon = List.map (fun (x : Core.InformationStructure.CatItem α) => x.den) lexicon

structure Core.InformationStructure.Theme (P : Type) : Type

Theme: what the utterance is about (the "topic" or "given" part).

The theme:

• Presupposes a QUD (set of alternatives)
• Is often prosodically marked (L+H* LH% in English)
• Corresponds to the λ-abstract in structured meanings

Example: In "FRED ate the beans" (answering "Who ate the beans?"), the theme is "λx. ate(x, beans)" or informally "_ ate the beans".

• content : P

  The thematic content (often a property/λ-abstract)

• marked : Bool

  Whether the theme is prosodically marked

structure Core.InformationStructure.Rheme (P : Type) : Type

Rheme: what's asserted about the theme (the "comment" or "new" part).

The rheme:

• Restricts the QUD alternatives to one
• Is often prosodically marked (H* LL% in English)
• Provides the "answer" to the implicit question

Example: In "FRED ate the beans", the rheme is "Fred".

• content : P

  The rhematic content

• marked : Bool

  Whether the rheme is prosodically marked

structure Core.InformationStructure.Focus (α : Type) : Type

Focus: the contrasted element(s) within theme or rheme.

Focus is marked by pitch accent and:

• Evokes alternatives (Rooth)
• Associates with focus-sensitive particles (only, even)
• Determines the "question" being answered

Focus is orthogonal to theme/rheme: both can contain focused elements.

• focused : α

  The focused element

• alternatives : List α

  Alternatives evoked by focus (including the focused element)

structure Core.InformationStructure.Background (α : Type) : Type

Background: the non-focused, given material.

Background material is:

• Not pitch-accented
• Presupposed to be salient in context
• Often recoverable/predictable

• elements : List α

  The background elements

structure Core.InformationStructure.InfoStructure (P : Type) : Type

A complete Information Structure analysis of an utterance.

Partitions the utterance into:

• Theme vs. Rheme (what's talked about vs. what's said)
• Focus vs. Background (within each)

• theme : Theme P

  The theme (topic, λ-abstract, presupposed QUD)

• rheme : Rheme P

  The rheme (comment, answer, assertion)

• foci : List P

  Focused elements (evoking alternatives)

• background : List P

  Background elements (given)

class Core.InformationStructure.HasInfoStructure (D P : Type) : Type

Typeclass for theories that provide Information Structure.

Implementations:

• CCG/Intonation: prosodic realization
• (Future) Syntactic approaches, discourse models

The key insight: different surface forms (derivations, prosody) can map to the same propositional content but different Information Structures.

• infoStructure : D → InfoStructure P

  Extract Information Structure from a derivation/form

inductive Core.InformationStructure.DiscourseStatus : Type

The three-way partition of discourse status. Descriptive type used across multiple theories (@cite{kratzer-selkirk-2020}, @cite{arnold-wasow-losongco-ginstrom-2000}, backgrounded islands).

• focused : DiscourseStatus

  Contrasted with discourse referent

• given : DiscourseStatus

  Given, matching discourse referent

• new : DiscourseStatus

  Unmarked: merely new information

instance Core.InformationStructure.instDecidableEqDiscourseStatus : DecidableEq DiscourseStatus

Equations

• Core.InformationStructure.instDecidableEqDiscourseStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.InformationStructure.instReprDiscourseStatus.repr : DiscourseStatus → ℕ → Std.Format

Equations

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

instance Core.InformationStructure.instReprDiscourseStatus : Repr DiscourseStatus

Equations

• Core.InformationStructure.instReprDiscourseStatus = { reprPrec := Core.InformationStructure.instReprDiscourseStatus.repr }

instance Core.InformationStructure.instBEqDiscourseStatus : BEq DiscourseStatus

Equations

• Core.InformationStructure.instBEqDiscourseStatus = { beq := Core.InformationStructure.instBEqDiscourseStatus.beq }

def Core.InformationStructure.instBEqDiscourseStatus.beq : DiscourseStatus → DiscourseStatus → Bool

Equations

• Core.InformationStructure.instBEqDiscourseStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.InformationStructure.DiscourseStatus.rank : DiscourseStatus → Fin 3

Ordinal rank: given < new < focused. Used by extraction-acceptability theories (@cite{lu-degen-2025}) and focus-comparison constraints (@cite{winckel-et-al-2025}).

Equations

• Core.InformationStructure.DiscourseStatus.given.rank = 0
• Core.InformationStructure.DiscourseStatus.new.rank = 1
• Core.InformationStructure.DiscourseStatus.focused.rank = 2

def Core.InformationStructure.DiscourseStatus.ofAtIssueness (d : Discourse.AtIssueness.AtIssuenessDegree) (θ : Discourse.AtIssueness.AtIssuenessThreshold := Discourse.AtIssueness.defaultThreshold) : DiscourseStatus

Map gradient at-issueness to discourse status.

High at-issueness content is foregrounded (new or focused); low at-issueness content is backgrounded (given). This connects the at-issue/not-at-issue distinction to the Focus/Background partition.

• At-issue → .new (unmarked foreground; .focused requires additional evidence of contrast)
• Not-at-issue → .given (backgrounded)

Equations

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

Polarity-Switch Contexts

@cite{turco-braun-dimroth-2014} distinguish two discourse contexts for polarity switches (negation → affirmation). The distinction is theory-neutral: it characterizes the discourse relation between the antecedent and the target utterance, independent of how languages mark the switch.

• @cite{klein-2008}: contrast = different topic situations, compatible claims
• @cite{umbach-2004}: correction = same topic situation, mutually exclusive claims

inductive Core.InformationStructure.PolaritySwitchContext : Type

The discourse context in which a polarity switch (neg → affirm) occurs. Crosslinguistically relevant: Dutch and German mark both contexts but with different strategies.

This is the information-structural reflex of the discourse-structural distinction between CoherenceRelation.contrast and CoherenceRelation.correction (@cite{umbach-2004} §3).

• contrast : PolaritySwitchContext

  Different topic situations, compatible claims

• correction : PolaritySwitchContext

  Same topic situation, mutually exclusive claims

instance Core.InformationStructure.instDecidableEqPolaritySwitchContext : DecidableEq PolaritySwitchContext

Equations

• Core.InformationStructure.instDecidableEqPolaritySwitchContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.InformationStructure.instReprPolaritySwitchContext : Repr PolaritySwitchContext

Equations

• Core.InformationStructure.instReprPolaritySwitchContext = { reprPrec := Core.InformationStructure.instReprPolaritySwitchContext.repr }

def Core.InformationStructure.instReprPolaritySwitchContext.repr : PolaritySwitchContext → ℕ → Std.Format

Equations

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

def Core.InformationStructure.instBEqPolaritySwitchContext.beq : PolaritySwitchContext → PolaritySwitchContext → Bool

Equations

• Core.InformationStructure.instBEqPolaritySwitchContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.InformationStructure.instBEqPolaritySwitchContext : BEq PolaritySwitchContext

Equations

• Core.InformationStructure.instBEqPolaritySwitchContext = { beq := Core.InformationStructure.instBEqPolaritySwitchContext.beq }

def Core.InformationStructure.PolaritySwitchContext.toCoherenceRelation : PolaritySwitchContext → Discourse.CoherenceRelation.CoherenceRelation

Bridge from polarity-switch contexts to discourse coherence relations. @cite{umbach-2004} §3: the contrast/correction distinction in information structure corresponds directly to two distinct resemblance relations at the discourse level.

Equations

• Core.InformationStructure.PolaritySwitchContext.contrast.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.contrast
• Core.InformationStructure.PolaritySwitchContext.correction.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.correction

inductive Core.InformationStructure.PolarityMarkingStrategy : Type

How a language marks polarity switches (neg → affirm). Theory-neutral inventory: individual languages select a subset.

• particle : PolarityMarkingStrategy

  Sentence-internal affirmative particle (e.g., Dutch wel)

• verumFocus : PolarityMarkingStrategy

  Pitch accent on the finite verb (@cite{hohle-1992} Verum focus)

• polarityReversal : PolarityMarkingStrategy

  Polarity-reversing particle: affirms [+Pol] while contradicting a negative context (e.g., German doch, Swedish jo, French si; @cite{holmberg-2016})

• other : PolarityMarkingStrategy

  Other strategy (e.g., pre-utterance particle, intonation pattern)

• unmarked : PolarityMarkingStrategy

  No overt polarity marking

instance Core.InformationStructure.instDecidableEqPolarityMarkingStrategy : DecidableEq PolarityMarkingStrategy

Equations

• Core.InformationStructure.instDecidableEqPolarityMarkingStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.InformationStructure.instReprPolarityMarkingStrategy : Repr PolarityMarkingStrategy

Equations

• Core.InformationStructure.instReprPolarityMarkingStrategy = { reprPrec := Core.InformationStructure.instReprPolarityMarkingStrategy.repr }

def Core.InformationStructure.instReprPolarityMarkingStrategy.repr : PolarityMarkingStrategy → ℕ → Std.Format

Equations

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

instance Core.InformationStructure.instBEqPolarityMarkingStrategy : BEq PolarityMarkingStrategy

Equations

• Core.InformationStructure.instBEqPolarityMarkingStrategy = { beq := Core.InformationStructure.instBEqPolarityMarkingStrategy.beq }

def Core.InformationStructure.instBEqPolarityMarkingStrategy.beq : PolarityMarkingStrategy → PolarityMarkingStrategy → Bool

Equations

• Core.InformationStructure.instBEqPolarityMarkingStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Core.InformationStructure.PolarityMarkingEntry : Type

A cross-linguistic polarity-marking entry.

Unified structure for all strategies — particles (Dutch wel), prosodic (German VF), or other. Language-specific Fragment files instantiate this with appropriate optional fields.

• label : String

  Descriptive label (e.g., "wel", "Verum focus", "doch (pre-utterance)")

• form : Option String

  Surface form, if the strategy is a particle

• prosodicTarget : Option String

  What bears prosodic prominence, if the strategy is prosodic

• sentenceInternal : Bool

  Whether the marker appears sentence-internally (vs. pre-utterance)

• contrastOk : Bool

  Available in contrast contexts

• correctionOk : Bool

  Available in correction contexts

• strategy : PolarityMarkingStrategy

  The polarity-marking strategy category

instance Core.InformationStructure.instReprPolarityMarkingEntry : Repr PolarityMarkingEntry

Equations

• Core.InformationStructure.instReprPolarityMarkingEntry = { reprPrec := Core.InformationStructure.instReprPolarityMarkingEntry.repr }

def Core.InformationStructure.instReprPolarityMarkingEntry.repr : PolarityMarkingEntry → ℕ → Std.Format

Equations

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

def Core.InformationStructure.instDecidableEqPolarityMarkingEntry.decEq (x✝ x✝¹ : PolarityMarkingEntry) : Decidable (x✝ = x✝¹)

Equations

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

instance Core.InformationStructure.instDecidableEqPolarityMarkingEntry : DecidableEq PolarityMarkingEntry

Equations

• Core.InformationStructure.instDecidableEqPolarityMarkingEntry = Core.InformationStructure.instDecidableEqPolarityMarkingEntry.decEq

def Core.InformationStructure.instBEqPolarityMarkingEntry.beq : PolarityMarkingEntry → PolarityMarkingEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.InformationStructure.instBEqPolarityMarkingEntry.beq x✝¹ x✝ = false

instance Core.InformationStructure.instBEqPolarityMarkingEntry : BEq PolarityMarkingEntry

Equations

• Core.InformationStructure.instBEqPolarityMarkingEntry = { beq := Core.InformationStructure.instBEqPolarityMarkingEntry.beq }

Alternative Set Well-Formedness (@cite{umbach-2004} §2.2)

@cite{umbach-2004} identifies two constraints that jointly determine when elements can serve as alternatives (in focus, coordination, or discourse):

1. Semantic independence: neither alternative entails the other (dissimilarity). Explains why #John had a drink and Mary had a martini is odd — "drink" subsumes "martini".

2. Common integrator: a concept subsuming all alternatives (similarity). Explains why alternatives must be of a comparable type.

Together these define comparability = similarity + dissimilarity, which is the prerequisite for any type of contrast.

def Core.InformationStructure.semanticallyIndependent {W : Type} (a b : W → Bool) : Prop

Two propositions are semantically independent iff neither entails the other. @cite{umbach-2004} §2.2: required for alternatives in focus, coordination, and discourse relations. Violation explains the oddness of #John had a drink and Mary had a martini.

Equations

• Core.InformationStructure.semanticallyIndependent a b = ((¬∀ (w : W), a w = true → b w = true) ∧ ¬∀ (w : W), b w = true → a w = true)

def Core.InformationStructure.commonIntegrator {W : Type} (alts : List (W → Bool)) (integ : W → Bool) : Prop

A common integrator subsumes all alternatives. @cite{umbach-2004} §2.2, following @cite{lang-1984}: coordinated elements and focus alternatives must share a common superordinate concept. For example, in "beer and martini", "drink" is the common integrator.

Equations

• Core.InformationStructure.commonIntegrator alts integ = ∀ a ∈ alts, ∀ (w : W), a w = true → integ w = true

def Core.InformationStructure.wellFormedAlts {W : Type} (alts : List (W → Bool)) (integ : W → Bool) : Prop

A well-formed alternative set satisfies both constraints. @cite{umbach-2004} §2.2: alternatives must be comparable, i.e., similar (common integrator) and dissimilar (pairwise independent).

Equations

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

Exclusion Variety (@cite{umbach-2004} §2.3, §3.2)

@cite{umbach-2004} distinguishes two varieties of exclusion that cross-cut information structure and discourse structure:

• Additional: the excluded alternative would hold in addition to the asserted item. Instantiated by only-phrases (§2.3: "only RONALD went shopping" excludes anyone in addition to Ronald) and the discourse relation CONTRAST (§3.2: "Did John go to Berlin, and also to Paris?").
• Substitution: the excluded alternative would hold instead of the asserted item. Instantiated by contrastive focus (§2.3: "RONALD went shopping" excludes anyone instead of Ronald) and the discourse relation CORRECTION (§3.2: German sondern).

This distinction explains why contrastive focus and only-phrases have different presuppositions (§2.3), and why CONTRAST and CORRECTION respond to different implicit questions (§3.2).

inductive Core.InformationStructure.ExclusionVariety : Type

Two varieties of exclusion that distinguish only-phrases from contrastive focus, and CONTRAST from CORRECTION.

@cite{umbach-2004} §2.3: An only-phrase excludes the possibility that someone in addition to the focused item satisfies the predicate. A contrastive focus excludes the possibility that someone instead of the focused item satisfies the predicate.

• additional : ExclusionVariety

  Excludes additional alternatives: the excluded item would hold in addition to the asserted one. Only-phrases / CONTRAST.

• substitution : ExclusionVariety

  Excludes by substitution: the excluded item would hold instead of the asserted one. Contrastive focus / CORRECTION.

instance Core.InformationStructure.instDecidableEqExclusionVariety : DecidableEq ExclusionVariety

Equations

• Core.InformationStructure.instDecidableEqExclusionVariety x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.InformationStructure.instReprExclusionVariety.repr : ExclusionVariety → ℕ → Std.Format

Equations

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

instance Core.InformationStructure.instReprExclusionVariety : Repr ExclusionVariety

Equations

• Core.InformationStructure.instReprExclusionVariety = { reprPrec := Core.InformationStructure.instReprExclusionVariety.repr }

def Core.InformationStructure.instBEqExclusionVariety.beq : ExclusionVariety → ExclusionVariety → Bool

Equations

• Core.InformationStructure.instBEqExclusionVariety.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.InformationStructure.instBEqExclusionVariety : BEq ExclusionVariety

Equations

• Core.InformationStructure.instBEqExclusionVariety = { beq := Core.InformationStructure.instBEqExclusionVariety.beq }

def Core.InformationStructure.ExclusionVariety.toCoherenceRelation : ExclusionVariety → Discourse.CoherenceRelation.CoherenceRelation

Bridge from exclusion variety to discourse coherence relation. @cite{umbach-2004} §3.2: the information-structural exclusion type determines which discourse relation holds.

Equations

• Core.InformationStructure.ExclusionVariety.additional.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.contrast
• Core.InformationStructure.ExclusionVariety.substitution.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.correction

Focus Interpretation Principle Applications (@cite{rooth-1992} §2)

Four domains in which focus alternatives interact with context. Defined here (rather than in Theories/Semantics/Focus/ or Phenomena/Focus/) because it is a theory-neutral classification used by both layers.

inductive Core.InformationStructure.FIPApplication : Type

Application type for the Focus Interpretation Principle. @cite{rooth-1992} §2 identifies four domains where focus semantic values constrain interpretation.

• focusingAdverb : FIPApplication

  Focusing adverbs: only, even, also

• contrast : FIPApplication

  Contrast/parallelism in discourse

• scalarImplicature : FIPApplication

  Scalar implicature computation

• qaCongruence : FIPApplication

  Question-answer congruence

instance Core.InformationStructure.instDecidableEqFIPApplication : DecidableEq FIPApplication

Equations

• Core.InformationStructure.instDecidableEqFIPApplication x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.InformationStructure.instReprFIPApplication.repr : FIPApplication → ℕ → Std.Format

Equations

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

instance Core.InformationStructure.instReprFIPApplication : Repr FIPApplication

Equations

• Core.InformationStructure.instReprFIPApplication = { reprPrec := Core.InformationStructure.instReprFIPApplication.repr }

instance Core.InformationStructure.instBEqFIPApplication : BEq FIPApplication

Equations

• Core.InformationStructure.instBEqFIPApplication = { beq := Core.InformationStructure.instBEqFIPApplication.beq }

def Core.InformationStructure.instBEqFIPApplication.beq : FIPApplication → FIPApplication → Bool

Equations

• Core.InformationStructure.instBEqFIPApplication.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Discourse Context

A composite type bundling the dimensions that most commonly co-occur at discourse analysis sites: the current QUD, the expression's discourse status, and the coherence relation to prior discourse.

Motivated by co-occurrence analysis: DiscourseStatus appears in 5 of 7 multi-import sites across Phenomena/ and Theories/.

structure Core.Discourse.DiscourseContext (M : Type u_1) : Type u_1

A discourse-structural context for an expression under analysis.

Bundles three dimensions:

• QUD: what question is currently at issue (@cite{roberts-2012})
• Status: how foregrounded the expression is (given/new/focused)
• Coherence: how the current unit relates to prior discourse (@cite{kehler-2002})

The M parameter is the meaning type for the QUD partition.

• qud : QUD M

  The current Question Under Discussion

• status : InformationStructure.DiscourseStatus

  Discourse status of the current expression

• coherence : Option CoherenceRelation.CoherenceRelation

  Coherence relation to the preceding discourse unit, if any