Manuscript Hawk04-B@2 · Hawk04-B.tex · section · ba3b0713

Types, ownership, and observable interfaces

A finite typed circuit semantics › Types, ownership, and observable interfaces · lines 626–667

Define the fragment

T ::= I ∣ Q ∣ Bit ∣ T \otimes T

with observable algebras

A_{I} = C, A_{Q} = M_{2} (C), A_{Bit} = C \oplus C .

Hybrid states are block diagonal on their classical registers. A bit is not an unrestricted qubit under a different name.

A judgement $P : T \to T^{'}$ consumes its input interface and returns its output interface. Sequential and tensor composition require matching interfaces. A live quantum wire is never duplicated. Every live quantum output is either returned or explicitly consumed by an admitted operation. Classical control acts blockwise.

The primitive channels are

new U Enter dropBit : I \to Q, : Q^{\otimes k} \to Q^{\otimes k}, : Q \to Bit, : Bit \to I, new (1) ρ ρ (p_{0}, p_{1}) = ∣ 0 ⟩ ⟨ 0 ∣, ⟼ U ρ U^{†}, ⟼ x = 0 \sum^{1} ⟨ x ∣ ρ ∣ x ⟩ ∣ x ⟩ ⟨ x ∣, ⟼ p_{0} + p_{1} .

Return commands designate the retained interface; they are not additional dynamics.

Only specified unitary constants are admitted. A semantic constant is not a claim of exact compilation over a fixed finite gate set, efficient synthesis, or physical realization. This independently defined ownership discipline agrees with the minimal interface supplied in CheungEn03A.

Displayed formulas in this passage

unlabeled · line 648
$new U Enter dropBit : I \to Q, : Q^{\otimes k} \to Q^{\otimes k}, : Q \to Bit, : Bit \to I, new (1) ρ ρ (p_{0}, p_{1}) = ∣ 0 ⟩ ⟨ 0 ∣, ⟼ U ρ U^{†}, ⟼ x = 0 \sum^{1} ⟨ x ∣ ρ ∣ x ⟩ ∣ x ⟩ ⟨ x ∣, ⟼ p_{0} + p_{1} .$
unlabeled · line 629
$T ::= I ∣ Q ∣ Bit ∣ T \otimes T$
unlabeled · line 633
$A_{I} = C, A_{Q} = M_{2} (C), A_{Bit} = C \oplus C .$