We developed an operational model that incorporates a history track for the quantum programming language QML, considering 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 rst with classical data and extrapolated to quantum data.
Introduction
There are several quantum programming languages, based on the imperative,
functional or other paradigms. Only a few are described below: QML [
Some languages based on imperative paradigm are: QCL [
We will focus on QML developed by Grattage y Altenkirch, is a rst order
language and has nite data-types, the semantics of QML assigns to every
welltyped 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 [
Several authors have considered this language, is the case of D az-Caro,
Arrighi, Gadella y Grattage who give an idea to implement a history track and
quantum measurements [14{16]. Altenkirch, Grattage, Vizzotto and Sabry not
de ne operational semantics in terms of circuits and develop a sound and
complete equational theory omitting measurements, they work QML subdividing
the classical and quantum part of the language [
Quantum languages must consider the implicit property of reversibility, if the operations are de ned 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
operational model, the track will store the operations performed in a program. With
this, reversibility can be explicitly executed. The above is added to QML
language de ned by Altenkirch, Grattage, Vizzotto and Sabry [
Preliminaries
There are four principles or postulates that de ne the behavior of quantum
computing. The pure states are unitary vectors, which store in memory the
information used. Evolution, this indicates how change from one state to another,
for which unit matrices are applied, they have implicit instructions that the
computer 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,
implying a collapse of the system. Composite systems, will be in charge of de ning
states conformed by states of di erent systems and how they interact among
them [
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
semantics [
(Variables) x; y; : : : 2 V ars (Terms) t; u ::= x j () j (t; u) (Prob. amplitudes) ; ; : : : 2 C j let p = t in uj f alse (Patterns) p; q ::= x j (x; y) j truej 0 j t j t + u j 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 de ne 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: = Q1jQ2j , where Q1 is the type (), which carry no information and Q2 corresponds to qubits (0 and 1). The types are nite and non-recursive, and the only types that can be represented are those in the collection of qubits.
Typing contexts ( ; ) are given by: ; x : = j ; x : , where stands for the empty context. We context correspond to functions from a nite 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 2= dom
=
Interpret a judgement ` t : as a function is J ` t : K 2 J K ! J K, where, given a typing contexts, it returns a type of the collection of qubits.
To de ne 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 :
` let x = t in u :
let
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 [
Our proposal will be described below, which is based on modifying the operational 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 modi ed 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 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
J
J
` let x = t in u : J
Rules like J ` f alse : Q2 KQ = (const 0) 1; 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.
Considering the auxiliary functions (Appendix 2) de ned in the operational
model (with quantum operations), the authors extend the functions using a
Kleisli Triple, where each derivation returns a complex vector [
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 [
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 de ne 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 f (a) = b. Then, the function r has type J K ! J KQ, e.g. r : J K ! J K ! C (by de nition of J KQ), de ned as r(a f (a)) = , 2 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-byname evaluation mechanism, so its argument will not be evaluated until needed.
The following functions are part of our contribution. For each auxiliary functions f we consider r to de ne the inverse f 1, the lift f (associated with a Kleisli Triple) and its inverse f 1. Consider S 2 JQ2 K, the modi ed functions are:
id+ 1(r a0 b; r a0 a) = { id : S ! (S ! S ! C), this function returns the argument it receives, and is de ned as: id(a) = (r a a). id : (S ! V S) ! (S ! S ! C) de ned as: id (r a0 a) = (r a0 a) id 1 : (S ! V S) ! S de ned as: id 1(r a0 a) = a id 1 : (S ! V S) ! (S ! S ! C) de ned 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 de ned as: id+(a) = (r a 0; r 0 a) id+ : (S ! V S) ! (S ! JQ1 K ! C) (S ! S ! C) de ned as: id+ (r a0 a) = (r a 0; r 0 a), and the other options are de ned as: (a; if b=0
b; if b=1 id+ 1(r a0 0; r a0 a) = (r a0 a) { id+ : (JQ1 K S) ! (S ! S ! C) de ned as: id+(0; a) = (r a a) id+ : (S ! V JQ1 K) (S ! V S) ! (S ! S ! C) de ned 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(r a0 a) = (0; a) id+ 1(r a0 a) = (r a0 a; r 0 a) const 0 1(r a0 a) = 0, and const 1 1(r a0 a) = const 0 1(r a0 a) = (r a 0), and const 1 1(r a0 a) = (1; if a=0 0; if a=1 (r a 1; if a=0 r a 0; if a=1 { const a : JQ1 K ! (JQ1 K ! S ! C) is de ned as: const a(0) = (r 0 a) const a : (S ! V S) ! (JQ1 K ! S ! C) de ned as: const a (r a0 a00) = (r 0 a), and its inverse as: {
: S ! ((S ! S ! C) (S ! S ! C)) double the argument received, de ned as: (a) = (r a a; r a a)
: (S ! V S) ! ((S ! S ! C) (S ! S ! C)), de ned 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, de ned as: swap(a; b) = (r a b; r b a) swap : ((S ! V S) (S ! V T )) ! ((S ! T ! C)) (T ! S ! C)) de ned as: swap (r a0a; 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 de ned as: f g (a; b) = (f a; g b) f g : (S1 ! V S10) (S2 ! V S20) ! (S10 ! T1 ! C) (S20 ! T2 ! C), de ned 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) de ned 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 de ned 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:
>8 0; 0 if = 0; x : y = 0; x : ( ; ) = < 0; id if = 0; x : y x 2= dom( )
>:id+ if = { (f jg) : (JQ2 K S) ! (S ! T ! C), is associated with if conditional, de ned as: (f jg) (1; a) = (f a) and (f jg) (0; a) = (g a). (f 1jg 1) : (S ! V T ) ! ((S ! S ! C) (S ! S ! C)), de ned as: 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, however, we still need de ne the modi ed rules for terms with probability amplitudes and superpositions. The new rules to form well-typed judgements and for deriving terms (quantum and classic) are in Table 3 and Table 4, respectively. Based on these de nitions, we propose the modi cation that also allows storing operations in the history stack. prob sup ` t; u : `
` t : 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 j 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, for example: J ` if 1 then ( 1) true + f alse else true + f alse : Q2 KQ = (g jh ) (f id 1; id ) (( ; ) 1; ; ): At this point, the functions are mixed with their inverses, which must be separated, how to achieve this we will de ne immediately.
J `
t : KQ = ( ) f J ` t + u : KQ = p12 f + g where 8a 2 J K:v a = 0:0 where 8b 2 J K f = J ` t : KQ where 8a 2 J K f = J ` t : K g = J ` u : K
Q Q To apply reversibility, several points are important: A concept called a history stack and auxiliary functions de ned 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: De nition 2 (Computational state). The computational state is a sequence of the form: htn ; tn where htn ; ; ht2 ; ht1 , is called the history track and t1 the computational register. t2; tn, Regarding hti ; ti, the part hti represents and stores the inverse operation that executes ti.
De nition 3. H, denotes the (possibly empty) history track.
To arrive at the computational state, the terms must be factored, considering di erent cases. 4.1
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 operational model. therefore, they will receive arguments.
The expressions (hti ; ti) can have di erent forms, for wich, to factor consider the following cases:
ht ; tjht0 ; t0 (a; b) = 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 2 C v) If t; t0 are superpositions or tuples then (H; ht ; t(b)
H; ht0 ; t0(b) if a = 1 if a = 0 else ht ; tjht0 ; t0 (a; b) = H; (ht jht0 ); (tjt0)(a; b) , and the conditional de nition is applied.
The factorization is started from right to left, namely: ht1 ; t1 ht2 ; t2 htn ; tn = htn ; ht1 ; t1 ht2 ; t2
tn = htn ; = htn ; |
If there exists a conditional (tjt0), 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. 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 nal 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). Reversibility can be applied to the value q, from the history stack (ht1 ; ht2 ; ; htn ), considering the following cases: i) hti ; q = hti (q) ii) (hti htj ) (q1; q2) = (hti q1; htj q2) iii) (hti + htj ) (q1 + q2) = (hti q1; htj q2), where iv) ht1 ; q = ht1 (q) where ; 2 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 KQ = (g jh ) (f id 1; id ) (( ; ) 1; ; ) = z1 p2 (( 1) const 1 g }| 1; const 1 + const 0
{ 1; const 0 ) j If evaluate r functions we get: p12 ( 1) (0:0) + (1:0) . Explicitly H is: (id+ 1); (const 1 1 id 1); (const 1 1 + const 0 1);
Applying reversibility we have: (id+ 1); (const 1 1 id 1); (const 1 1 + const 0 1)(r 0 1 + r 0 0) = (id+ 1); (const1 = (id+ 1); (const 1 = (id+ 1); (const 1 = (id+ 1); (const 1 1 1 1 id id id 1); (const 1 1); (const 1 1)(r 1 0; r 0 0) 1 + const 0
1)(r 0 1 + r 0 0) 1(r 0 1); const 0 1(r 0 0)) 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 elements of the syntax and its respective operational model were considered rst, immediately, the inverse functions were de ned 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 superpositions, 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.
J ` () : Q1 K = const 0 J ` false : Q2 K = const 0 J ` true : Q2 K = const 1
Jx : ` x : K = id ` let x = t in u : K = g (f id) ; where: J
Let a; a0; b 2 S, S = f0; 1g (Source: [
id : S ! V S, de ned by: id(a) = a id+ : S ! JQ1 K S, de ned by: id+(a) = (0; a) id+ : JQ1 K S ! S, de ned by: id+(0; a) = a const a : JQ1 K ! S, de ned by: const a(0) = a
: S ! (S; S), de ned by: (a) = (a; a) swap : S T ! T S, de ned by: swap(a; b) = (b; a) Let a functions f : S1 ! T1 and g : S2 ! T2, therefore f g : S1 S2 ! T1 T2, is de ned by: f g (a; b) = (f a; g b) ; : J K ! J K J K de ned by induction as follows: 8> 0; 0 if = 0; x : y = 0; x : ; = < 0; id if = 0; x : y x 2= dom( ) >:id+ if = For any two functions f; g 2 S ! T; (f jg) 2 S ! T , de ned as: (f jg) (1; a) = (f a) (f jg) (0; a) = (g a) Example 1. true + false therefore:
J ` true + f alse : Q2 KQ = p12 (f + g) f = J ` true : Q2 KQ = const 1 1; const 1 g = J ` f alse : Q2 KQ = const 0 1; const 0 J ` true + f alse : Q2 KQ = p12 const 1 1; const 1 (0) =(0 + 0)