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

Values and evaluation

Configurations and specified Born semantics › Values and evaluation · lines 511–576

I@2#eq:born-rule

Values are

v ::= * ∣ 0 ∣ 1 ∣ q ∣ λ x : A . t ∣ ⟨ v_{1}, v_{2} ⟩ .

Left-to-right call-by-value contexts are

E ::= [] ∣ E t ∣ v E ∣ ⟨ E, t ⟩ ∣ ⟨ v, E ⟩ ∣ let ⟨ x, y ⟩ = E in t ∣ let * = E in t ∣ if E then u else u^{'} ∣ V (E) ∣ Enter (E) .

They do not enter abstraction bodies, let-bodies, or conditional alternatives.

Administrative root reductions are

(λ x : A . t) v let ⟨ x, y ⟩ = ⟨ v, w ⟩ in t let * = * in t if 1 then u else u^{'} if 0 then u else u^{'} ⟶ t [v / x], ⟶ t [v / x, w / y], ⟶ t, ⟶ u, ⟶ u^{'} .

They preserve the state and are closed under $E$ . Together with allocation and gates,

[ψ, E [new]] ⟶_{d} [ψ \otimes ∣ 0 ⟩_{r}, E [r]] (r fresh),

[ψ, E [V (q_{S})]] ⟶_{d} [V_{S} ψ, E [q_{S}]],

they form the deterministic transitions.

The specified Born measurement transition is

[ψ, E [Enter (q_{S})]] ⟶_{B} [\frac{M ^{S} _{κ} ψ}{b _{κ}}, E [κ]] with probability b_{κ} = M^{S}_{κ} ψ^{2} > 0.

There is no transition on a zero-weight branch. Measured names are removed. For $S = \emptyset$ , the outcome is $*$ and the state is unchanged. A zero-qubit gate changes only an irrelevant phase.

The calculus with these transitions is $EC_{Born}$ . Equation (eq:born-rule) is a definition in Layer I.

Displayed formulas in this passage

I@2#eq:born-rule · line 556
$[ψ, E [Enter (q_{S})]] ⟶_{B} [\frac{M ^{S} _{κ} ψ}{b _{κ}}, E [κ]] with probability b_{κ} = M^{S}_{κ} ψ^{2} > 0.$
unlabeled · line 514
$v ::= * ∣ 0 ∣ 1 ∣ q ∣ λ x : A . t ∣ ⟨ v_{1}, v_{2} ⟩ .$
unlabeled · line 519
$E ::= [] ∣ E t ∣ v E ∣ ⟨ E, t ⟩ ∣ ⟨ v, E ⟩ ∣ let ⟨ x, y ⟩ = E in t ∣ let * = E in t ∣ if E then u else u^{'} ∣ V (E) ∣ Enter (E) .$
unlabeled · line 532
$(λ x : A . t) v let ⟨ x, y ⟩ = ⟨ v, w ⟩ in t let * = * in t if 1 then u else u^{'} if 0 then u else u^{'} ⟶ t [v / x], ⟶ t [v / x, w / y], ⟶ t, ⟶ u, ⟶ u^{'} .$
unlabeled · line 544
$[ψ, E [new]] ⟶_{d} [ψ \otimes ∣ 0 ⟩_{r}, E [r]] (r fresh),$
unlabeled · line 549
$[ψ, E [V (q_{S})]] ⟶_{d} [V_{S} ψ, E [q_{S}]],$