Manuscript Psy04-B@1 · Psy04-B-v1.tex · section · 62c2b6f0

Local encoding and late decoding

Sequential qubit routing and explicit Enter operations › Local encoding and late decoding · lines 1012–1062

Psy04-B@1#eq:decoderterm

Let

R_{y} (θ) = e^{- i θ σ_{y} /2}, H = \frac{1}{2} (11 1 - 1) .

Define the local encoding macros

Enc_{1} (x, q) = if x then R_{y} (- π /4) (q) else R_{y} (π /4) (q),

Enc_{2} (x, q) = if x then σ_{x} (q) else q .

They have the judgments

x : Bit, q : Q ⊢ Enc_{1} (x, q) : Q, x : Bit, q : Q ⊢ Enc_{2} (x, q) : Q .

Write $z = J - 1$ . The decoder is

Dec (z, q) = if z then Enter (q) else Enter (H (q)) .

Its type is

z : Bit, q : Q ⊢ Dec (z, q) : Bit .

For $J = 1$ it reads the $X$ basis; for $J = 2$ it reads the $Z$ basis.

The prepared and stored carrier may be returned to the late-query continuation

q : Q ⊢ λ z : Bit . Dec (z, q) : Bit ⊸ Bit .

The continuation captures one quantum name, not the earlier input bits. Actual delivery of $z$ at the declared late event is an external scheduling hypothesis. A lambda term alone is not a physical freshness certificate.

Displayed formulas in this passage

unlabeled · line 1015
$R_{y} (θ) = e^{- i θ σ_{y} /2}, H = \frac{1}{2} (11 1 - 1) .$
unlabeled · line 1021
$Enc_{1} (x, q) = if x then R_{y} (- π /4) (q) else R_{y} (π /4) (q),$
unlabeled · line 1026
$Enc_{2} (x, q) = if x then σ_{x} (q) else q .$
unlabeled · line 1030
$x : Bit, q : Q ⊢ Enc_{1} (x, q) : Q, x : Bit, q : Q ⊢ Enc_{2} (x, q) : Q .$
Psy04-B@1#eq:decoderterm · line 1038
$Dec (z, q) = if z then Enter (q) else Enter (H (q)) .$
unlabeled · line 1045
$z : Bit, q : Q ⊢ Dec (z, q) : Bit .$
unlabeled · line 1053
$q : Q ⊢ λ z : Bit . Dec (z, q) : Bit ⊸ Bit .$

Local encoding and late decoding

Displayed formulas in this passage

Nearby in this section