# Common expressions for the theory of proveit.physics.quantum.circuits¶

In [1]:
import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.

from proveit import (Function, Variable, IndexedVar, Conditional, ConditionalSet,
ExprRange, ExprTuple, VertExprArray, var_range)
from proveit import a, b, i, j, k, l, m, n, p, t, A, B, C, D, N, P, Q, R, S, U, pi
from proveit.core_expr_types import (
a_i, b_i, c_i, i_k, j_k, n_k, n_1_to_m, A_k, A_1_to_m,
U_1_to_m, U_1_to_i, V_1_to_j)
from proveit.core_expr_types.expr_arrays import (
Aij, Bij, Cij, Dij, Eij, Pij, Qij, Rij, Sij, Tij, Uij, Vij,
A11_to_Akl, A11_to_Akl_varray, B11_to_Bmn, B11_to_Bkl_varray,
D11_to_Dmn, S11_to_Smn)
from proveit.logic import (And, Equals, NotEquals, Set, InSet, CartExp, Disjoint,
InvImage)
from proveit.numbers import NaturalPos, Complex, Interval, zero, one, two, three
from proveit.numbers import Add, Neg, subtract, frac, sqrt, Exp, exp2pi_i, greater
from proveit.linear_algebra import VecAdd, ScalarMult, TensorProd
from proveit.physics.quantum import (
I, X, Y, Z, H, Ket, varphi, ket_plus, ket0, ket1, var_ket_u, var_ket_v, m_ket_domain,
var_ket_psi, NumKet, Qmult)
from proveit.physics.quantum.circuits import (
Qcircuit, Gate, Input, Output, Measure, MultiQubitElem,
control_elem, multi_wire, multi_gate_entries,
multi_input_entries, multi_output_entries, multi_measure_entries)
In [2]:
%begin common
Defining common sub-expressions for theory 'proveit.physics.quantum.circuits'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [3]:
Igate, Xgate, Ygate, Zgate, Hgate = Gate(I), Gate(X), Gate(Y), Gate(Z), Gate(H)
Out[3]:
Igate:
Xgate:
Ygate:
Zgate:
Hgate:
In [4]:
target = Gate(X).with_implicit_representation()
Out[4]:
target:
In [5]:
unitary_gate_op = Qcircuit(
VertExprArray([*multi_input_entries(var_ket_psi, one, m, (one, m))],
[*multi_gate_entries(U, one, m, (one, m))],
[*multi_output_entries(Qmult(U, var_ket_psi), one, m, (one, m))]))
Out[5]:
unitary_gate_op:
In [6]:
qubit_meas = Qcircuit(VertExprArray([Input(var_ket_psi)], [Measure(Z)], [Output(Ket(b))]))
Out[6]:
qubit_meas:
In [7]:
register_meas = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_psi, one, m, (one, m))],
[ExprRange(k, Measure(Z), one, m)],
[*multi_output_entries(NumKet(n, m), one, m, (one, m))]))
Out[7]:
register_meas:
In [8]:
circuit_Am = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, m)))
Out[8]:
circuit_Am:
In [9]:
circuit_Bn = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(B, i), one, n)))
Out[9]:
circuit_Bn:
In [10]:
circuit_Bk = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(B, i), one, k)))
Out[10]:
circuit_Bk:
In [11]:
circuit_Dm = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(D, i), one, m)))
Out[11]:
circuit_Dm:
In [12]:
circuit_AjBkCl = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, j),
ExprRange(i, IndexedVar(B, i), one, k),
ExprRange(i, IndexedVar(C, i), one, l)))
Out[12]:
circuit_AjBkCl:
In [13]:
circuit_AjDmCl = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, j),
ExprRange(i, IndexedVar(D, i), one, m),
ExprRange(i, IndexedVar(C, i), one, l)))
Out[13]:
circuit_AjDmCl:
In [14]:
circuit_aUb = Qcircuit(VertExprArray(
[*multi_input_entries(a, one, k, (one, k))],
U_1_to_m,
[*multi_output_entries(b, one, k, (one, k))]))
Out[14]:
circuit_aUb:
In [15]:
circuit_aU = Qcircuit(VertExprArray(
[*multi_input_entries(a, one, k, (one, k))],
U_1_to_m))
Out[15]:
circuit_aU:
In [16]:
circuit_Ua = Qcircuit(VertExprArray(
U_1_to_m,
[*multi_output_entries(a, one, k, (one, k))]))
Out[16]:
circuit_Ua:
In [17]:
circuit_Ub = Qcircuit(VertExprArray(
U_1_to_m,
[*multi_output_entries(b, one, k, (one, k))]))
Out[17]:
circuit_Ub:
In [18]:
circuit_b = Qcircuit(VertExprArray(
[*multi_input_entries(b, one, k, (one, k))]))
Out[18]:
circuit_b:
In [19]:
circuit_Akm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Aij, Rij), one, k)], one, m)))
Out[19]:
circuit_Akm:
In [20]:
circuit_Bkm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k)], one, m)))
Out[20]:
circuit_Bkm:
In [21]:
circuit_Bkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k)], one, n)))
Out[21]:
circuit_Bkn:
In [22]:
circuit_Ckm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Cij, Tij), one, k)], one, m)))
Out[22]:
circuit_Ckm:
In [23]:
circuit_Dkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Dij, Uij), one, k)], one, n)))
Out[23]:
circuit_Dkn:
In [24]:
circuit_AkClm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Aij, Rij), one, k),
ExprRange(j, MultiQubitElem(Cij, Tij), one, l)],
one, m)))
Out[24]:
circuit_AkClm:
In [25]:
circuit_BkClm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k),
ExprRange(j, MultiQubitElem(Cij, Tij), one, l)],
one, m)))
Out[25]:
circuit_BkClm:
In [26]:
no_1tok_in_Ts = ExprRange(i, ExprRange(j, Disjoint(Tij, Interval(one, k)), one, m), one, l)
Out[26]:
no_1tok_in_Ts:
In [27]:
no_1tok_in_Ts.body
Out[27]:
In [28]:
no_1tok_in_Ts = (ExprRange(i, ExprRange(j, Disjoint(Tij, Interval(one, k)), one, m), one, l)
.with_wrapping_at(8, 16))
Out[28]:
no_1tok_in_Ts:
In [29]:
circuit_permuted_Akm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j,
MultiQubitElem(IndexedVar(A, [pi, j]),
Function(InvImage(p), IndexedVar(R, [pi, j]))),
one, k)],
one, m)))
Out[29]:
circuit_permuted_Akm:
In [30]:
circuit_permuted_Bkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j,
MultiQubitElem(IndexedVar(B, [pi, j]),
Function(InvImage(p), IndexedVar(S, [pi, j]))),
one, k)],
one, n)))
Out[30]:
circuit_permuted_Bkn:
In [31]:
circuit_compressed_inputAm = Qcircuit(
VertExprArray([*multi_input_entries(A, one, m, (one, m))]))
Out[31]:
circuit_compressed_inputAm:
In [32]:
circuit_compressed_outputAm = Qcircuit(
VertExprArray([*multi_output_entries(A, one, m, (one, m))]))
Out[32]:
circuit_compressed_outputAm:
In [33]:
circuit_expanded_inputBm = Qcircuit(
VertExprArray([ExprRange(k, Input(IndexedVar(B, k)), one, m)]))
Out[33]:
circuit_expanded_inputBm:
In [34]:
circuit_expanded_outputBm = Qcircuit(
VertExprArray([ExprRange(k, Output(IndexedVar(B, k)), one, m)]))
Out[34]:
circuit_expanded_outputBm:
In [35]:
N_0_to_m = var_range(N, zero, m)
Out[35]:
N_0_to_m:
In [36]:
N_0 = IndexedVar(N, zero)
Out[36]:
N_0:
In [37]:
N_m = IndexedVar(N, m)
Out[37]:
N_m:
In [38]:
N_km1 = IndexedVar(N, subtract(k, one))
Out[38]:
N_km1:
In [39]:
kth_start = Add(N_km1, one)
Out[39]:
kth_start:
In [40]:
kth_end = N_k = IndexedVar(N, k)
Out[40]:
kth_end:
In [41]:
each_Nk_is_partial_sum = And(Equals(N_0, zero),
ExprRange(k, Equals(N_k, Add(N_km1, n_k)), one, m))
Out[41]:
each_Nk_is_partial_sum:
In [42]:
input_Ak_nk = (list(multi_input_entries(A_k, kth_start, kth_end, (one, n_k),
check_part_index_span=True))[0]
.with_wrapping_at(2, 6))
Out[42]:
input_Ak_nk:
In [43]:
output_Ak_nk = (list(multi_output_entries(A_k, kth_start, kth_end, (one, n_k),
check_part_index_span=True))[0]
.with_wrapping_at(2, 6))
Out[43]:
output_Ak_nk:
In [44]:
consolidated_input_A_1_to_m = ExprRange(
i, MultiQubitElem(Input(TensorProd(A_1_to_m), part=i),
targets=Interval(one, N_m)), kth_start, kth_end).with_wrapping_at(2, 6)
Out[44]:
consolidated_input_A_1_to_m:
In [45]:
consolidated_output_A_1_to_m = ExprRange(
i, MultiQubitElem(Output(TensorProd(A_1_to_m), part=i),
targets=Interval(one, N_m)), kth_start, kth_end).with_wrapping_at(2, 6)
Out[45]:
consolidated_output_A_1_to_m:
In [46]:
circuit_Ui_psi_m = Qcircuit(
VertExprArray(U_1_to_i.with_front_expansion(1),
[*multi_output_entries(var_ket_psi, one, m, (one, m))]))
Out[46]:
circuit_Ui_psi_m:
In [47]:
circuit_psi_m_Vj = Qcircuit(
VertExprArray([*multi_input_entries(var_ket_psi, one, m, (one, m))],
V_1_to_j.with_front_expansion(1)))
Out[47]:
circuit_psi_m_Vj:
In [48]:
circuit_Ui_Vj = Qcircuit(VertExprArray(U_1_to_i, V_1_to_j))
Out[48]:
circuit_Ui_Vj:
In [49]:
circuit_Akl = Qcircuit(A11_to_Akl_varray)
Out[49]:
circuit_Akl:
In [50]:
circuit_Bkl = Qcircuit(B11_to_Bkl_varray)
Out[50]:
circuit_Bkl:
In [51]:
circuit__u_Akl_v = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_u, one, l, (one, l))],
ExprRange(i, ExprTuple(ExprRange(j, Aij, one, l)),
one, k),
[*multi_output_entries(var_ket_v, one, l, (one, l))]))
Out[51]:
circuit__u_Akl_v:
In [52]:
m_wire = multi_wire(m)
Out[52]:
m_wire:
In [53]:
n_wire = multi_wire(n)
Out[53]:
n_wire:
In [54]:
circuit__psi_m__u_Akl_v = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_psi, one, m, (one, m)),
*multi_input_entries(var_ket_u, Add(m, one), Add(m, l), (one, l))],
ExprRange(i, ExprTuple(multi_wire(m),
ExprRange(j, Aij, one, l)),
one, k),
[*multi_output_entries(var_ket_psi, one, m, (one, m)),
*multi_output_entries(var_ket_v, Add(m, one), Add(m, l), (one, l))]))
Out[54]:
circuit__psi_m__u_Akl_v:
In [55]:
circuit__u_Akl_v__psi_m = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_u, one, l, (one, l)),
*multi_input_entries(var_ket_psi, Add(l, one), Add(l, m), (one, m))],
ExprRange(i, ExprTuple(ExprRange(j, Aij, one, l),
multi_wire(m)),
one, k),
[*multi_output_entries(var_ket_v, one, l, (one, l)),
*multi_output_entries(var_ket_psi, Add(l, one), Add(l, m), (one, m))]))
Out[55]:
circuit__u_Akl_v__psi_m:
In [56]:
phase_kickback_circuit = Qcircuit(VertExprArray(
[Input(ket_plus), *multi_input_entries(var_ket_u, two, Add(m, two), (one, Add(m, one)))],
[control_elem(two), *multi_gate_entries(U, two, Add(m, two), (one, Add(m, one)))],
[Output(ScalarMult(frac(one, sqrt(two)), VecAdd(ket0, ScalarMult(exp2pi_i(varphi), ket1)))),
*multi_output_entries(var_ket_u, two, Add(m, two), (one, Add(m, one)))]))
Out[56]:
phase_kickback_circuit:
In [57]:
phase_kickback_on_register_circuit = Qcircuit(VertExprArray(
[ExprRange(i, Input(ket_plus), one, t),
*multi_input_entries(var_ket_u, Add(t, one), Add(t, m), (one, m))],
ExprRange(i,
[ExprRange(j, ConditionalSet(
Conditional(control_elem(Add(t, one)),
Equals(i, j)),
Conditional(Gate(I), NotEquals(i, j))),
one, t).with_case_simplification(),
*multi_gate_entries(IndexedVar(U, i), Add(t, one), Add(t, m), (one, m))],
one, t).with_case_simplification(),
[ExprRange(i, Output(ScalarMult(frac(one, sqrt(two)),
VecAdd(ket0, ScalarMult(exp2pi_i(IndexedVar(varphi, i)), ket1)))),
one, t),
*multi_output_entries(var_ket_u, Add(t, one), Add(t, m), (one, m))]))
Out[57]:
phase_kickback_on_register_circuit:
In [58]:
%end common
These common expressions may now be imported from the theory package: proveit.physics.quantum.circuits