Manuscript En08-A@1 · En08-A.tex · section · c688d76d

An affine first-order interface

Causal typing as an explicit refinement › An affine first-order interface · lines 1821–1866

Fix an event order $(E, \leq)$ , types, and typed primitives

op : A_{1} \times \dots \times A_{k} ⟶ B,

including nullary constants. Terms are

t ::= x ∣ op (t_{1}, \dots, t_{k}) .

An origin-annotated context is a finite map

Γ = {x_{1} : A_{1} @ e_{1}, \dots, x_{n} : A_{n} @ e_{n}} .

The annotation records the capability's origin, not a claim of physical storage at every subsequent event. Judgments are $Γ ⊢_{f} t : A$ .

The rules are

\frac{e \leq f}{x : A @ e ⊢ _{f} x : A} \textsc V a r,

\frac{Γ _{i} ⊢ _{f} t _{i} : A _{i} ( 1 \leq i \leq k ) dom Γ _{i} \cap dom Γ _{j} = \emptyset ( i \neq = j )}{⨄ _{i = 1} ^{k} Γ _{i} ⊢ _{f} op ( t _{1} , \dots , t _{k} ) : B} \textsc O p,

and

\frac{Γ ⊢ _{f} t : A x \in / dom Γ}{Γ , x : B @ e ⊢ _{f} t : A} \textsc W e ak .

A nullary operation has empty context; there is no contraction rule.

Let $∣Γ∣$ erase origins. The ordinary affine system $∣Γ∣ ⊢_{aff} t : A$ has the same rules without event annotations or the variable side condition.

Displayed formulas in this passage

unlabeled · line 1824
$op : A_{1} \times \dots \times A_{k} ⟶ B,$
unlabeled · line 1828
$t ::= x ∣ op (t_{1}, \dots, t_{k}) .$
unlabeled · line 1832
$Γ = {x_{1} : A_{1} @ e_{1}, \dots, x_{n} : A_{n} @ e_{n}} .$
unlabeled · line 1840
$\frac{e \leq f}{x : A @ e ⊢ _{f} x : A} \textsc V a r,$
unlabeled · line 1844
$\frac{Γ _{i} ⊢ _{f} t _{i} : A _{i} ( 1 \leq i \leq k ) dom Γ _{i} \cap dom Γ _{j} = \emptyset ( i \neq = j )}{⨄ _{i = 1} ^{k} Γ _{i} ⊢ _{f} op ( t _{1} , \dots , t _{k} ) : B} \textsc O p,$
unlabeled · line 1856
$\frac{Γ ⊢ _{f} t : A x \in / dom Γ}{Γ , x : B @ e ⊢ _{f} t : A} \textsc W e ak .$