# Quantum Calculi--From Theory to Language Design
## 2 On Quantum Language Design: Main Features
### On the Linearity of Quantum Data  
It is well-known that quantum data are not duplicable (_no cloning property_) [33]. Therefore, the design of the type system for a quantum programming language necessarily has to address the problem of data linearity. In this section, we specifically take a look at this aspect through a quick overview of some languages in literature. A more general discussion about the state of art of quantum programming is in Section 3. Following [PERSON]'s suggestion in his seminal work about quantum programming theory [16], higher-order language can be equipped with some kind of linear type system along the lines of [PERSON]'s linear logic (LL), in order to account for the non-duplicability of quantum data [3; 8; 34; 35; 36; 37; 38]. Figure 1: Direct and indirect equivalence between quantum computational models. Several versions of LL have been used in literature.For example, [PERSON] and [PERSON]'s quantum lambda calculus [3] (on which the programming language Quipper is partially inspired) is based on the multiplicative fragment of _affine_ LL, that is, contraction structural rule is not allowed. This choice is justified by the no-cloning property of quantum states and, logically, signifies that one can not duplicate resources but can discard them. Instead, [PERSON] and [PERSON] [4; 39] chose a different approach to the (central) problem of copy and discard quantum data. In their language QML (that can not be completely considered QRAM based but is relevant for this discussion) is possible to write expressions like let \(x=(\mathsf{false}+\mathsf{true})\mathsf{in}\langle x,x\rangle\) which (apparently) violates no-cloning properties, since the variable x is duplicate in the let expression (notice also that a limited superposition \"+\" between ground value is admitted). The previous expression does not clone quantum data (this is guaranteed by the formal semantics the authors provide): it shares a copy of the quantum datum among different references. This is captured through a type system based on multiplicative _strict_ LL, that is, linear logic with contraction and without weakening. We spend some further words about these calculi in Section3. In [PERSON] et al. [34] the untyped quantum lambda calculus Q is introduced and studied. The set of well-formation rules (w.f.r.) is based on [PERSON]'s formulation of LL and the! (\"bang\") operator allows distinguishing between duplicable (classical) and non-duplicable (quantum) resources. Classical variables and quantum variables (variables \"pointing to\" qubits) belong to different syntactical classes. These choices statically respect the linearity of quantum data, that can neither be duplicated or erased (duplication and erasing of classical data are allowed). Moreover, the _surface reduction_ is adopted, to avoid dynamic duplication of linear resources: informally, a term of the form! (\(M\)) can not contain quantum variables (this is guaranteed by w.f.r. ) and can not be reduced. Lambda calculus' \(\beta\)-reduction is modified accordingly (in particular, \(\beta\)-reduction is split into three different rules). A small example clarifies the design of the language and the operational behavior of programs. **Example 1** (How to violate quantum linearity). : _In Q computational steps are defined between configurations that is, triples of the form [Q,QV,M] where \(Q\) is \"the quantum memory\" (it keeps information about the mathematical state we are computing and qubit names), QV is the set of qubit names contained in the lambda term \(M\). Q inherits configurations from Reference [3] (and this tradition can be retraced in Idealized ALGOL programming style [40])._  
_Let us consider the following well-formed expression, where 1 represent a empty quantum state (a memory containing 0 qubits), the subterm new \((1)\) create a qubit and its name and cnot is the controlled not operator [9]: \([1,\emptyset,(\lambda!x.cnot\langle x,x\rangle)! (\mathsf{new}\ (1))]\)._  
_Observe that the sub-term!