Features.InformationStructure

@cite{rooth-1992} @cite{steedman-2000} @cite{kuroda-1972} @cite{umbach-2004} @cite{turco-braun-dimroth-2014}

Theory-neutral substance taxonomies for Information Structure: theme/ rheme partitions, focus/background (binary FocusMark + structured Roothian Focus α), focus-marking strategies, judgment type.

@cite{krifka-2008} enumerates four IS notions — focus, givenness, topic, and delimitation (frame-setting); @cite{fery-ishihara-2016} (Oxford Handbook of Information Structure) adopts Krifka's definitions as the unifying baseline. At-issueness (the QUD-tradition axis from Roberts / Tonhauser-Beaver-Roberts-Simons / Tonhauser-Beaver-Degen) is treated as orthogonal to Krifka's four. Substrate for each:

• Focus: FocusMark + Focus α (this file).
• Givenness: Features/Givenness.lean (GivennessStatus + BinaryGivenness).
• Topic: Features/Topic.lean (TopicMark + ContrastiveTopic α).
• At-issueness: Core/Discourse/AtIssueness.lean (gradient AtIssuenessDegree).
• Delimitation: no substrate yet — deferred.

Theme/Rheme and JudgmentType (Kuroda 1972) live here too — they predate Krifka's decomposition and target distinct phenomena (Prague-school packaging, categorical-vs-thetic judgments).

Theory-level predicates over these taxonomies (Umbach's alt-set well-formedness, Erteschik-Shir/Abeillé extraction-IS clash) live in Theories/Semantics/Focus/Comparability.lean. Focus-specific compositional operations (AltMeaning) live in Theories/Semantics/Alternatives/.

Theme and Rheme

structure Features.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 per @cite{pierrehumbert-hirschberg-1990}; attributed by @cite{steedman-2000} to the Theme tune)
• 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)

structure Features.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 per @cite{pierrehumbert-hirschberg-1990})
• Provides the "answer" to the implicit question

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

• content : P

  The rhematic content

Focus and Background

inductive Features.InformationStructure.FocusMark : Type

Binary focus marking — whether a constituent bears focus or not. The simplest categorical encoding of the focus axis (Krifka 2008 one of four IS notions). Mirror of Features.TopicMark for the topic axis. Use FocusMark when a study only needs the binary focus-vs-not distinction; use Focus α (below) when the Roothian alternative-set structure is needed.

• focused : FocusMark

  Constituent is focus-marked (pitch accent / contrast).

• nonFocused : FocusMark

  Constituent is not focus-marked.

@[implicit_reducible]

instance Features.InformationStructure.instDecidableEqFocusMark : DecidableEq FocusMark

Equations

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

def Features.InformationStructure.instReprFocusMark.repr : FocusMark → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.InformationStructure.instReprFocusMark : Repr FocusMark

Equations

• Features.InformationStructure.instReprFocusMark = { reprPrec := Features.InformationStructure.instReprFocusMark.repr }

@[implicit_reducible]

instance Features.InformationStructure.instInhabitedFocusMark : Inhabited FocusMark

Equations

• Features.InformationStructure.instInhabitedFocusMark = { default := Features.InformationStructure.instInhabitedFocusMark.default }

def Features.InformationStructure.instInhabitedFocusMark.default : FocusMark

Equations

• Features.InformationStructure.instInhabitedFocusMark.default = Features.InformationStructure.FocusMark.focused

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

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

Focus is marked by pitch accent and:

• Evokes alternatives (@cite{rooth-1992} alternative semantics — note that Schwarzschild 1999, Wagner 2012 contest the alt-set primitive; the field alternatives : List α here commits to the Roothian view)
• 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 Features.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

Information Structure Partition

structure Features.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)

Note: foci : List P and background : List P are flat lists of P-values, not List (Focus P) / List (Background P). The Focus/Background structs are reusable pieces for theories that want to bundle alternatives explicitly, but InfoStructure's own fields use the underlying P type.

• 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)

Focus Interpretation Principle (Rooth 1992)

inductive Features.InformationStructure.FIPApplication : Type

Application type for the Focus Interpretation Principle. The four constructors below pick out the families of focus uses Rooth surveys (focusing adverbs, contrast/parallelism, scalar implicature, question–answer congruence). UNVERIFIED whether the paper specifies exactly these four under a single header — earlier prose claimed @cite{rooth-1992} §2, removed pending PDF check.

• focusingAdverb : FIPApplication

  Focusing adverbs: only, even, also

• contrast : FIPApplication

  Contrast/parallelism in discourse

• scalarImplicature : FIPApplication

  Scalar implicature computation

• qaCongruence : FIPApplication

  Question-answer congruence

@[implicit_reducible]

instance Features.InformationStructure.instDecidableEqFIPApplication : DecidableEq FIPApplication

Equations

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

def Features.InformationStructure.instReprFIPApplication.repr : FIPApplication → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.InformationStructure.instReprFIPApplication : Repr FIPApplication

Equations

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

Categorical vs Thetic Judgment (Kuroda 1972)

@cite{kuroda-1972} distinguishes two types of judgment that correspond to different information structures:

• Categorical judgment: a subject-predicate structure where the subject (ψ-subject) is the topic of predication, yielding a Theme + Rheme partition.
• Thetic judgment: presents an event or situation as a whole, without a subject of predication, yielding an all-Rheme (no Theme) structure.

Cross-linguistically attested in Japanese (wa/ga), Romance (subject inversion), and Mayan (ψ-subject constructions, @cite{aissen-polian-2025}).

inductive Features.InformationStructure.JudgmentType : Type

Judgment type following @cite{kuroda-1972}. Categorical judgments have a subject of predication (ψ-subject); thetic judgments present an event without one.

• categorical : JudgmentType

  Subject-predicate; ψ-subject is Topic

• thetic : JudgmentType

  Event-presenting; no subject of predication

@[implicit_reducible]

instance Features.InformationStructure.instDecidableEqJudgmentType : DecidableEq JudgmentType

Equations

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

def Features.InformationStructure.instReprJudgmentType.repr : JudgmentType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.InformationStructure.instReprJudgmentType : Repr JudgmentType

Equations

• Features.InformationStructure.instReprJudgmentType = { reprPrec := Features.InformationStructure.instReprJudgmentType.repr }

def Features.InformationStructure.JudgmentType.HasψSubject (j : JudgmentType) : Prop

Does this judgment type place a subject of predication (ψ-subject) in a dedicated syntactic position (e.g., Spec,TP)?

Equations

• j.HasψSubject = (j = Features.InformationStructure.JudgmentType.categorical)

@[implicit_reducible]

instance Features.InformationStructure.instDecidableHasψSubject (j : JudgmentType) : Decidable j.HasψSubject

Equations

• Features.InformationStructure.instDecidableHasψSubject j = Features.InformationStructure.instDecidableHasψSubject._aux_1 j