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