Subexponential Logic

Origin. Danos, Joinet, Schellinx (1993). Nigam and Miller (2009). Multiple exponential modalities. Fine-grained resource control. Foundation for logic programming semantics.

Models. Family of !ₐ modalities. Preorder on subexponentials. Controls which structural rules apply. Modular specification of behaviors.

Formalism.

Subexponential signature: Σ = (I, ≤, U) where:

I: set of indices (subexponential labels)
≤: preorder on I
U ⊆ I: unbounded subexponentials

Multiple exponentials: !ₐA for a ∈ I Each !ₐ has its own behavior.

Structural rules per modality: If a ∈ U: weakening and contraction for !ₐ If a ∉ U: linear (no structural rules)

Promotion: !ᵦ₁A₁, ..., !ᵦₙAₙ ⊢ B ────────────────────────── !ₐ-promotion !ᵦ₁A₁, ..., !ᵦₙAₙ ⊢ !ₐB (requires all βᵢ ≤ a)

Dereliction: Γ, A ⊢ B ──────────── der Γ, !ₐA ⊢ B

Absorption: If a ≤ b: !ᵦA ⊸ !ₐA Higher index absorbs lower.

Example (linear logic programming): !_∞: classical (unlimited) !0: linear (one use) Program clauses in !∞, queries linear.

Symbols.

Symbol	Unicode	Name	Meaning
!ₐ	—	Subexponential	Indexed modality
≤	U+2264	Preorder	Index ordering
U	—	Unbounded	Allows contraction
Σ	U+03A3	Signature	Configuration

Metatheory. Cut elimination. Focusing. Logic programming semantics. Expressiveness varies with signature.

Applies to. Linear logic programming. Concurrent systems. Proof search strategies. Resource management. Multi-level security.

Limitations. Signature design matters. Complexity varies. Less studied than basic linear. Tooling limited.