Components / Parameters

Syntax (Λ, Ⅎ, Ⱶ)
Reduction rules
Typing discipline
Semantic interpretation

Λ denotes binding,
Ⅎ denotes application (flow), and
Ⱶ denotes evaluation modality.

Theorem 5.1 (Controlled β-Reduction).

Ⱶ((Λx.t) Ⅎ s) → Ⱶ(t[x := s])

Proof. By Definition 1.1 and Axiom 2.3, application reduces only when guarded by Ⱶ. ∎

Prediction. Future calculi will make evaluation and resource flow explicit primitives.