# Quantum Calculi--From Theory to Language Design
## 4 Foundational Quantum Programming Languages
### qPCF and IQu
#### 4.5.1 qPCF  
The language qPCF is based on a version of the QRAM model where measurements are all performed at the end of the computation. qPCF is a simple extension of [PERSON]'s PCF: essentially, it extends PCF with a new kind of classical data, quantum circuits, that can be, thanks to the type system, treated as classical objects (i.e., freely duplicated). In qPCF linear logic-based typing has been completely avoided, in favor of the use of a simple version of _dependency_, that permits to soundly encode quantum circuits families directly controlling arities of subcircuits, avoiding illegal erasing or duplication of wires. qPCF types includes: the types of quantum circuits \(\mathsf{circ}(E)\) (where \(E\) that morally represents a circuit dimension), the type of _indexes_ (i.e., strongly normalizing expressions) \(\mathsf{Idx}\) and the (standard) quantification over types \(\Pi\!x.\tau\).  
The syntax of qPCF allows us to easily manipulate circuits through operations such as sequentialization and parallelization of an arbitrary number of sub-circuits. For example, consider the program \(\mathsf{M}_{\mathsf{seq}}=\lambda\mathsf{u}^{\mathsf{circ}(\underline{k})} \lambda x^{\mathsf{Nat}},\gamma\mathsf{Wux}:\mathsf{circ}(\underline{k}) \rightarrow\mathsf{Nat}\rightarrow\mathsf{circ}(\underline{k}):\sigma\rightarrow\sigma\) where \(Y\) is the recursion operation, \(\mathsf{W}=\lambda\mathsf{u}^{\sigma}.\lambda\mathsf{u}^{\mathsf{circ}( \underline{k})}.\lambda\mathsf{y}^{\mathsf{Nat}}.\mathtt{if}\ y\ (\mathsf{u})\ (\$\,(\mathsf{u})\,(\mathsf{w}\,(\mathtt{predy})))\) and \(\sigma=\mathsf{circ}(\underline{k})\rightarrow\mathsf{Nat}\rightarrow\mathsf{ circ}(\underline{k})\). Given a term representing a circuit (of ariety \(\underline{k}\)) \(\mathsf{C}:\mathsf{circ}(\underline{k})\), it is easy to observe that \(\mathsf{M}_{\mathsf{seq}}\) applied to \(\mathsf{C}\) and \(\underline{n}\) concatenates \(n+1\) copies of \(\mathsf{C}\).  
The parallel composition of quantum circuit can be achieved by using the operator \(\mathtt{iter}\) (that has type \(\Pi\!x^{\mathsf{Idx}}.\mathsf{circ}(\underline{c}_{0})\rightarrow\mathsf{circ }(\underline{c}_{1})\rightarrow\mathsf{circ}(\underline{c}_{0}+((1+E_{1})* \mathsf{x}))\)).  
Consider the program \(\mathsf{M}_{\mathsf{par}}=\lambda x^{\mathsf{Idx}}.\lambda\mathsf{u}^{ \mathsf{circ}(\underline{k})}\lambda\mathsf{u}^{\mathsf{circ}(\underline{k})}. \mathtt{iter}\,\mathtt{x}\,\mathtt{u}\,\mathtt{w}:\Pi\!x^{\mathsf{Idx}}. \mathsf{circ}(\underline{k})\rightarrow\mathsf{circ}(\underline{n}) \rightarrow\mathsf{circ}(\underline{k}+(\mathsf{x}*(\underline{n}+1)))\). When applied to a numeral \(\underline{n}\) and two unitary gates \(\mathsf{U}_{1}:\mathsf{circ}(\underline{k})\) and \(\mathsf{U}_{2}:\mathsf{circ}(\underline{n})\), \(\mathsf{M}_{\mathsf{par}}\) generates a circuit built upon a copy of gate \(\overline{\mathsf{U}}_{1}\) in parallel with \(n\) copies of gate \(\overline{\mathsf{U}}_{2}\). Notice that the term is driven by an argument of type \(\mathsf{Idx}\), to ensure that iteration is strong normalizing and, consequently, that the arity of the generated circuit is always a numeral.  
qPCF makes especially convenient the programming of quantum algorithms in _deferred form_, where measurements are all postponed at the end of the computation. qPCF quantum states are not stored. This is possible since the interaction with the quantum co-processor is neatly decoupled using the operator dmeas. It offloads a quantum circuit to a co-processor for the evaluation which is immediately followed by a (von Neumann) Total Measurement. This means that partial measures are forbidden. Thanks to the deferred measurement principle [9], this restriction does not represent a theoretical limitation. Nevertheless, general measurement is an useful programming tool and we model it in the language lQu described in Section 4.5.2.