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
In [3]:
Igate, Xgate, Ygate, Zgate, Hgate = Gate(I), Gate(X), Gate(Y), Gate(Z), Gate(H)
Igate: 
Xgate: 
Ygate: 
Zgate: 
Hgate: 
In [4]:
target = Gate(X).with_implicit_representation()
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))]))
unitary_gate_op: 
In [6]:
qubit_meas = Qcircuit(VertExprArray([Input(var_ket_psi)], [Measure(Z)], [Output(Ket(b))]))
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))]))
register_meas: 
In [8]:
circuit_Am = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, m)))
circuit_Am: 
In [9]:
circuit_Bn = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(B, i), one, n)))
circuit_Bn: 
In [10]:
circuit_Bk = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(B, i), one, k)))
circuit_Bk: 
In [11]:
circuit_Dm = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(D, i), one, m)))
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)))
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)))
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))]))
circuit_aUb: 
In [15]:
circuit_aU = Qcircuit(VertExprArray(
[*multi_input_entries(a, one, k, (one, k))],
U_1_to_m))
circuit_aU: 
In [16]:
circuit_Ua = Qcircuit(VertExprArray(
U_1_to_m,
[*multi_output_entries(a, one, k, (one, k))]))
circuit_Ua: 
In [17]:
circuit_Ub = Qcircuit(VertExprArray(
U_1_to_m,
[*multi_output_entries(b, one, k, (one, k))]))
circuit_Ub: 
In [18]:
circuit_b = Qcircuit(VertExprArray(
[*multi_input_entries(b, one, k, (one, k))]))
circuit_b: 
In [19]:
circuit_Akm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Aij, Rij), one, k)], one, m)))
circuit_Akm: 
In [20]:
circuit_Bkm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k)], one, m)))
circuit_Bkm: 
In [21]:
circuit_Bkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k)], one, n)))
circuit_Bkn: 
In [22]:
circuit_Ckm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Cij, Tij), one, k)], one, m)))
circuit_Ckm: 
In [23]:
circuit_Dkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Dij, Uij), one, k)], one, n)))
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)))
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)))
circuit_BkClm: 
In [26]:
no_1tok_in_Ts = ExprRange(i, ExprRange(j, Disjoint(Tij, Interval(one, k)), one, m), one, l)
no_1tok_in_Ts: 
In [27]:
no_1tok_in_Ts.body
In [28]:
no_1tok_in_Ts = (ExprRange(i, ExprRange(j, Disjoint(Tij, Interval(one, k)), one, m), one, l)
.with_wrapping_at(8, 16))
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)))
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)))
circuit_permuted_Bkn: 
In [31]:
circuit_compressed_inputAm = Qcircuit(
VertExprArray([*multi_input_entries(A, one, m, (one, m))]))
circuit_compressed_inputAm: 
In [32]:
circuit_compressed_outputAm = Qcircuit(
VertExprArray([*multi_output_entries(A, one, m, (one, m))]))
circuit_compressed_outputAm: 
In [33]:
circuit_expanded_inputBm = Qcircuit(
VertExprArray([ExprRange(k, Input(IndexedVar(B, k)), one, m)]))
circuit_expanded_inputBm: 
In [34]:
circuit_expanded_outputBm = Qcircuit(
VertExprArray([ExprRange(k, Output(IndexedVar(B, k)), one, m)]))
circuit_expanded_outputBm: 
In [35]:
N_0_to_m = var_range(N, zero, m)
N_0_to_m: 
In [36]:
N_0 = IndexedVar(N, zero)
N_0: 
In [37]:
N_m = IndexedVar(N, m)
N_m: 
In [38]:
N_km1 = IndexedVar(N, subtract(k, one))
N_km1: 
In [39]:
kth_start = Add(N_km1, one)
kth_start: 
In [40]:
N_k = IndexedVar(N, k)
N_k: 
In [41]:
each_Nk_is_partial_sum = And(Equals(N_0, zero),
ExprRange(k, Equals(N_k, Add(N_km1, n_k)), one, m))
each_Nk_is_partial_sum: 
In [42]:
input_Ak_nk = (list(multi_input_entries(A_k, kth_start, N_k, (one, n_k),
check_part_index_span=True))[0]
.with_wrapping_at(2, 6))
input_Ak_nk: 
In [43]:
output_Ak_nk = (list(multi_output_entries(A_k, kth_start, N_k, (one, n_k),
check_part_index_span=True))[0]
.with_wrapping_at(2, 6))
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, N_k).with_wrapping_at(2, 6)
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, N_k).with_wrapping_at(2, 6)
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))]))
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)))
circuit_psi_m_Vj: 
In [48]:
circuit_Ui_Vj = Qcircuit(VertExprArray(U_1_to_i, V_1_to_j))
circuit_Ui_Vj: 
In [49]:
circuit_Akl = Qcircuit(A11_to_Akl_varray)
circuit_Akl: 
In [50]:
circuit_Bkl = Qcircuit(B11_to_Bkl_varray)
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))]))
circuit__u_Akl_v: 
In [52]:
m_wire = multi_wire(m)
m_wire: 
In [53]:
n_wire = multi_wire(n)
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))]))
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))]))
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)))]))
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))]))
phase_kickback_on_register_circuit: 
In [58]:
%end common