Expression of type Lambda ¶

from the theory of proveit.physics.quantum.QPE ¶

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, ExprRange, Lambda, Variable, VertExprArray, a, b
from proveit.logic import And, InSet, NotEquals
from proveit.numbers import Add, Interval, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE, _U, _ket_u, _m_domain, _s, _s_wire, _t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(_t, one)
sub_expr3 = Add(_t, _s)
sub_expr4 = Interval(one, _t)
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire]
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr8 = ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)
sub_expr9 = [ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)]
sub_expr10 = [ExprRange(sub_expr1, sub_expr7, one, _t), ExprRange(sub_expr1, sub_expr7, sub_expr2, sub_expr3)]
expr = Lambda([a, b], Conditional(NotEquals(Qcircuit(vert_expr_array = VertExprArray(sub_expr9, sub_expr10, sub_expr6, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(a, _t), part = sub_expr1), targets = sub_expr4), one, _t), sub_expr8])), Qcircuit(vert_expr_array = VertExprArray(sub_expr9, sub_expr10, sub_expr6, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(b, _t), part = sub_expr1), targets = sub_expr4), one, _t), sub_expr8]))), And(InSet(a, _m_domain), InSet(b, _m_domain), NotEquals(a, b))))

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(a, b\right) \mapsto \left\{\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert a \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert a \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert a \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert a \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) \neq \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert b \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert b \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) \textrm{ if } a \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  b \in \{0~\ldotp \ldotp~2^{t} - 1\} ,  a \neq b\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Lambda	parameters: 19 body: 1
1	Conditional	value: 2 condition: 3
2	Operation	operator: 18 operands: 4
3	Operation	operator: 5 operands: 6
4	ExprTuple	7, 8
5	Literal
6	ExprTuple	9, 10, 11
7	Operation	operator: 13 operands: 12
8	Operation	operator: 13 operands: 14
9	Operation	operator: 16 operands: 15
10	Operation	operator: 16 operands: 17
11	Operation	operator: 18 operands: 19
12	ExprTuple	21, 22, 23, 20
13	Literal
14	ExprTuple	21, 22, 23, 24
15	ExprTuple	113, 25
16	Literal
17	ExprTuple	115, 25
18	Literal
19	ExprTuple	113, 115
20	ExprTuple	26, 34
21	ExprTuple	27, 28
22	ExprTuple	29, 30
23	ExprTuple	31, 32
24	ExprTuple	33, 34
25	Operation	operator: 94 operands: 35
26	ExprRange	lambda_map: 36 start_index: 116 end_index: 117
27	ExprRange	lambda_map: 37 start_index: 116 end_index: 117
28	ExprRange	lambda_map: 38 start_index: 116 end_index: 118
29	ExprRange	lambda_map: 39 start_index: 116 end_index: 117
30	ExprRange	lambda_map: 39 start_index: 103 end_index: 104
31	ExprRange	lambda_map: 40 start_index: 116 end_index: 117
32	ExprRange	lambda_map: 41 start_index: 116 end_index: 118
33	ExprRange	lambda_map: 42 start_index: 116 end_index: 117
34	ExprRange	lambda_map: 43 start_index: 116 end_index: 118
35	ExprTuple	44, 45
36	Lambda	parameter: 102 body: 46
37	Lambda	parameter: 102 body: 47
38	Lambda	parameter: 102 body: 48
39	Lambda	parameter: 102 body: 49
40	Lambda	parameter: 102 body: 50
41	Lambda	parameter: 102 body: 51
42	Lambda	parameter: 102 body: 52
43	Lambda	parameter: 102 body: 54
44	Literal
45	Operation	operator: 111 operands: 55
46	Operation	operator: 64 operands: 56
47	Operation	operator: 86 operands: 57
48	Operation	operator: 64 operands: 58
49	Operation	operator: 64 operands: 59
50	Operation	operator: 60 operands: 61
51	Operation	operator: 87 operands: 62
52	Operation	operator: 64 operands: 63
53	ExprTuple	102
54	Operation	operator: 64 operands: 65
55	ExprTuple	66, 67
56	NamedExprs	element: 68 targets: 76
57	NamedExprs	state: 69
58	NamedExprs	element: 70 targets: 78
59	NamedExprs	element: 71 targets: 72
60	Literal
61	NamedExprs	basis: 73
62	NamedExprs	operation: 74
63	NamedExprs	element: 75 targets: 76
64	Literal
65	NamedExprs	element: 77 targets: 78
66	Operation	operator: 79 operands: 80
67	Operation	operator: 81 operand: 116
68	Operation	operator: 92 operands: 83
69	Operation	operator: 84 operand: 98
70	Operation	operator: 86 operands: 93
71	Operation	operator: 87 operands: 88
72	Operation	operator: 94 operands: 89
73	Literal
74	Literal
75	Operation	operator: 92 operands: 90
76	Operation	operator: 94 operands: 91
77	Operation	operator: 92 operands: 93
78	Operation	operator: 94 operands: 95
79	Literal
80	ExprTuple	96, 117
81	Literal
82	ExprTuple	116
83	NamedExprs	state: 97 part: 102
84	Literal
85	ExprTuple	98
86	Literal
87	Literal
88	NamedExprs	operation: 99 part: 102
89	ExprTuple	116, 104
90	NamedExprs	state: 100 part: 102
91	ExprTuple	116, 117
92	Literal
93	NamedExprs	state: 101 part: 102
94	Literal
95	ExprTuple	103, 104
96	Literal
97	Operation	operator: 108 operands: 105
98	Literal
99	Operation	operator: 106 operands: 107
100	Operation	operator: 108 operands: 109
101	Literal
102	Variable
103	Operation	operator: 111 operands: 110
104	Operation	operator: 111 operands: 112
105	ExprTuple	113, 117
106	Literal
107	ExprTuple	114, 117
108	Literal
109	ExprTuple	115, 117
110	ExprTuple	117, 116
111	Literal
112	ExprTuple	117, 118
113	Variable
114	Literal
115	Variable
116	Literal
117	Literal
118	Literal

Expression of type Lambda¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type Lambda ¶

from the theory of proveit.physics.quantum.QPE ¶