Manuscript VII-E@1 · VII-E.tex · section · b713cf3c

A minimal linear interface

Types, states, and external geometry › A minimal linear interface · lines 389–419

Wire types are generated by

A ::= I ∣ Q ∣ Bit ∣ A \otimes A .

A judgement $f : A \to B$ consumes the complete input interface and returns the declared output interface. Composition and tensoring obey

\frac{f : A \to B g : B \to C}{g \circ f : A \to C}, \frac{f : A \to B g : C \to D}{f \otimes g : A \otimes C \to B \otimes D} .

Identities and wire permutations are available. Circuit constants used below include quantum unitaries, preparation of $∣ 0 ⟩$ , and destructive computational-basis readout. The finite classical-code implementation also uses reversible NOT, CNOT, and Toffoli operations on classical interfaces. Their quantum-carrier realizations are the corresponding permutation unitaries.

Linearity is an ownership condition. It permits a sequence of gates to consume and return the same physical tensor factor. It provides neither duplication of an arbitrary quantum wire nor an implicit discard operation.

The semantic matter-rule class below permits declared channels. We do not claim that every such channel has an exact implementation in the displayed finite gate library. Exact gate realizability is proved only for the finite reversible event code in sec:event-code.

Displayed formulas in this passage

unlabeled · line 392
$A ::= I ∣ Q ∣ Bit ∣ A \otimes A .$
unlabeled · line 397
$\frac{f : A \to B g : B \to C}{g \circ f : A \to C}, \frac{f : A \to B g : C \to D}{f \otimes g : A \otimes C \to B \otimes D} .$