Skip to content

Commit c0f0e31

Browse files
hawkrobehawkrobe
committed
add bouletic flavor, Cat.Nmlz, Washo/Koryak fragments, Roberts 2023, C-only phases (0.229.713)
1 parent 33bd8f5 commit c0f0e31

19 files changed

Lines changed: 1224 additions & 64 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,25 @@
11
# Changelog
22

3+
## [0.229.713] - 2026-04-13
4+
5+
### Added
6+
- **Bouletic modal flavor**: add `.bouletic` to `ModalFlavor` (3→4 flavors, 9→12 ForceFlavor pairs), following Kratzer 1981's four-way classification; update all downstream files (German modals, Japanese particles, Narrog, OutlookMarker, ImelGuoST2026)
7+
- **German *sollte***: add as separate modal from *sollen* (Konjunktiv II, wider flavor range); German inventory now 7 modals
8+
- **Washo fragment** (`Fragments/Washo/Modals.lean`): *-eʔ* as SAV counterexample (variable force + variable flavor); satisfies IFF
9+
- **Koryak fragment** (`Fragments/Koryak/Modals.lean`): *ivək* as second SAV counterexample; satisfies IFF
10+
- **`Cat.Nmlz`**: nominalizer head (Keine 2020, Hindi -naa/-ne); update `catFeatures`, `fValue` (F3), `catFamily`, `categorialFeatures`, `epSemanticType`
11+
- **`isPhaseHeadV`**: traditional C+v phase identification; `isPhaseHead` now C-only per Keine 2020 ch. 5
12+
- **`Discourse/Goals.lean`**, **`Discourse/Scoreboard.lean`**: core discourse infrastructure (Portner 2004, Roberts 2023)
13+
- **`Roberts2023.lean`** (`Phenomena/Directives/Studies/`): imperatives in dynamic pragmatics
14+
- **Unattested meaning tests**: `mighst_not_iff`, `mighst_not_sav` (IFF rules out epistemic-possibility + deontic-necessity)
15+
- Bibliography: Bochnak 2015a/b, Močnik & Abramovitz 2019, Chemla et al. 2019, Ferreira 2023, von Fintel & Iatridou 2017, Portner 2004, Bratman 1987, Roberts 2023, Veltman 2018, Polinsky & Potsdam 2001, Bobaljik & Wurmbrand 2005, Keine 2020
16+
17+
### Changed
18+
- Rename `fpos_iff_functional` → `fpos_iff_not_lexical` (cleaner biconditional: `isFHead ↔ ¬isLHead`)
19+
- German *wollen* now `.bouletic` (was `.deontic`); `sollen_wollen_deontic` split into `sollen_deontic` + `wollen_bouletic`
20+
- `Narrog.modalFlavor_roundtrip` and `orientationOfFlavor_consistent` exclude `.bouletic` (collapses with deontic in Narrog's 2D space)
21+
- Cross-linguistic summary: 10→12 inventories, `eight_of_ten_perfect_iff` → `ten_of_twelve_perfect_iff`
22+
323
## [0.229.712] - 2026-04-13
424

525
### Added

‎Linglib/Core/Discourse/Goals.lean‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
import Linglib.Core.Semantics.Proposition
2+
3+
/-!
4+
# Discourse Goals and Plans
5+
@cite{bratman-1987} @cite{portner-2004} @cite{roberts-2023}
6+
7+
The interlocutors' publicly evident goals, plans, and priorities — the **G**
8+
component of @cite{roberts-2023}'s scoreboard K = ⟨I, M, ≺, CG, QUD, G⟩.
9+
10+
@cite{bratman-1987}: intentions are commitments to action, organized
11+
hierarchically into plans. Goals subserve other goals, and an agent's
12+
priorities induce a partial order over them.
13+
14+
@cite{portner-2004}'s ToDo list is a special case: an unstructured set of
15+
properties the addressee is committed to realizing. The present formalization
16+
follows @cite{roberts-2023} in giving G richer internal structure — conditional
17+
goals with priority ordering — while remaining compatible with Portner's
18+
interface (a `GoalSet` projects to a flat property list).
19+
20+
## Key Design Choices
21+
22+
1. Goals are **conditional**: realized only when applicable circumstances
23+
obtain (@cite{roberts-2023} §2.1.1). We represent the condition as a
24+
proposition (the modal base propositions that must hold).
25+
2. Goals carry **priority**: a natural number where lower = higher priority.
26+
@cite{roberts-2023}: "i's priorities are reflected in additional structure
27+
over G_i."
28+
3. Goal sets are **per-agent**: G = {G_i | i ∈ I}, one set per interlocutor.
29+
-/
30+
31+
namespace Core.Discourse
32+
33+
open Core.Proposition (BProp)
34+
35+
variable {W : Type*}
36+
37+
/-- A single goal: a proposition the agent is committed to realizing,
38+
conditional on certain circumstances obtaining.
39+
40+
@cite{roberts-2023} §2.1.1: "for all g ∈ G_i, g is a conditional goal,
41+
its presence in G_i representing i's intention to achieve the goal
42+
should certain conditions obtain in the actual world at some future
43+
time t' > t." -/
44+
structure Goal (W : Type*) where
45+
/-- The content: what the agent aims to bring about -/
46+
content : BProp W
47+
/-- The condition: circumstances under which this goal is active.
48+
`λ _ => true` for unconditional goals. -/
49+
condition : BProp W := λ _ => true
50+
/-- Priority level: 0 = highest priority. @cite{roberts-2023}: goals are
51+
hierarchically organized to reflect plans and priorities. -/
52+
priority : Nat := 0
53+
deriving Inhabited
54+
55+
/-- An agent's goal set: the publicly evident goals, plans, and priorities.
56+
57+
@cite{roberts-2023} §2.1.1: "G_i is the set of i's evident goals,
58+
including those which i is publicly committed at t to trying to realize."
59+
Goals are organized to reflect plans and priorities. -/
60+
structure GoalSet (W : Type*) where
61+
/-- The goals, ordered by priority (lower index = mentioned earlier,
62+
not necessarily higher priority — use `Goal.priority` for ranking). -/
63+
goals : List (Goal W) := []
64+
deriving Inhabited
65+
66+
namespace GoalSet
67+
68+
/-- The empty goal set. -/
69+
def empty : GoalSet W := ⟨[]⟩
70+
71+
/-- Add a goal to the set. -/
72+
def add (gs : GoalSet W) (g : Goal W) : GoalSet W :=
73+
⟨g :: gs.goals⟩
74+
75+
/-- Add an unconditional goal with given priority. -/
76+
def addSimple (gs : GoalSet W) (content : BProp W) (priority : Nat := 0) : GoalSet W :=
77+
gs.add { content, priority }
78+
79+
/-- Remove goals whose content matches a predicate (e.g., realized or abandoned). -/
80+
def remove (gs : GoalSet W) (shouldRemove : Goal W → Bool) : GoalSet W :=
81+
⟨gs.goals.filter (λ g => !shouldRemove g)⟩
82+
83+
/-- Goals active in circumstance w (condition satisfied). -/
84+
def activeGoals (gs : GoalSet W) (w : W) : List (Goal W) :=
85+
gs.goals.filter (λ g => g.condition w)
86+
87+
/-- Active goal contents at w, sorted by priority (ascending = most important first). -/
88+
def activeContents (gs : GoalSet W) (w : W) : List (BProp W) :=
89+
(gs.activeGoals w |>.mergeSort (λ g₁ g₂ => g₁.priority ≤ g₂.priority))
90+
|>.map Goal.content
91+
92+
/-- Project to a flat list of contents (@cite{portner-2004} ToDo list interface). -/
93+
def toPropertyList (gs : GoalSet W) : List (BProp W) :=
94+
gs.goals.map Goal.content
95+
96+
/-- Whether the goal set is empty. -/
97+
def isEmpty (gs : GoalSet W) : Bool :=
98+
gs.goals.isEmpty
99+
100+
/-- Number of goals. -/
101+
def size (gs : GoalSet W) : Nat :=
102+
gs.goals.length
103+
104+
end GoalSet
105+
106+
end Core.Discourse

‎Linglib/Core/Discourse/Scoreboard.lean‎

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
import Linglib.Core.Discourse.Goals
2+
import Linglib.Core.Discourse.SpeechActs
3+
import Linglib.Core.Discourse.QUD
4+
5+
/-!
6+
# Scoreboard: Unified Discourse State
7+
@cite{roberts-2023} @cite{roberts-2012} @cite{lewis-1979} @cite{portner-2004}
8+
9+
The scoreboard K for a language game at time t is a tuple
10+
⟨I, M, ≺, CG, QUD, G⟩ (@cite{roberts-2023} §2.1.1), tracking:
11+
12+
- **I**: the set of interlocutors
13+
- **M**: illocutionary moves made so far (with subsets A, Q, D, Acc)
14+
- **≺**: temporal order on moves
15+
- **CG**: the common ground (propositions treated as mutually believed)
16+
- **QUD**: the ordered set of questions under discussion
17+
- **G**: the interlocutors' publicly evident goals, plans, and priorities
18+
19+
The three central elements — CG, QUD, G — are updated by the three
20+
canonical speech acts via the **Illocutionary Force Linking Principle**
21+
(@cite{roberts-2023} (56)):
22+
23+
| Clause type | Semantic type | Default force | Updates |
24+
|-------------|-------------------|---------------|---------|
25+
| declarative | proposition | assertion | CG |
26+
| interrogative| set of propositions| interrogation | QUD |
27+
| imperative | indexed property | direction | G |
28+
29+
## Relation to Prior Work
30+
31+
@cite{lewis-1979}'s "scorekeeping in a language game" introduced the
32+
metaphor. @cite{roberts-2012} formalized CG + QUD. @cite{portner-2004}
33+
added the addressee's ToDo list. @cite{roberts-2023} unifies all three
34+
into a single scoreboard and gives G richer internal structure
35+
(conditional goals with hierarchical priorities, following @cite{bratman-1987}).
36+
-/
37+
38+
namespace Core.Discourse
39+
40+
open Core.Proposition (BProp)
41+
42+
variable {W : Type*}
43+
44+
/-- The semantic type of a clause, determining its default illocutionary force.
45+
46+
@cite{roberts-2023} (56): propositions → assertion, sets of propositions →
47+
interrogation, indexed properties → direction. -/
48+
inductive SemanticType where
49+
/-- Type ⟨s, t⟩: a proposition (set of worlds) -/
50+
| proposition
51+
/-- Type ⟨⟨s, t⟩, t⟩: a set of propositions (Hamblin question denotation) -/
52+
| setOfPropositions
53+
/-- Type ⟨s, ⟨e, t⟩⟩: a property indexed to the addressee -/
54+
| indexedProperty
55+
deriving DecidableEq, Repr
56+
57+
/-- **Illocutionary Force Linking Principle** (@cite{roberts-2023} (56)):
58+
the default illocutionary force of a root sentence is determined by
59+
its semantic type.
60+
61+
(a) proposition → assertion
62+
(b) set of propositions → interrogation
63+
(c) indexed property → direction -/
64+
def forceLinkingPrinciple : SemanticType → IllocutionaryMood
65+
| .proposition => .declarative
66+
| .setOfPropositions => .interrogative
67+
| .indexedProperty => .imperative
68+
69+
/-- The default semantic type for each illocutionary mood (inverse of IFLP). -/
70+
def defaultSemanticType : IllocutionaryMood → SemanticType
71+
| .declarative => .proposition
72+
| .interrogative => .setOfPropositions
73+
| .imperative => .indexedProperty
74+
| .promissive => .indexedProperty -- promissives also denote properties
75+
| .exclamative => .proposition -- exclamatives denote propositions
76+
77+
/-- IFLP round-trips for the three core moods. -/
78+
theorem iflp_roundtrip_decl :
79+
forceLinkingPrinciple (defaultSemanticType .declarative) = .declarative := rfl
80+
theorem iflp_roundtrip_interrog :
81+
forceLinkingPrinciple (defaultSemanticType .interrogative) = .interrogative := rfl
82+
theorem iflp_roundtrip_imp :
83+
forceLinkingPrinciple (defaultSemanticType .imperative) = .imperative := rfl
84+
85+
/-! ## The Scoreboard -/
86+
87+
/-- An illocutionary move on the scoreboard.
88+
89+
@cite{roberts-2023} §2.1.1: M is the set of moves, with distinguished
90+
subsets A (assertions), Q (questions), D (directions), Acc (accepted). -/
91+
structure Move (W : Type*) where
92+
/-- Which kind of speech act -/
93+
mood : IllocutionaryMood
94+
/-- Propositional content (for assertions and questions; for directions,
95+
the propositional closure of the targeted property) -/
96+
content : BProp W
97+
/-- Who made the move -/
98+
agent : Nat -- agent index into interlocutors
99+
/-- Whether this move has been accepted by the interlocutors -/
100+
accepted : Bool := false
101+
deriving Inhabited
102+
103+
/-- The scoreboard K for a language game.
104+
105+
@cite{roberts-2023} §2.1.1: K = ⟨I, M, ≺, CG, QUD, G⟩.
106+
We represent ≺ implicitly via list order in `moves`. -/
107+
structure Scoreboard (W : Type*) where
108+
/-- I: the interlocutors (by index) -/
109+
numInterlocutors : Nat
110+
/-- M: illocutionary moves in temporal order (≺ = list position) -/
111+
moves : List (Move W) := []
112+
/-- CG: the common ground — propositions treated as mutually believed.
113+
Represented as a list of propositions; the context set is their
114+
intersection. -/
115+
cg : List (BProp W) := []
116+
/-- QUD: questions under discussion (as a stack of proposition-sets).
117+
Simplified from the full `QUDStack` for composability. -/
118+
qud : List (BProp W) := []
119+
/-- G: per-agent goal sets. `goals[i]` is G_i.
120+
Length should equal `numInterlocutors`. -/
121+
goals : List (GoalSet W) := []
122+
deriving Inhabited
123+
124+
namespace Scoreboard
125+
126+
/-- The context set: worlds compatible with all CG propositions. -/
127+
def contextSet (K : Scoreboard W) : BProp W :=
128+
λ w => K.cg.all (λ p => p w)
129+
130+
/-- An agent's goal set. Returns empty if index out of bounds. -/
131+
def agentGoals (K : Scoreboard W) (i : Nat) : GoalSet W :=
132+
K.goals.getD i GoalSet.empty
133+
134+
/-- **Assertion update** (@cite{roberts-2023} (57), following @cite{stalnaker-1978}):
135+
If a proposition is asserted and accepted, it is added to CG_K. -/
136+
def assertionUpdate (K : Scoreboard W) (p : BProp W) (agent : Nat) : Scoreboard W :=
137+
{ K with
138+
cg := p :: K.cg
139+
moves := ⟨.declarative, p, agent, true⟩ :: K.moves }
140+
141+
/-- **Interrogation update** (@cite{roberts-2023} (58), following @cite{roberts-2012}):
142+
If a question is posed and accepted, it is added to QUD_K. -/
143+
def interrogationUpdate (K : Scoreboard W) (q : BProp W) (agent : Nat) : Scoreboard W :=
144+
{ K with
145+
qud := q :: K.qud
146+
moves := ⟨.interrogative, q, agent, true⟩ :: K.moves }
147+
148+
/-- **Direction update** (@cite{roberts-2023} (59)):
149+
If a targeted property is issued to addressee i and accepted,
150+
G_i is revised to include the realization of the property in any
151+
applicable circumstances. -/
152+
def directionUpdate (K : Scoreboard W) (p : BProp W)
153+
(speaker target : Nat) (priority : Nat := 0) : Scoreboard W :=
154+
let newGoal : Goal W := { content := p, priority }
155+
let rec go : List (GoalSet W) → Nat → List (GoalSet W)
156+
| [], _ => []
157+
| gs :: rest, i => (if i == target then gs.add newGoal else gs) :: go rest (i + 1)
158+
let updatedGoals := go K.goals 0
159+
{ K with
160+
goals := updatedGoals
161+
moves := ⟨.imperative, p, speaker, true⟩ :: K.moves }
162+
163+
/-- Assertion update adds to CG. -/
164+
theorem assertion_adds_to_cg (K : Scoreboard W) (p : BProp W) (a : Nat) :
165+
(K.assertionUpdate p a).cg = p :: K.cg := rfl
166+
167+
/-- Direction update preserves CG. -/
168+
theorem direction_preserves_cg (K : Scoreboard W) (p : BProp W) (s t pr : Nat) :
169+
(K.directionUpdate p s t pr).cg = K.cg := rfl
170+
171+
/-- Direction update preserves QUD. -/
172+
theorem direction_preserves_qud (K : Scoreboard W) (p : BProp W) (s t pr : Nat) :
173+
(K.directionUpdate p s t pr).qud = K.qud := rfl
174+
175+
/-- Assertion update preserves G. -/
176+
theorem assertion_preserves_goals (K : Scoreboard W) (p : BProp W) (a : Nat) :
177+
(K.assertionUpdate p a).goals = K.goals := rfl
178+
179+
end Scoreboard
180+
end Core.Discourse

‎Linglib/Core/Modality/ModalTypes.lean‎

Lines changed: 11 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -102,10 +102,13 @@ theorem ModalForce.possibility_weakest (f : ModalForce) :
102102

103103
/-- Modal flavor: the contextual source of modality.
104104
Theory-neutral: avoids commitment to how flavor is semantically encoded.
105-
Teleological is subsumed under circumstantial (both concern facts/abilities). -/
105+
Teleological is subsumed under circumstantial (both concern facts/abilities).
106+
Bouletic (desires/wishes) is distinguished from deontic (norms/rules),
107+
following @cite{kratzer-1981}'s four-way classification. -/
106108
inductive ModalFlavor where
107109
| epistemic -- Evidence/knowledge
108110
| deontic -- Norms/rules
111+
| bouletic -- Desires/wishes
109112
| circumstantial -- Facts/abilities (subsumes teleological)
110113
deriving DecidableEq, Repr, Inhabited
111114

@@ -114,23 +117,23 @@ instance : LawfulBEq ModalFlavor where
114117
rfl {a} := by cases a <;> decide
115118

116119
instance : ToString ModalFlavor where
117-
toString | .epistemic => "e" | .deontic => "d" | .circumstantial => "c"
120+
toString | .epistemic => "e" | .deontic => "d" | .bouletic => "b" | .circumstantial => "c"
118121

119122
/-- All modal flavors. -/
120-
def ModalFlavor.all : List ModalFlavor := [.epistemic, .deontic, .circumstantial]
123+
def ModalFlavor.all : List ModalFlavor := [.epistemic, .deontic, .bouletic, .circumstantial]
121124

122125
-- ============================================================================
123126
-- §3. Force-Flavor Pairs
124127
-- ============================================================================
125128

126129
/-- A force-flavor pair: one point in the modal semantic space P.
127-
|P| = |Force| × |Flavor| = 3 × 3 = 9.
130+
|P| = |Force| × |Flavor| = 3 × 4 = 12.
128131
129132
Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026}: modal meanings are subsets of P.
130133
Their original database uses a 2×3 space (necessity/possibility × 3 flavors);
131-
we extend to 3×3 by adding weak necessity as a distinct force value,
132-
following @cite{agha-jeretic-2026}'s treatment of weak necessity as a
133-
category intermediate between □ and ◇. -/
134+
we extend to 3×4 by adding weak necessity as a distinct force value
135+
(following @cite{agha-jeretic-2026}) and bouletic as a distinct flavor
136+
(following @cite{kratzer-1981}). -/
134137
structure ForceFlavor where
135138
force : ModalForce
136139
flavor : ModalFlavor
@@ -150,7 +153,7 @@ instance : ToString ForceFlavor where
150153
def ForceFlavor.universe : List ForceFlavor :=
151154
ModalForce.all.flatMap fun fo => ModalFlavor.all.map fun fl => ⟨fo, fl⟩
152155

153-
theorem ForceFlavor.universe_length : ForceFlavor.universe.length = 9 := by native_decide
156+
theorem ForceFlavor.universe_length : ForceFlavor.universe.length = 12 := by native_decide
154157

155158
/-- The Cartesian product of forces and flavors. Infrastructure for constructing
156159
modal meanings; no theoretical commitment (just list operations). -/

0 commit comments

Comments
 (0)