=Paper=
{{Paper
|id=None
|storemode=property
|title=A history and reversibility for quantum programming language QML
|pdfUrl=https://ceur-ws.org/Vol-2264/paper3.pdf
|volume=Vol-2264
|authors=Nely Plata César,J. Raymundo Marcial Romero,J. Antonio Hernández Servín
|dblpUrl=https://dblp.org/rec/conf/lanmr/CesarMS18
}}
==A history and reversibility for quantum programming language QML==
https://ceur-ws.org/Vol-2264/paper3.pdf
A History and Reversibility for Quantum
Programming Language QML
Nely Plata César1 , J. Raymundo Marcial Romero1 , and J. Antonio Hernández
Servı́n1
Facultad de Ingenierı́a
Universidad Autónoma del Estado de México
Abstract. We developed an operational model that incorporates a
history track for the quantum programming language QML, consider-
ing classical and quantum data, and omitting measurements. With the
history, the reversibility can be explicitly and naturally applied from
the proposed rules. The language is worked first with classical data
and extrapolated to quantum data.
Keywords: Functional quantum programming QML · History · Re-
versibility.
1 Introduction
There are several quantum programming languages, based on the imperative,
functional or other paradigms. Only a few are described below: QML [1], nQML
[2] and Quantum Lambda Calculus (λq ) [3] with operational semantics and im-
plicit reversibility, and QML and nQML have denotational semantic and imple-
mentation, but only λq have a history track and measurements.
Some languages based on imperative paradigm are: QCL [4], LanQ [5] and
qGCL [6], all three with measurements; QCL and LanQ have an implementation
and implicit reversibility, but only LanQ and qGCL have operational semantic.
And based on other paradigms are pQCL [7], QPAlg [8], CQP [9,10], etc [11–13].
We will focus on QML developed by Grattage y Altenkirch, is a first order
language and has finite data-types, the semantics of QML assigns to every well-
typed program a quantum circuit, the computations have the property of being
reversible and irreversible. Also implements the notion of quantum control if,
which would lead to implicit measurements and quantum collapse [1, 7].
Several authors have considered this language, is the case of Dı́az-Caro, Ar-
righi, Gadella y Grattage who give an idea to implement a history track and
quantum measurements [14–16]. Altenkirch, Grattage, Vizzotto and Sabry not
define operational semantics in terms of circuits and develop a sound and com-
plete equational theory omitting measurements, they work QML subdividing
the classical and quantum part of the language [17]. Also Lampis, Ginis, Pa-
pakyriakou and Papaspyrou define nQML with quantum data and control, an
interpreter written in Haskell and being a more intuitive language [2].
25
Quantum languages must consider the implicit property of reversibility, if the
operations are defined as unit matrix, and therefore, if the previous immediate
matrix is applied to actual state, it can be returned to the previous step, and
successively.
The contribution of this article is incorporate a history track to the opera-
tional model, the track will store the operations performed in a program. With
this, reversibility can be explicitly executed. The above is added to QML lan-
guage defined by Altenkirch, Grattage, Vizzotto and Sabry [17]. Our research
guide is proposed by Dı́az-Caro, Arrigui, Gadella and Grattage, who work a sim-
ilar area but in the quantum lambda calculus language [14]. The resulting oper-
ational model considers classical and quantum data (superpositions), preserving
orthogonality in programs that consider if. The rules to apply reversibility based
on the history track are also defined.
2 Preliminaries
2.1 Quantum computing
There are four principles or postulates that define the behavior of quantum
computing. The pure states are unitary vectors, which store in memory the in-
formation used. Evolution, this indicates how change from one state to another,
for which unit matrices are applied, they have implicit instructions that the com-
puter will carry out and that will be applied to the state to evolve. Measurement
or observation focuses on the existence of an observer who, upon seeing the state
of the system, will determine with what probability a result can happen, imply-
ing a collapse of the system. Composite systems, will be in charge of defining
states conformed by states of different systems and how they interact among
them [18, 19].
2.2 Quantum programming language QML
QML is a functional quantum language introduced by Grattage and Altenkirch,
they apply quantum properties and develop a denotational and operational se-
mantics [1, 20]. Subsequently, they research and develop a sound and complete
equational theory, omitting recursive types and measurements [17]. This latest
research will be retaken, which describes its syntax.
(Variables) x, y, . . . ∈ V ars (Terms) t, u ::= x | () | (t, u)
(Prob. amplitudes) κ, ι, . . . ∈ C | let p = t in u| f alse
(Patterns) p, q ::= x | (x, y) | true| 0 | κ ∗ t | t + u
| if◦ t then u else u0
From the syntax you can form conventional programs such as tuples, let, if,
among others, and in turn append terms with a probability amplitude κ, that is,
have a probability value that they happen, and also define superposition t + u,
it means than a term can be in t and u at the same time.
The types are given by the grammar: σ = Q1 |Q2 |σ ⊗ τ , where Q1 is the type
(), which carry no information and Q2 corresponds to qubits (0 and 1). The
26
types are finite and non-recursive, and the only types that can be represented
are those in the collection of qubits.
Typing contexts (Γ, ∆) are given by: Γ, x : σ = •|Γ, x : σ, where • stands
for the empty context. We context correspond to functions from a finite set of
variables to types. For this case, we assume that every variable appears at most
once. To maps pairs of contexts to contexts, the ⊗ operator is incorporated, with
the following operation:
Γ, x : σ ⊗ ∆, x : σ = (Γ ⊗ ∆), x : σ
Γ, x : σ ⊗ ∆ = (Γ ⊗ ∆), x : σ si x ∈
/ dom∆
•⊗∆ =∆
Interpret a judgement Γ ` t : σ as a function is JΓ ` t : σ K ∈ JΓ K → Jσ K,
where, given a typing contexts, it returns a type of the collection of qubits.
To define well-formed programs Γ ` t : σ, the rules can be observed in Table
1. For example: Γ ⊗ ∆ ` if◦ c then t else u : σ, requires that Γ ` c : Q2 and
∆ ` t, u : σ, that is, c has a value of qubit, and t and u are the same type.
Γ `t:σ ∆, x : σ ` t : τ Γ ` c : Q2 ∆ ` t, u : σ ◦
var let if
x:σ`x:σ Γ ⊗ ∆ ` let x = t in u : τ Γ ⊗ ∆ ` if◦ c then t else u : σ
Γ `t:σ ∆`u:τ
⊗ intro f-intro t-intro
Γ ⊗ ∆ ` (t, u) : σ ⊗ τ • ` false : Q2 • ` true : Q2
Γ `t:σ⊗τ ∆, x : σ, y : τ ` u : ρ Γ, x : Q1 ` t : σ
⊗ −elim wk-unit unit
Γ ⊗ ∆ ` let (x, y) = t in u : ρ Γ `t:σ • ` () : Q1
Table 1: Typing classical terms (Source: [17], p. 29).
Semantically the types are described as JQ1 K = {0}, JQ2 K = {0, 1} and
Jσ ⊗ τ K = Jσ K × Jτ K, where tensor product returns a types tuple. This informa-
tion will be taken as basis for QML; next, a brief introduction about the history
and reversibility.
2.3 Quantum history
The quantum computation implicitly has the property of reversibility, for this,
several authors have made contributions in classical and quantum computation
[21–24]. For example Van Tonder proposes in quantum lambda calculus a history
stack that stores the executed operations in a program [3]. For reversibility, we
propose that is enough sufficient to execute operations in reverse order and return
to initial value.
Our proposal will be described below, which is based on modifying the op-
erational model, to which are added inverse functions that allow storing the
operation executed in a certain step; also the functions used in the model are
modified and appended.
3 Quantum Data and Control
In this section the history stack is added to operational model, as well as the
functions and rules to execute a program and reversibility. The base model is
27
located at Appendix 1. Our operational model stores the inverse operations
executed during a certain derivation. The rules are observed in Table 2.
J• ` () : Q1 KQ = (const 0)−1
− ; const 0
J• ` f alse : Q2 KQ = (const 0)−1
− ; const 0
J• ` true : Q2 KQ = (const 1)−1
− ; const 1
Jx : σ ` x : σ KQ = id−1
+− ; id+
JΓ ⊗ ∆ ` let x = t in u : σ KQ = g ∗ ◦ (f ∗ × id∗−1
−
−1
; id∗ ) ◦ (δΓ,∆− ; δΓ,∆ )
where f = JΓ ` t : σ KQ
g = J∆, x : σ ` u : τ KQ
JΓ ⊗ ∆ ` (t,u) : σ ⊗ τ K Q
= (f × g ) ◦ ((δΓ,∆ )−1
∗ ∗
− ; δΓ,∆ )
where f = JΓ ` t : σ KQ
g = J∆ ` u : τ KQ
JΓ ⊗ ∆ ` let (x,y) = t in u : ρ KQ
= g ◦ (f × id∗−1
∗ ∗
−
−1
; id∗ ) ◦ (δΓ,∆− ; δΓ,∆ )
where f = JΓ ` t : σ ⊗ σ KQ
g = J∆, x : σ, y : τ ` u : ρ KQ
= (g ∗ |h∗ ) ◦ (f ∗ × id∗−1
Q
JΓ ⊗ ∆ ` if◦ c then t else u : σ K − ; id∗ )
◦ ((δΓ,∆ )−1
− ; δΓ,∆ )
where f = JΓ ` c : Q2 K
g = J∆ ` t : σ K
h = J∆ ` u : σ K
Q
JΓ ` t : σ K = (f × id+−1
− ; id+ )
where f = JΓ , x : Q1 ` t : σ KQ
Table 2: Operational rules.
Rules like J• ` f alse : Q2 K = (const 0)−1
Q
− ; const 0, that is, if you have a
f alse term, then the function const 0 is applied, and its inverse is stored. This
is similar for all statements.
3.1 Auxiliary functions
Considering the auxiliary functions (Appendix 2) defined in the operational
model (with quantum operations), the authors extend the functions using a
Kleisli Triple, where each derivation returns a complex vector [17, 25, 26].
We develop the inverse functions (.−1 ) and the r function applied to all, such
that later allow the reversibility. The r function is responsible for storing the
argument received respectively.
In quantum environment the states are complex unit vectors and can be
in superposition, to achieve this, Kleisli Triple are used [17, 25]. With this, we
28
Q Q
interpret judgements Γ ` t : σ as a function JΓ K → Jσ K , where Jσ K = Jσ K →
Q
C represents complex vectors over the base set Jσ K; Jσ K is denoted as V Jσ K.
Remember that σ is a type, defined from σ = Q1 |Q2 |σ ⊗ τ , interpreted as:
JQ2 K = {0, 1} (associated with qubits) and JQ1 K (no information).
Definition 1 (Triple Kleisli). A Triple Kleisli on a category C, is defined by
tuple (V, return, ∗ ), where:
– V :C→C
– return : S → V S, for S ∈ C
– f ∗ : V S → V T , for f : S → V T
To work with complex vectors, it is required modify the functions of the
operational model by implementing Kleisli Triple. Every function of type S → T
turns to a function of type S → V T using the return function; this must be
done for all the classical auxiliary functions (Appendix 2). For example, consider
the function const a : JQ1 K → S, then, adjusting Kleisli Triple, you get: return ◦
const a : JQ1 K → V S. We use const a = return ◦ const a.
Now, we define an r function which allows to carry the input arguments and
output for any auxiliary function f .
Let f be any auxiliary function where classically f : Jσ K → Jτ K, such that
Q
f (a) = b. Then, the function r has type Jσ K → Jτ K , e.g. r : Jσ K → Jτ K → C
Q
(by definition of Jτ K ), defined as r(a f (a)) = α, α ∈ C, where (r a f (a)) = 1.0
if a = f (a) and 0.0 otherwise. So f a = r(a f (a)). Our function r has a call-by-
name evaluation mechanism, so its argument will not be evaluated until needed.
The following functions are part of our contribution. For each auxiliary func-
tions f we consider r to define the inverse f −1 , the lift f ∗ (associated with a
Kleisli Triple) and its inverse f ∗−1 . Consider S ∈ JQ2 K, the modified functions
are:
– id : S → (S → S → C), this function returns the argument it receives, and
is defined as: id(a) = (r a a).
id∗ : (S → V S) → (S → S → C) defined as: id∗ (r a0 a) = (r a0 a)
id−1 : (S → V S) → S defined as: id−1 (r a0 a) = a
id∗−1 : (S → V S) → (S → S → C) defined as: id∗−1 (r a0 a) = (r a0 a)
– id+ : S → (S → JQ1 K → C), concatenates the received argument with the
value 0 and is defined as: id+ (a) = (r a 0, r 0 a)
id+∗ : (S → V S) → (S → JQ1 K → C) × (S → S → C) defined as:
id+∗ (r a0 a) = (r a 0, r(0 a), and the other options are defined as:
a, if b=0
id+−1 (r a0 b, r a0 a) =
b, if b=1
id +∗−1
(r a 0, r a a) = (r a0 a)
0 0
– id+ : (JQ1 K × S) → (S → S → C) defined as: id+ (0, a) = (r a a)
id∗+ : (S → V JQ1 K) × (S → V S) → (S → S → C) defined with the
conditions: id∗+ (r a0 0, r a0 a) = (r a0 a) and id∗+ (r a00 1, r a0 a) = (r a0 1)
id−1 0
+ (r a a) = (0, a)
∗−1
id+ (r a0 a) = (r a0 a, r 0 a)
29
– const a : JQ1 K → (JQ1 K → S → C) is defined as: const a(0) = (r 0 a)
const a∗ : (S → V S) → (JQ1 K → S → C) defined as: const a∗ (r a0 a00 ) =
(r 0 a), and its inverse as: (
−1 0 −1 0 1, if a=0
const 0 (r a a) = 0, and const 1 (r a a) =
0, if a=1
(
∗−1 0 ∗−1 0 r a 1, if a=0
const 0 (r a a) = (r a 0), and const 1 (r a a) =
r a 0, if a=1
– δ : S → ((S → S → C) × (S → S → C)) double the argument received,
defined as: δ(a) = (r a a, r a a)
δ ∗ : (S → V S) → ((S → S → C) × (S → S → C)), defined as: δ(r a0 a) =
(r a0 a, r a0 a), and
δ −1 (r a0 a, r a0 a) = a
δ ∗−1 (r a00 a, r a0 a) = (r a0 a)
– swap : (S × T ) → (S → T → C) × (T → S → C), function that exchanges
the arguments, defined as: swap(a, b) = (r a b, r b a)
swap∗ : ((S → V S) × (S → V T )) → ((S → T → C)) × (T → S → C))
defined as: swap∗ (r a0 a, r b0 b) = (r a b, r b a)
swap−1 (r a b, r b a) = (a, b)
swap∗−1 (r a0 b, r b0 a) = (r b a, r a b)
– f × g; for any two functions:
f : S1 → (S1 → V T1 ), and f ∗ : (S1 → V S10 ) → (S10 → T1 → C)
g : S2 → (S2 → V T2 ), and g ∗ : (S2 → V S20 ) → (S20 → T2 → C), we have:
f × g : (S1 × S2 ) → (S1 → T1 → C) × (S2 → T2 → C) is defined as:
f × g (a, b) = (f a, g b)
f ∗ × g ∗ : (S1 → V S10 ) × (S2 → V S20 ) → (S10 → T1 → C) × (S20 → T2 → C),
defined as: f ∗ × g ∗ (r a0 a, r b0 b) = (f ∗ (r a0 a), g ∗ (r b0 b))
(f −1 × g −1 ) (r a0 a, r b0 b) = (f −1 (r a0 a), g −1 (r b0 b))
(f ∗−1 × g ∗−1 ) (r a0 a, r b0 b) = (f ∗−1 (r a0 a), g ∗−1 (r b0 b))
– δΓ,∆ , separate contexts depending on the program formed, the conditions
are below.
δΓ,∆ : JΓ ⊗ ∆ K → (S → JΓ K → C) × (S → J∆ K → C) defined as: δΓ,∆ (a ⊗
a0 ) = ((r a a), (r a0 a0 )), if one of the contexts is empty •, then it applies:
δΓ,∆ (a) = (r a a). The function with ∗ is defined as:
∗
δΓ,∆ ((r a a0 ) ⊗ (r b b0 )) = ((r a a0 ), (r b b0 )) or δΓ,∆
∗
(r a a0 ) = (r a a0 ), the
inverse functions are obtained similarly to the previous cases.
The conditions
are the following:
δΓ 0 ,∆0 × δ
if Γ = Γ 0 , x : σ y ∆ = ∆0 , x : σ
(δΓ,∆ ) = δΓ 0 ,∆ × id if Γ = Γ 0 , x : σ y x ∈/ dom(∆)
+
id if Γ = •
– (f |g) : (JQ2 K × S) → (S → T → C), is associated with if ◦ conditional,
defined as: (f |g) (1, a) = (f a) and (f |g) (0, a) = (g a).
(f −1 |g −1 ) : (S → V T ) → ((S → S → C) × (S → S → C)), defined as:
30
(
−1 −1 0 (a, f −1 a) if a=1
(f |g )(r a a) = −1
(a, g a) if a=0
(f ∗ |g ∗ ) : (S → V S) × (S → V S) → (S → T → C), defined as:
(f ∗ |g ∗ ) (r a0 1, r a0 a) = f ∗ (r a0 a) or (f ∗ |g ∗ ) (r a0 0, r a0 a) = g ∗ (r a0 a)
(f ∗−1 |g ∗−1 ) : (S → V T ) → (S → S → C) × (S → S → C)
(
∗−1 ∗−1 0 ((r a0 a), f ∗−1 (r a0 a)) if a=0
(f |g ) (r a a) = 0 ∗−1 0
((r a a), g (r a a)) if a=1
Consider the following: (f × g)∗ = f ∗ × g ∗ and (f × g)−1 = f −1 × g −1 .
With the previous rules and functions, certain programs can be derived, how-
ever, we still need define the modified rules for terms with probability amplitudes
and superpositions. The new rules to form well-typed judgements and for de-
riving terms (quantum and classic) are in Table 3 and Table 4, respectively.
Based on these definitions, we propose the modification that also allows storing
operations in the history stack.
Γ `◦ c : Q2 ∆ `◦ t, u : σ
#» z-intro if◦
•` 0 :σ Γ ⊗ ∆ `◦ if◦ c then t else u : σ
Γ `t:σ Γ `◦ t, u : σ t ⊥ u |λ|2 + |κ|2 = 1
prob sup◦
Γ `κ+t:σ Γ `◦ λ ∗ t + κ ∗ u : σ
Γ ` t, u : σ Γ `◦ t : σ Γ ` t ≡ u : σ
sup subst
Γ `t+u:σ Γ `◦ u : σ
Table 3: Typing quantum data (II) (Source: [17], p. 36,38).
3.2 Operational model for quantum control with history
Three rules are attached that consider: the vector zero, a term with a certain
probability amplitude and superposition.
If we have quantum data and control, consider the programs that contain
if ◦ or t + u, its terms must be orthogonal to each other. This is denoted in the
derivations with the symbol `◦ , the orthogonality with ⊥ and internal product
with h | i. To satisfy orthogonality we can see Table 5, and for a quantum terms
well formed see Table 3.
Having the above, now we can apply the operational model with a program,
Q
for example: J• ⊗ • ` if◦ 1 then (−1) ∗ true + f alse else true + f alse : Q2 K =
∗ ∗ ∗ ∗−1 ∗ −1
(g |h ) ◦ (f × id− ; id ) ◦ ((δΓ,∆ ) ; δΓ,∆ ).
At this point, the functions are mixed with their inverses, which must be sepa-
rated, how to achieve this we will define immediately.
31
−1
J• ` 0 : σ KQ = const v− ; const v where ∀a ∈ Jσ K.v a = 0.0
Q
JΓ ` κ ∗ t : σ K = (κ) ∗ f where ∀b ∈ JΓ K
f = JΓ ` t : σ KQ
1
JΓ ` t + u : σ KQ = √ f + g
where ∀a ∈ JΓ K
2
f = JΓ ` t : σ KQ
g = JΓ ` u : σ KQ
Table 4: Operational rules for quantum data.
#»
ht|ti = 1 if t 6= 0 hλ ∗ t + λ0 ∗ t0 |ui = λ ∗ ht|ui + λ0 ∗ ht0 |ui
hf alse|truei = 0 ht|κ ∗ u + κ0 ∗ u0 i = κ ∗ ht|ui + κ0 ∗ ht|u0 i
htrue|f alsei = 0
hλ ∗ t|ui = λ ht|ui
#» #»
h 0 |truei = 0 = htrue| 0 i ht|λ ∗ ui = λ ∗ ht|ui
#» #»
h 0 |f alsei = 0 = hf alse| 0 i ht + t0 |ui = ht|ui + ht0 |ui
#» #»
h 0 |xi = 0 = hx| 0 i ht|u + u0 i = ht|ui + ht|u0 i
0 0 0 0
h(t, t )|(u, u )i = ht|ui ∗ ht |u i ht|ui =? otherwise
Table 5: Inner products and orthogonality (Source: [17], p. 38).
4 History and Reversibility
To apply reversibility, several points are important: A concept called a history
stack and auxiliary functions defined in our proposal of the operational model.
Considering that each derivation is given from functions, and these are stored in
a stack, then, the inverse functions will result in reversibility, allowing returns to
the initial argument of the program. Formally, the terms and the history stack
make a computational state, that is:
Definition 2 (Computational state). The computational state is a sequence
of the form:
htn − ; · · · ; ht2 − ; ht1 − ; t1 ◦ t2 ◦ · · · ◦ tn
where htn − ; · · · ; ht2 − ; ht1 − , is called the history track and t1 ◦ t2 ; ◦ · · · ◦ tn ,
the computational register.
Regarding hti − ; ti , the part hti represents and stores the inverse operation that
executes ti .
Definition 3. H, denotes the (possibly empty) history track.
To arrive at the computational state, the terms must be factored, considering
different cases.
32
4.1 Factorization
Let the expression ht1 − ; t1 ◦ ht2 − ; t2 ◦ · · · ◦ htn − ; tn , where the semicolon (;)
denotes string concatenation. The hti expressions are histories corresponding to
each term ti , respectively. The terms ti are associated with functions of opera-
tional model. therefore, they will receive arguments.
The expressions (hti − ; ti ) can have different forms, for wich, to factor consider
the following cases:
i) H; ht− ; t(a) factored as: H; ht− ; t(a)
ii) H; ht1 − ; t1 × ht2 − ; t2 (a, b) is factored as: H; ht1 − × ht2 − ; t1 ×, t2 (a,
b)
iii) H; ht1 − ; t1 + ht2 − ; t2 (a) factored as: H; ht1 − + ht2 − ; t1 (a) + t2 (a)
iv) H; κ ∗ ht1 − ; t1 (a) factored as: H; ht1 − ; κ ∗ t1 (a) , where κ ∈ C
v) If t, t0 are superpositions(or tuples then
0
H; ht− ; t(b) if a = 1
ht− ; t|ht − ; t (a, b) =
0
H; ht0 − ; t0 (b)
if a = 0
else
ht− ; t|ht0 − ; t0 (a, b) = H; (ht− |ht0 − ); (t|t0 )(a, b) , and the conditional
definition is applied.
The factorization is started from right to left, namely:
ht1 − ; t1 ◦ ht2 − ; t2 ◦ · · · ◦ htn − ; tn = htn − ; ht1 − ; t1 ◦ ht2 − ; t2 ◦ · · · ◦ tn
= htn − ; · · · ; ht2 − ; ht1 − ; t1 ◦ t2 ◦ · · · ◦ tn
= htn − ; · · · ; ht2 − ; ht1 − ; t1 ◦ t2 ◦ · · · ◦ tn
| {z } | {z }
History track (H) Computational Register
If there exists a conditional (t|t0 ), where t and t0 , are superpositions; will
be incorporated into the history track once the conditional has been evaluated.
With the above we have the computational state, and we continue with the rules
developed for the reversibility.
4.2 Reversibility
The reversibility can be executed starting from the fact that if we have a state
and execute all the functions of the computational register we will obtain a final
value q, i.e., htn − ; · · · ; ht2 − ; ht1 − ; t1 ◦t2 ◦· · ·◦tn (a) = · · · = htn − ; · · · ; ht2 − ;
ht1 − ; q. Let a computational state (result of derivations) with the form:
ht1 − ; · · · ; ht2 − ; ht1 − ; q,
where q it’s an irreducible term (for the operational model). Given hti − a history,
apply as argument q to the previous immediate history, replacing by the symbol
− , and applying the respective function, for example: hti − ; a = hti (a). Reversibil-
ity can be applied to the value q, from the history stack (ht1 − ; ht2 − ; · · · ; htn − ),
considering the following cases:
33
i) hti − ; q = hti (q)
ii) (hti − × htj − ) (q1 , q2 ) = (hti q1 , htj q2 )
iii) (hti − + htj − ) α(q1 + q2 ) = (hti q1 , htj q2 ), where α ∈ C.
iv) ht1 − ; κ ∗ q = ht1 (q)
where κ, α ∈ C are discarded.
With the previous proposals, we show an example with classic and quantum
data, this is the Hadamard gate.
5 Example: Hadamard gate
had 1 = if◦ 1 then (−1) ∗ true + f alse else true + f alse
J• ⊗ • ` had 1 : Q2 K = (g ∗ |h∗ ) ◦ (f ∗ × id∗−1
Q ∗ −1
− ; id ) ◦ ((δΓ,∆ ) ; δΓ,∆ )
g∗
z }| {
1
∗−1 ∗ ∗−1 ∗
= √ ((−1) ∗ const 1− ; const 1 + const 0− ; const 0 ) |
2
h∗
z }| {
1 ∗−1 ∗ ∗−1 ∗
√ (const 1− ; const 1 + const 0− ; const 0 )
2
∗−1
◦ const 1∗−1 ∗
− ; const 1 × id− ; id
∗
◦ id+−1
− ; id+
H
z }| {
= (id+−1 ); (const 1∗−1 × id∗−1 ∗ ∗
◦ (const 1∗ × id∗ ) ◦ id+ (1)
− − − ); g |h
= H; g ∗ |h∗ ◦ (const 1∗ × id∗ )(r 1 0, r 0 1)
= H; g ∗ |h∗ ◦ (const 1∗ (r 1 0), id∗ (r 0 1))
= H; g ∗ |h∗ (r 0 1, r 0 1) = H; g ∗ (r 0 1)
1
= H; √ ((−1) ∗ const 1∗−1 − ; const 1∗
+ const 0 ∗−1
− ; const 0 ∗
) (r 0 1)
2
1
= H; (const 1∗−1− + const 0∗−1 ∗
− ); √ ((−1) ∗ const 1 + const 0 ) (r 0 1)
∗
2
1
= H; √ (−1) ∗ const 1 (r 0 1) + const 0∗ (r 0 1)
∗
2
1
= H; √ (−1) ∗ (r 0 1) + (r 0 0)
2
√1 (−1) ∗ (0.0) + (1.0) . Explicitly H is:
If evaluate r functions we get: 2
∗−1 ∗−1
(id+−1
− ); (const 1 − × id− ); (const 1∗−1
− + const 0∗−1
− );
34
Applying reversibility we have:
(id+−1
− ); (const 1∗−1
− × id∗−1 ∗−1
− ); (const 1− + const 0∗−1
− )(r 0 1 + r 0 0)
= (id+−1
− ); (const1∗−1
− × id∗−1 ∗−1
− ); (const 1− + const 0∗−1
− )(r 0 1 + r 0 0)
= (id+−1
− ); (const 1∗−1
− × id∗−1
− ); (const 1
∗−1
(r 0 1), const 0∗−1 (r 0 0))
= (id+−1
− ); (const 1∗−1
− × id∗−1
− )(r 1 0, r 0 0)
= (id+−1
− ); (const 1∗−1 (r 1 0), id∗−1
− (r 0 0)) = id
+−1
(r 0 1, r 0 0) = 1
Through this example, is observed how the reversibility is executed and that
it is successfully achieved, that is, return to the initial argument, in this case, to
value 1. We proceed with the conclusions and future work.
6 Conclusions and Further Work
The construction to add the history track was partially worked, the classical el-
ements of the syntax and its respective operational model were considered first,
immediately, the inverse functions were defined and added to the model, where
the inverse operations are stored in the history stack. This is extrapolated to the
complete syntax incorporating terms with probability amplitude and superposi-
tions, allowing a model also with inverse functions.
If you have a value (resulting from a program) and this is applied to the
respective history stack, then the inverse functions are applied, allowing you to
return to the initial value of the program, this results in reversibility.
As a possible future work, a simple implementation of programs can be made
than execute reversibility in a more direct and natural way.
References
1. Altenkirch, T., Grattage, J.: A functional quantum programming language. In:
20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05). pp. 249
– 258 (2005). 10.1109/LICS.2005.1
2. Lampis, M., Ginis, K.G., Papakyriakou, M.A., Papaspyrou, N.S.: Quantum data
and control made easier. Electron. Notes Theor. Comput. Sci. 210, 85–105 (Jul
2008). 10.1016/j.entcs.2008.04.020
3. Tonder, A.v.: A lambda calculus for quantum computation. SIAM J. Comput.
33(5), 1109–1135 (2004). 10.1137/S0097539703432165
4. Ömer, B.: A procedural formalism for quantum computing. AIP Conference Pro-
ceedings 627(1), 276 (2002). 10.1063/1.1503695
5. Mlnar’k, H.: Quantum Programming Language LanQ. phdthesis, Faculty of Infor-
matics (September 2007)
6. Sanders, J.W., Zuliani, P.: Quantum programming. In: Backhouse, R., Oliveira,
J.N. (eds.) Mathematics of Program Construction. pp. 80–99. Springer Berlin Hei-
delberg, Berlin, Heidelberg (2000)
7. Gay, S.J.: Quantum programming languages: Survey and bibliography. Mathemat-
ical. Structures in Comp. Sci. 16(4), 581–600 (2006). 10.1017/S0960129506005378
35
8. Jorrand, P., Lalire, M.: From Quantum Physics to Programming Languages: A
Process Algebraic Approach, pp. 1–16. Springer Berlin Heidelberg, Berlin, Heidel-
berg (2005). 10.1007/11527800 1
9. Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings
of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Program-
ming Languages. pp. 145–157. POPL ’05, ACM, New York, NY, USA (2005).
10.1145/1040305.1040318
10. Gay, S.J., Nagarajan, R.: Communicating quantum processes. SIGPLAN Not.
40(1), 145–157 (2005). 10.1145/1047659.1040318
11. Miszczak, J.A.: High-level structures for quantum computing. Synthesis Lectures
on Quantum Computing 4 (05 2012). 10.2200/S00422ED1V01Y201205QMC006
12. Selinger, P.: A brief survey of quantum programming languages. In: In Proceed-
ings of the 7th International Symposium on Functional and Logic Programming.
Springer (2004). 10.1007/978-3-540-24754-8 1
13. Selinger, P.: Towards a quantum programming language. In: Mathematical Struc-
tures in Computer Science. pp. 527–586 (2004). 10.1017/S0960129504004256
14. Dı́az-Caro, A., Arrighi, P., Gadella, M., Grattage, J.: Measurements and confluence
in quantum lambda calculi with explicit qubits. Electronic Notes in Theoretical
Computer Science 270(1), 59 – 74 (2011). 10.1016/j.entcs.2011.01.006, proceedings
of the Joint 5th International Workshop on Quantum Physics and Logic and 4th
Workshop on Developments in Computational Models (QPL/DCM 2008)
15. Abramsky, S.: Computational interpretations of linear logic. Theoretical Computer
Science 111(1), 3 – 57 (1993). 10.1016/0304-3975(93)90181-R
16. Abramsky, S.: A structural approach to reversible computation. Theor. Comput.
Sci. 347(3), 441–464 (2005). 10.1016/j.tcs.2005.07.002
17. Altenkirch, T., Grattage, J., Vizzotto, J.K., Sabry, A.: An algebra of pure quantum
programming. Electronic Notes in Theoretical Computer Science 170, 23 – 47
(2007). 10.1016/j.entcs.2006.12.010, proceedings of the 3rd International Workshop
on Quantum Programming Languages (QPL 2005)
18. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum In-
formation: 10th Anniversary Edition. Cambridge University Press (2010).
10.1017/CBO9780511976667
19. McMahon, D.: Quantum Computing Explained
20. Grattage, J.J.: A functional quantum programming language (2006)
21. Landauer, R.: Irreversibility and heat generation in the computing pro-
cess. IBM Journal of Research and Development 5(3), 183–191 (July 1961).
10.1147/rd.53.0183
22. Reversible computation in term rewriting. Journal of Logical and Algebraic Meth-
ods in Programming 94, 128 – 149 (2018). 10.1016/j.jlamp.2017.10.003
23. Abramsky, S.: A structural approach to reversible computation. Theoretical Com-
puter Science 347(3), 441 – 464 (2005). 10.1016/j.tcs.2005.07.002
24. Bennett, C.H.: Logical reversibility of computation. IBM J. Res. Dev. 17(6), 525–
532 (1973). 10.1147/rd.176.0525
25. Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the
Fourth Annual Symposium on Logic in Computer Science. pp. 14–23. IEEE Press
(1989)
26. Awodey, S.: Category Theory. Oxford Logic Guides (2006)
36
Appendix 1
J• ` () : Q1 K = const 0
J• ` f alse : Q2 K = const 0
J• ` true : Q2 K = const 1
Jx : σ ` x : σ K = id∗
JΓ ⊗ ∆ ` let x = t in u : σ K = g ◦ (f × id) ◦ δΓ,∆
where:
f = JΓ ` t : σ K
g = J∆, x : σ ` u : τ K
JΓ ⊗ ∆ ` (t,u) : σ ⊗ τ K = (f × g) ◦ δΓ,∆
where:
f = JΓ ` t : σ K
g = J∆ ` u : τ K
JΓ ⊗ ∆ ` let (x,y) = t in u : ρ K = g ◦ (f × id) ◦ δΓ,∆
where:
f = JΓ ` t : σ ⊗ σ K
g = J∆, x : σ, y : τ ` u : ρ K
◦
JΓ ⊗ ∆ ` if c then t else u : σ K = (g|h) ◦ (f × id) ◦ δΓ,∆
where:
f = JΓ ` c : Q2 K
g = J∆ ` t : σ K
h = J∆ ` u : σ K
JΓ ` t : σ K = f × id∗
where:
f = JΓ , x : Q1 ` t : σ K
Table 6: Meaning of classical derivations (Source: [17], p. 31).
37
Appendix 2. Auxiliary functions
Let a, a0 , b ∈ S, S = {0, 1} (Source: [17], p. 30).
id : S → V S, defined by: id(a) = a
id+ : S → JQ1 K × S, defined by: id+ (a) = (0, a)
id+ : JQ1 K × S → S, defined by: id+ (0, a) = a
const a : JQ1 K → S, defined by: const a(0) = a
δ : S → (S, S), defined by: δ(a) = (a, a)
swap : S × T → T × S, defined by: swap(a, b) = (b, a)
Let a functions f : S1 → T1 and g : S2 → T2 , therefore
f × g : S1 × S2 → T1 × T2 , is defined by: f × g (a, b) = (f a, g b)
δΓ,∆ : JΓ ⊗ ∆ K → JΓ K × J∆ K defined by induction as follows:
δΓ 0 ,∆0 × δ
if Γ = Γ 0 , x : σ y ∆ = ∆0 , x : σ
δΓ,∆ = δΓ 0 ,∆ × id if Γ = Γ 0 , x : σ y x ∈
/ dom(∆)
+
id if Γ = •
For any two functions f, g ∈ S → T, (f |g) ∈ S → T , defined as:
(f |g) (1, a) = (f a)
(f |g) (0, a) = (g a)
38
Appendix 3
Example 1. true + false
Q 1
J• ` true + f alse : Q2 K = √ (f + g)
2
where:
f = J• ` true : Q2 K = const 1−1
Q
− ; const 1
g = J• ` f alse : Q2 K = const 0−1
Q
− ; const 0
therefore:
1
J• ` true + f alse : Q2 K = √ const 1−1
Q
− ; const 1 (0)
2
+ const 0−1
− ; const 0 (0)
= const 1−1 −1
− + const 0− ;
1
√ const 1 (0) + const 0 (0)
2
1
= const 1− + const 0−1
−1
− ; √ r 0 1+r 0 0
2
is equivalent to
−1 1
= const 1−1
− + const 0− ; √ 0.0 + 1.0
2
Applying reversibility:
−1 1
const 1−1 r 0 1 + r 0 0 =const 1−1
− + const 0− ; √ − (r 0 1)
2
+ const 0−1
− (r 0 0)
=(0 + 0)
39