Proposition: Finite semantic realization and termination

Every finite-dimensional CPTP map admits a semantic implementation by pure allocation, a specified unitary, destructive readout of unused work qubits, discard of their outcomes, and quantum return of its designated output.

Every well-typed finite acyclic instruction tree in the declared fragment denotes a CPTP hybrid channel, including untouched references, and every evaluation branch terminates.

Proof. For Kraus operators $D_j$ of a finite channel, define

Completeness of the Kraus family makes $L$ an isometry. After qubit encoding and sufficient pure allocation, its orthonormal columns extend to a unitary. Readout and discard of $G$ give

while the designated logical output remains quantum.

For a finite instruction tree, allocation and unitary nodes are complete channels, and readout satisfies ${\sum }_x{M}_x^{†}{M}_x=I$. Classical discard sums unnormalized blocks. Induction gives path maps $K_h$ with

Grouping paths by reported outputs gives the hybrid denotation. Tensoring every path map with a reference identity proves reference preservation. A finite acyclic tree has finite maximum branch length.