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

Definition: Record-independent measurement form

Typed records and experiment interfaces › The record transformation · lines 974–1004

I@2#def:record, I@2#eq:record-source, I@2#eq:record-target

Let $L = S ⊔ B$ , $∣ S ∣ = k$ , and suppose

(q : Q)_{q \in B} ⊢ u : Bit^{\otimes m} .

The source term is

t_{S, u} = let x = Enter (q_{S}) in ⟨ u, x ⟩, x \in / u .

Its deferred term is

defer_{S} (t_{S, u}) = let r = new^{k} in let ⟨ s, r^{'} ⟩ = C_{k} (⟨ q_{S}, r ⟩) in ⟨ ⟨ u, Enter (r^{'}) ⟩, s ⟩ .

Here $new^{k}$ denotes a tuple of $k$ fresh allocations. The continuation consumes the entire register $B$ . It may contain allocations, gates, readouts, and classical control, but uses neither source nor record names.

Displayed formulas in this passage

I@2#eq:record-source · line 981
$t_{S, u} = let x = Enter (q_{S}) in ⟨ u, x ⟩, x \in / u .$
I@2#eq:record-target · line 988
$defer_{S} (t_{S, u}) = let r = new^{k} in let ⟨ s, r^{'} ⟩ = C_{k} (⟨ q_{S}, r ⟩) in ⟨ ⟨ u, Enter (r^{'}) ⟩, s ⟩ .$
unlabeled · line 977
$(q : Q)_{q \in B} ⊢ u : Bit^{\otimes m} .$

Definition: Record-independent measurement form

Displayed formulas in this passage

Nearby in this section