Manuscript I@2 · I.tex · section · 85631fa7

Branch-wise linearity

Language, typing, and ownership › Branch-wise linearity · lines 432–450

A resource may therefore appear in both unexecuted alternatives without being duplicated during execution.

Classical copying and deletion are definable:

copyBit dropBit = λb : Bit . if b then ⟨ 1, 1 ⟩ else ⟨ 0, 0 ⟩, = λb : Bit . if b then * else * .

Their types are $Bit ⊸ Bit \otimes Bit$ and $Bit ⊸ 1$ . Finite classical functions are definable by finite case analysis.

Displayed formulas in this passage

unlabeled · line 438
$copyBit dropBit = λb : Bit . if b then ⟨ 1, 1 ⟩ else ⟨ 0, 0 ⟩, = λb : Bit . if b then * else * .$