Linglib now contains over 700 files implementing theories from across formal linguistics — Montague semantics, RSA pragmatics, causal semantics, degree constructions, dynamic update, tense, aspect, presupposition. These are not independent modules that happen to coexist in the same repository. They share mathematical infrastructure, and the sharing is the point.

But what infrastructure, exactly? When you trace the import graph all the way down to Core/, a clear picture emerges. There are five genuinely independent mathematical foundations — files with zero mutual dependencies — and everything else is either derived from one root or, more interestingly, bridges between two roots. The bridges are where the interesting linguistic theory lives.

This post maps the territory.

The interactive map

Hover over any node to see its file path and connections. Use the buttons to filter by mathematical family or show only the cross-root bridges. Toggle “Show proposed” to see planned additions.

Five independent roots

When you trace every import in Core/ to its terminal node — a file with no further Core/ dependencies — you find five genuinely independent mathematical structures. Each has zero imports from any other root.

Scale (Core/Scale.lean). Linear orders and measurement. The mathematical content is StrictMono : (α, ≤) → (ℚ, ≤) — order-preserving maps that measure how big things are. Everything in degree semantics, mereological structure, spatial paths, and temporal intervals traces back here. Time is not a separate root; it imports Scale and specializes it to intervals over a linear order.

Causation (Core/Causation.lean). Structural causal models and fixpoint computation. The core operation is normalDevelopment: given a set of causal laws and an initial situation (a partial valuation of boolean variables), iterate the laws to a fixpoint. The resulting closure generates causal sufficiency (“make,” “manage”), necessity (“cause,” “because”), implicativity (“manage,” “fail”), and actuality entailments for ability modals.

RationalAction (Core/RationalAction.lean). The Luce choice rule: agents select actions with probability proportional to a score function. This is the unique choice rule satisfying independence of irrelevant alternatives (Luce 1959). The exponential parameterization (score = exp(α · utility)) gives softmax, which is the standard form in RSA. Every RSA agent — L0, S1, L1 — is a RationalAction instance with a different score function. The Gibbs variational principle and maximum-entropy characterizations follow.

Proposition (Core/Proposition.lean). Truth conditions: World → Prop. Together with Kleene.lean (three-valued logic, also zero imports), this grounds intensional types, common ground update, modal logic, and presupposition. The common ground update operation is itself a closure operator on (ContextSet, ⊆) — a connection we return to below.

QUD + DecisionTheory (Core/QUD.lean, Core/DecisionTheory.lean). Partitions as question denotations and decision problems with expected utility. Their merge point is Partition.lean, which defines the Blackwell ordering: one partition is more informative than another if and only if it yields higher expected utility under every prior and every decision problem. This connects information structure to rational choice.

Mathematical relationships

Three of the five roots — Scale, Causation, and Proposition — live in the category Pos (posets and monotone maps). But they occupy different structural niches within it.

Scale provides morphisms between posets: the measure function μ : (Entities, ⊑) → (ℚ, ≤) is a strictly monotone homomorphism. MereoDim recognizes this — it identifies monotone and strictly-monotone maps as the categorical morphisms that preserve part-whole structure across dimensions (temporal, spatial, object).

Causation provides a monad on a poset: normalDevelopment is an endofunctor on (Situation, ⊑) that is inflationary (η), monotone (naturality), and idempotent (μ). This is the definition of a closure operator, which is equivalent to a Galois connection between the poset and its sublattice of closed elements. Sufficiency, necessity, and actuality depend only on these three properties, not on the graph representation of the causal model.

Proposition provides products: propositions live in (World → Prop, ⊆) under entailment, and conjunction is the categorical product.

RationalAction is genuinely different. It belongs not to Pos but to something like Meas (probability spaces). The softmax function creates a probability distribution from a utility function via exp and log — analytic operations with no order-theoretic analog. This is why Luce cannot be unified with the other roots. It connects to them only at specific grounding interfaces, where a semantic backend (from Proposition or Scale) feeds a score function into the pragmatic machinery.

Bridges: where the theory lives

The most important files in the repository are not the roots. They are the bridges — files that import from two different roots and prove a theorem connecting them. Each bridge corresponds to a substantive linguistic generalization.

MereoDim (Core/MereoDim.lean) bridges Scale and Mereology. The DimensionBridge extends this further, connecting mereological structure to temporal intervals, spatial paths, and object measures through three dimension chains (τ, σ, θ). The telicity of “run to the store” is the boundedness of the spatial path; the telicity of “eat three apples” is the quantization of the object measure. These are the same mathematical theorem, instantiated in different dimensions.

Tense (Core/Tense.lean) bridges Scale (via Time and Reichenbach) and Proposition (via Intension). Abusch’s (1997) insight is that a tense morpheme is a temporal pronoun — a variable with a presupposed temporal constraint and a binding mode. This requires both temporal structure (from Scale) and intensional types (from Proposition).

Ability (Modality/Ability.lean) bridges Closure and Scale. The actuality entailment of was able to depends on viewpoint aspect: perfective triggers the inference that the complement event actually occurred; imperfective does not. This is formalized as aspect (from the temporal dimension chain) modulating membership in the causal closure.

Beller & Gerstenberg 2025 bridges Luce and Closure. An RSA speaker chooses between causal expressions (“caused,” “made,” “enabled”) based on the listener’s expected causal inference. The score function references causal sufficiency and necessity — features computed by the closure operator on situations.

Lassiter & Goodman 2017 bridges Luce and Scale. An RSA speaker and listener negotiate the threshold for a gradable adjective (“tall”). The degree scale provides the semantic content; Luce choice provides the pragmatic interpretation of where the threshold falls.

Blackwell ordering (Core/Partition.lean) bridges Decision and Luce. Finer partitions — more informative question-under-discussion resolutions — yield higher expected utility under any decision problem. This is the decision-theoretic foundation for why questions matter: they reshape the listener’s information in ways that improve action selection.

Missing bridges

There are several natural bridges not yet in the codebase.

Closure ↔ Scale: DegreeCausation. Nadathur’s analysis of enough and too treats them as degree constructions over causal sufficiency. “Tall enough to reach the shelf” asserts that at the actual degree of height, the complement (reaching the shelf) is in the causal closure. Each degree induces a different set of causal laws, giving a family of closure operators indexed by the degree scale. This is the most immediate bridge to build.

Closure ↔ Proposition: CommonGround as closure. The common ground update operation already has update_mono and update_assoc proved — it is a closure operator on (ContextSet, ⊆). Making this explicit would connect causal dynamics and discourse update as instances of the same algebra, enabling questions like: when does causal closure commute with context update?

Luce ↔ Time: Pragmatics of temporal reference. How do speakers choose between tense and aspect forms? An RSA model over temporal semantics would bridge Luce and the interval root, but this is sparse in the literature.

The dependency hierarchy

The mathematical picture, in summary:

Category Pos (posets, monotone maps)
├─ Hom(A, B)           ← Scale: μ : (Entities,⊑) → (ℚ,≤) is StrictMono
│   └─ MereoDim recognizes these as categorical morphisms
├─ Monad on A           ← Closure: cl : (Situation,⊑) → (Situation,⊑)
│   └─ η = inflationary, μ = idempotent, naturality = monotone
│   └─ ≡ Galois connection A ⇆ Closed(A) ≡ Scott information system
├─ Sub(Interval(A))     ← Time: specializes Scale to intervals over linear orders
└─ Π (products)         ← Proposition: W → Prop lives in Pos via entailment

Category Meas (probability spaces)
 └─ Luce: softmax : (utility : A → ℝ) → Δ(A)
     └─ Connects to Pos only at grounding interfaces

The roots are independent. The bridges are where the linguistics lives. Adding a new bridge — a theorem connecting two roots — is the primary way that Linglib grows.