# On Hofstadter butterfly spectrum: Chern-Simons theory, subband gap mapping,
IQHE and FQHE labelling

F. A. Buot1,2,3, G. Maglasang1,3, A. R. Elnar1,3 and C. M. Galon1,3
1CTCMP, Cebu Normal University, Cebu City 6000
Philippines,
2C&LB Research Institute, Carmen, Cebu 6005
Philippines,
3LCFMNN, University of San Carlos, Cebu City 6000,
Philippines

###### Abstract

The magnetic field affects the Bloch band structure in a couple of ways. First
it breaks the Bloch band into magnetic subbands or the Landau levels are
broadened into magnetic Bloch bands. The resulting group of subbands in the
central portion of the energy scale is associated with the integer quantum
Hall effect (IQHE). Then at high fields it changes the integrated density of
states of the remaining lowest and topmost subband, respectively, which can be
associated with fractional quantum Hall effect (FQHE).

Here, we employ the Maxwell Chern-Simons gauge theory to formulate the
subband-gap mapping algorithm and to construct the butterfly profile of the
Hofstadter spectrum. The two regions in the spectrum responsible for the IQHE
are identified. At very high magnetic fields the highest and lowest subband
are affected by magnetic-field induced restructuring of the integrated density
of states in each subband, respectively. The resulting transformation of each
of the two subband is responsible for the FQHE. Thus, in the central regions
of the energy scale, the principal group of subbands defined by the gap
mapping is responsible for the IQHE. The fine structure of the topmost and
lowest subband, which convey an iterative nature of the magnetic spectrum is a
result of a hierarchical scaling and restructuring by the magnetic fields on
the integrated density of states in each respective subband and is responsible
for the FQHE.

##  1 INTRODUCTION

When electrons are subjected to both a magnetic field and a periodic
electrostatic potential, two-dimensional systems of electrons exhibit a
complex energy spectrum, known as the Hofstadter’s butterfly [1]. This complex
spectrum results from an incommensurate/commensurate interplay between two
characteristic length scales, defined by the magnetic lattice with lattice
constant given by the magnetic length, $l_{B}$, and the periodic electrostatic
potential with lattice constant denoted by $a$. The magnetic length $l_{B}$
has the physical meaning of the smallest size of a circular orbit in a
magnetic field which is allowed by the uncertainty principle. Following
Hofstadter [1] and Wannier [2], we assume the square lattice model with the
two quantizing fields which perhaps yield the first fractal-like energy
spectrum discovered in physics.

The Schrödinger difference equation studied by Hofstadter[1] is known as the
Harper’s equation and can be written as

$u\left(m+1\right)+u\left(m-1\right)+2\cos\left(m\left(\frac{2\pi}{n}\right)-v\right)u\left(m\right)=\epsilon
u\left(m\right)$ (1)

where $m$ and $n$ are integers. We shall see that $n$ denotes the number of
magnetic subbands in what follows. Obviously, this equation has periodicity in
$\Phi=\frac{2\pi}{n}$. The energy spectrum obtained[1] is shown in Fig. 1

Figure 1: The Hofstadter butterfly energy spectrum obtained from computer
graphics rendering of computer numerical simulation results. One
characteristic feature is the wide band gap between topmost subband and lowest
subband. This wide subband gap appears to allow the field to restructure the
separated lower and upper central regions. Indeed, these two subbands are
restructured left and right of the middle of the abscissa. [Figure taken from
Hofstadter [1]]

To explain the above complex spectrum, Wannier [2], using counting arguments,
derived the so-called Diophantine equation to map out the energy subband gaps
of the spectrum. Here, we propose a simpler counting argument.

We employ the Maxwell Chern-Simons (CS) gauge theory[3, 4] to start the
counting arguments for subband gap mapping. First we set the basic variables
in analyzing the complex spectrum using CS gauge theory. Acknowledging the
symmetry and periodicity of the complex energy spectrum shown in Fig. 1, we
then draw the lines defining the bottom and top of the subbands, i.e, the
subband gaps. Our results is depicted in Fig. 2 and Fig. 3. These figures will
be discussed in more detail in what follows.

Figure 2: The lines in the figure map the center of the subband gaps. There
are essentially four regions of the spectrum, separated by the diagonal lines.
Remarkably, the diagonal lines represent wide subband gaps in Fig.1. The
central lower and upper regions of the spectrum is counted as the first lower
subband and the first upper subband, respectively. These two subbands clearly
show up in the middle of the spectrum. However, to the left and right of the
middle, these two subbands clearly undergo restructuring reminiscent of FQHE.
Therefore, we label these two, lower and upper central regions, of the
spectrum as the FQHE regions.

More of the lines are drawn in Fig.3 to show how the rays, defining different
values or numeration counting of the subbands emanates from the four corners
of the spectrum.

Figure 3: The figure shows how the lines emanates from the four corners of the
spectrum.

##  2 MAXWELL CHERN-SIMONS GAUGE THEORIES

We write the Chern-Simons Lagrangian density for $U\left(1\right)$ gauge
theory for $2$-dimensional system of manifold, $M$, as

$\mathcal{L}_{CS}=\gamma\varepsilon^{\mu\lambda\nu}A_{\mu}\partial_{\lambda}A_{\nu}-A_{\mu}J^{\mu}$
(2)

where $J^{\mu}=\left(\rho,\vec{J}\right)$, $\rho$ is the charge density and
$\vec{J}$ is the current density. Later, we will associate the parameter
$\gamma$ with our magnetic parameters. Equation (2) is often referred to as
the Maxwell Chern-Simons theory [4]. The equation of motion is obtained by
variation with respect to $A_{\mu}$

$\frac{\delta\mathcal{L}_{CS}}{\delta
A_{\mu}}=\gamma\varepsilon^{\lambda\nu}\partial_{\lambda}A_{\nu}-J^{\mu}=0$

This gives

$\gamma\int\limits_{M}\nabla\times\vec{A}\cdot
da=\int\limits_{M}J^{0}=\int\limits_{M}\rho$ (3)

$\int\limits_{M}\rho$ is equal to the integrated density of states of each
subband. In general, each subband have the same integrated density of states,
reflecting the same degeneracy for each Landau levels in free electrons case.

We now show that the total density of states is an integer, equal to the
magnetic flux divided by the quantum flux, which is equal to the degeneracy of
a Landau level in a magnetic field. We do this by first counting the number of
states in magnetic phase-space. This is given by [3]

$\displaystyle\mathcal{N}$ $\displaystyle=$
$\displaystyle\frac{1}{2\pi\hbar}\iint\vec{\nabla}\times\mathcal{\vec{K}}\cdot
d\vec{a}$ $\displaystyle=$
$\displaystyle\frac{1}{2\pi\hbar}\iint\vec{\nabla}\times\frac{e}{c}\vec{A}\cdot
d\vec{a}$

where $\mathcal{\vec{K}}=\vec{P}+$ $\frac{e}{c}\vec{A}+\vec{F}ct$, [5] $\Phi$
is the total magnetic flux, and $\vec{F}$ is the uniform electric field. We
will ignore the electric field from now on. Therefore, the Landau level
degeneracy, $\mathcal{N}$, is

$\displaystyle\mathcal{N}$ $\displaystyle=$
$\displaystyle\frac{1}{2\pi\hbar}\frac{e}{c}\iint\vec{B}\cdot d\vec{a}$
$\displaystyle=$ $\displaystyle\frac{\Phi}{2\pi\left(\frac{\hbar
c}{e}\right)}=\frac{\Phi}{\phi_{o}}$

where $\left(\frac{2\pi\hbar c}{e}\right)=\phi_{o}$ is the quantum flux. For a
square lattice, the number of quantum states in one Bloch band is equal to the
number of lattice sites, $N$. We denote by $n$ the number of magnetic subband
formed from a Bloch band under a uniform magnetic field. Since the magnetic
field does no work or does not impart energy on the systems, we can assume
that the number of quantum states in a Bloch band is conserved when uniform
magnetic field is applied. Thus for $n$ subbands, we have,

$\displaystyle N$ $\displaystyle=$
$\displaystyle\frac{n}{2\pi\hbar}\iint\vec{\nabla}\times\frac{e}{c}\vec{A}\cdot
d\vec{a}=n\frac{Na^{2}}{2\pi\left(l_{B}\right)^{2}}$ (4) $\displaystyle=$
$\displaystyle n\frac{\Phi}{\phi_{o}}$

In other words,

$n=\frac{N}{\left(\frac{\Phi}{\phi_{o}}\right)}=\frac{N}{\mathcal{N}}$

where the Landu level (LL) degeneracy $\mathcal{N}$ is,

$\mathcal{N}=\left(\frac{\Phi}{\phi_{o}}\right)$

Thus, we can measure the whole Bloch band in units of the LL degeneracy to
give us the number of subbands. We end up with

$n\frac{Na^{2}}{2\pi\left(l_{B}\right)^{2}}=N$ (5)

where $\mathcal{N=}$ $\frac{Na^{2}}{2\pi\left(l_{B}\right)^{2}}$ is the
degeneracy of each subband, $a$ is the lattice constant of a $2$-D square
lattice and $l_{B}=\sqrt{\frac{\hbar c}{eB}}$. Putting $N=1$ or cancelling on
both sides of Eq. (5), we have effectively normalized our Bloch band width to
unity.

We redefine our flux variable as

$\Phi=\frac{a^{2}}{2\pi\left(l_{B}\right)^{2}}=\frac{1}{n},\text{ \ \ \ \ \ \
}0\leq\frac{1}{n}\leq 1\text{, \ \ }$

Then we have

$n=\frac{1}{\frac{a^{2}}{2\pi\left(l_{B}\right)^{2}}}=\frac{1}{\Phi}$ (6)

In Eq. (6), the number of subbands is determined in units of $\Phi.$We see
that our normalized Bloch band is now measured in units of $\Phi$. We see that
when $\Phi=1$, the magnetic lattice coincides with the periodic atomic
potential lattice, and hence one expects that a single Bloch band is restored,
$E\left(k\right)$ is periodic in $k$ and in reduced Brillouin zone or one
band, $0\leq k\leq\frac{2\pi}{a}=\frac{2\pi}{l_{B}}$ with $l_{B}$ the magnetic
length, i.e., consisting of only one subband equal to the whole Bloch band
width.

##  3 SUBBAND GAP MAPPING

In tracing the first gap from the top of the Bloch band width, we reckon that
the bottom of the first gap from the topmost first subband must lie at values
of one value of $\Phi$ down in the Bloch energy-band scale. This will define
the diagonal line given by the linear equation,

$W_{bottop}=1-\Phi$

starting from $\left(0,1\right)$ coordinate, where $W$ is the ’$y$-coordinate’
representing the points in the normalized zero-field Bloch band width. Other
subbands bottom boundaries will be defined by lines given by the linear
equation,

$W_{t}=1-t\Phi\text{, \ \ \ \ \ \ }t\leq n\text{, }t\text{ integer}$

starting from $\left(0,1\right)$ coordinate, where $n$ is the total number of
subbands.

On the other hand, top boundary of the lowest subband must lie after a one
count of $\Phi$. This define another diagonal line of a linear equation,

$W_{toplow}=\Phi$

stating from $\left(0,0\right)$ coordinate. These diagonal lines are depicted
in Figs. 1 and 2. Other subbands top boundaries will be defined by lines given
by the linear equation,

$W_{l}=l\Phi\text{, \ \ \ \ }l\leq n\text{, \ \ \ }l\text{ integer}$

stating from $\left(0,0\right)$ coordinate.

###  3.1 Reflection symmetry at $\Phi=\frac{1}{2}$

The Hofstadter butterfly spectrum is somewhat reminiscent of a Cantor set,
which is an example of fractal string. In Fig.4, the horizontal line may
represent the zero-field Bloch band width. By tentatively identifying the
Hofstadter butterfly spectrum with the cantor set, we see that the limiting
lowest number of subbands is $n\geq 2$. Physically of course, the lower
integer value $n=1$ just coincide with the original zero-field Bloch band
width. Just like the Cantor set the gap between the limiting two subbands is
the largest in the set. This is also physically meaningful since at this
magnetic field strength the flux is large, or the degeneracy is large and
concentrated in the two subbands. Moreover, the cyclotron frequency spacing,
$\hbar\omega=\frac{eB}{mc}$, is also large and the two subbands are located
symmetrically near the middle of the zero-field Bloch band width. Since
$n=\infty$ and $n=1$ are physically identical, giving the whole zero-field
Bloch band width at this limiting cases, while also considering the
periodicity implied by Eq. (1) of period in$\frac{2\pi}{n}$
$\left(n=\infty\text{ and }n=1\right)$, we expect reflection symmetry of the
integer number of subbands at $\frac{2\pi}{n}=\pi$ or $n=2$. We can therefore
identify $n=1$ with $n=\infty$, and trace the gaps back towards $n=2$, with
decreasing integer $n$ as a complete mirror image of the left portion of the
flux corresponding to $n=2$. Thus, although reminiscent of Cantor set this
cyclic characteristic, among others, of the Hofstadter butterfly spectrum then
gives a diametrical contrast to the iterative construction of the Cantor set.

Figure 4: An example of the iterative construction of a Canto set. [Taken from
Wikipedia]

###  3.2 IQHE and FQHE Labelling

One most notable characteristics of the Hofstadter butterfly is the
reconstruction of the topmost subband as well as that of the lowest subband.
Although the left and right portion of the spectrum can be characterize as
regions of IQHE regions [6, 7, 8], the top and bottom regions of the spectrum
can be identified with the phenomenon of FQHE, since obviously this involves
the reconstruction of a single subband [3] at high magnetic fields . This
reconstruction is evidenced by the measurements [9, 10, 11] and Chern-Simons
theoretical explanation of the FQHE given by Buot [3]. These are all indicated
in Figs. (2) and (3).

##  4 CONCLUDING REMARKS

We need to say something about the profile of the top boundary of the topmost
subband, as well as the bottom boundary of the lowest subband. The bottom
profile of the lowest subband boundary must of the form of a convex curve with
endpoints connecting the point $\left(0,0\right)$ and $\left(1,0\right)$.
Similarly, the profile of the top boundary of the topmost subband must be a
concave curve with endpoints at $\left(0,1\right)$ and $\left(1,1\right)$.
This the main reason for the butterfly profile of the spectrum. This is
reminiscent of the Landau levels shifting the lowest energies to higher
energies, and the highest energy to lower energies in the presence of magnetic
flux, reflecting the increase of $\hbar\omega=\frac{eB}{mc}$ without changing
the total energies, since the magnetic field does not work on the system. This
aspect of the spectrum is indicated in Figs. (2) and (3).

###### Acknowledgement 1

The author is grateful for the ’Balik Scientist’ Visiting Professor grant of
the PCIEERD-DOST, Philippines, at Cebu Normal University, Cebu City,
Philippines.

## References

  * [1] D.R. Hofstadter, Energy levels and wave functions of Bloch electrons in rational and irrational magnetic fields, Phys. Rev. B14, 2239 (1976).
  * [2] G.H. Wannier, A Result Not Dependent on Rationality for Bloch Electrons in a Magnetic Field, Phys. Stat. Sol. (b) 88, 757 (1978).
  * [3] F.A Buot, G. Maglasang, A.R.F. Elnar,and C.M. Galon, On Fractional Quantum Hall Effect (FQHE): A Chern-Simons and nonequilibrium quantum transport Weyl transform approach, arXiv: 2107.13970 (2021).
  * [4] T. Van Mechelen and Z. Jacob, Viscous Maxwell-Chern-Simons theory for topological electromagnetic phases of matter, Phys. Rev. B 102, 155425 (2020).
  * [5] Felix A. Buot, On quantum Hall effect: Covariant derivatives, Wilson lines, gauge potentials, lattice Weyl transforms, and Chern numbers, arXiv:2106.16238 (2021).
  * [6] Felix A. Buot, Nonequilibrium superfield and lattice Weyl transform approach to quantum Hall effect, arXiv:2001.06993
  * [7] Felix A. Buot, Comments on the Weyl-Wigner calculus for lattice models,http://arxiv.org/abs/2103.10351
  * [8] Felix A. Buot, On the quantization of Hall effect in electrical conductivity: A nonequilibrium quantum superfield and lattice Weyl transform transport approach, AIP Conference Proceedings 2286, 030007 (2020). Quantum-Based Devices, Phys. Rev. B42, 9429-9456 (1990).
  * [9] Stormer, H. (1992). Two-dimensional electron correlation in high magnetic fields. Physica B: Condensed Matter, 177(14), 401-408.
  * [10] R. Willett, J. P. Eisenstein, H.L. Stormer, D. C. Tsui, A. C. Gossard and J. H. English, Observation of an Even-Denominator Quantum Number in the Fractional Quantum Hall Effect, Phys. Rev. Letts. 59, 1776 (1987).
  * [11] W. Pan, H. L. Stormer, D. C. Tsui, L. N. Pfeiffer, K.W. Baldwin, and K.W.West, Fractional Quantum Hall Effect of Composite Fermions, Phys. Rev. Letts. 90, 016801-1 (2003).


# A Quick Overview on the
Quantum Control Approach to the Lambda Calculus

Alejandro Díaz-Caro Founded by PICT-2019-1272, STIC-AmSud 21STIC10 Qapla’,
ECOS-Sud A17C03 QuCa, and PIP 11220200100368CO.  Departamento de Ciencia y
Tecnología Universidad Nacional de Quilmes Bernal, Buenos Aires, Argentina &
Instituto de Ciencias de la Computación CONICET–Universidad de Buenos Aires
Buenos Aires, Argentina<EMAIL_ADDRESS>
###### Abstract

In this short overview we start with the basics of quantum computing,
explaining the difference between the quantum and the classical control
paradigms. We give an overview of the quantum control line of research within
the lambda calculus, ranging from untyped calculi up to categorical and
realisability models. This is a summary of the last 10+ years of research in
this area, starting from Arrighi and Dowek’s seminal work until today.

##  1 Introduction

The study of quantum computing in the framework of the lambda calculus has
more than one motivation.

On the one hand, it is a tool to develop programming languages with firm
foundations. For example, from the study of Selinger and Valiron’s “Quantum
Lambda Calculus” (QLC) [48], Quipper [27] and QWIRE [38] arose. Both quantum
languages are quite advanced and complex, and while they are not fully
formalised, their cores are based on Knill’s QRAM model [29], which proposes
that a quantum computer is a device attached to a classical computer, and it
is the classical computer which instructs the quantum computer on what
operations to perform, over which qubits, etc. Selinger took this QRAM model
and formalised it in what is called the “Quantum Data, Classical Control”
approach [47]. This approach derived later into the QLC, and finally in
Quipper and QWIRE. Most quantum programming languages follow the same model,
including high level languages such as IBM’s Qiskit [2] or Microsoft’s
Q$\sharp$ [51]. Indeed, the Quantum Data, Classical Control approach is the
more practical approach.

On the other hand, typed lambda calculus provides a way to study logics,
through the Curry-Howard isomorphism (see, for example, [49]), which connects
logics with computation. The logic of quantum mechanics has been a challenging
subject since the beginnings of quantum mechanics. The seminal work of
Birkhoff and von Neumann [9], in which the authors tried to reconcile the
apparent inconsistency of classical logic with the quantum measurement, was
the birth of a long field of study among physicists. However, due to its
origins, there is no formal connection of this line with computing, and so, an
extension to the Curry-Howard isomorphism contemplating this logic is not easy
to envisage. The apparition of quantum computing as a way of understanding
quantum mechanics brought all the computer science machinery to the game. As a
consequence, a quantum logic formally connected to a quantum lambda calculus
seems reasonable. If Birkhoff and von Neumann’s quantum logic takes into
account the superposition of quantum states, and the uncertainty principle, a
quantum lambda calculus aimed at being the basis for a quantum logic must also
consider these non-classical aspects of the quantum theory. With this
objective in mind is that the first developments in this direction dropped the
idea of Quantum Data, Classical Control, embracing Quantum Control instead.

The quantum control approach has several origins. Most notably, quantum
automata exploit quantum control. The main difference with classical control
is that in classical control the control flow of a program is classical in the
sense that its description does not admit superpositions, measurement, or any
other kind of quantum properties. For example, we can describe a quantum
algorithm by describing its classical flow such as:

Prepare a quantum state $|{\psi}\rangle$

Apply the unitary transformation $U$ to $|{\psi}\rangle$

Apply the unitary transformation $V$ to the result of the previous step

Measure the obtained system

There is nothing quantum in the flow described here. This list of instructions
can be done by a classical computer. The quantum computer is the device which
will have to perform the operations prescribed by this classical machine. In
quantum control instead the flow is not classical. For example, in the
instruction

$\mathtt{If}\ c\ \mathtt{then}\ |{\psi}\rangle\ \mathtt{else}\
|{\varphi}\rangle$

if we admit $c$ to be a superposition such as
$\alpha.|{\mathsf{true}}\rangle+\beta.|{\mathsf{false}}\rangle$, this
instruction would become the superposition

$\alpha.\bigg{(}\mathtt{If}\ |{\mathsf{true}}\rangle\ \mathtt{then}\
|{\psi}\rangle\ \mathtt{else}\ |{\varphi}\rangle\bigg{)}\ +\
\beta.\bigg{(}\mathtt{If}\ |{\mathsf{false}}\rangle\ \mathtt{then}\
|{\psi}\rangle\ \mathtt{else}\ |{\varphi}\rangle\bigg{)}$

and so resulting in

$\alpha.|{\psi}\rangle+\beta.|{\varphi}\rangle$

The control flow is in superposition, and so it is not classic. Of course this
instruction is only valid if the final state
$\alpha.|{\psi}\rangle+\beta.|{\varphi}\rangle$ is a valid quantum state,
which is not always the case. In particular, if the norm of the input
$\alpha.|{\mathsf{true}}\rangle+\beta.|{\mathsf{false}}\rangle$ being $1$
implies that the norm of the output is also $1$, then this “quantum if”
instruction can be implemented by a quantum operator. The first work in this
line, defining the quantum-if in the lambda calculus, was that of Altenkirch
and Grattage [3]. Since then, there has been a long line of independent
research pursuing a “quantum computational logic”, that is, some sort of
quantum logic firmly founded on quantum computing.

This article intends to be an overview on this quest for a quantum
computational logic.

#### Plan of the paper

In Section 2 we give a brief introduction to the quantum computing formalism.
In Section 3 we present Lineal, an untyped extension to the lambda calculus to
deal with superpositions. It is the starting point on the quest for a quantum
computational logic. In Section 4 we present Vectorial and some of its
fragments, which is the first typed Lineal. In Section 5 we present
Lambda-$\mathcal{S}$, which is another typed Lineal, extended with quantum
measurements. We also provide a categorical interpretation of this calculus.
In Section 6 we show the first restriction of Lineal into a quantum language,
achieved by using realisability techniques. We then introduce the calculus
Lambda-$\mathcal{S}_{\\_}1$, which has been derived from this technique, and
give some details on its categorical interpretation. Such an interpretation is
related to that of Lambda-$\mathcal{S}$. In Section 7 we move from the
opposite direction: we define a new connective $\odot$ (read “sup”) in Natural
Deduction, which induces the $\odot$-calculus. Then, we show how to
transparently add complex scalars, defining the $\odot^{\mathbb{C}}$-calculus,
and use it to encode a quantum language. In Section 8 we refer to a few recent
works towards recursive types in the quantum control setting. Finally, we
conclude in Section 9 with some final thoughts and open problems.

##  2 Quantum computing in terms of four postulates

This section does not pretend to be an extensive introduction to quantum
computing but just for the basics, and we take the liberty to simplify many
things for the sake of readability. For a quite complete introduction to
quantum computing the reader is referred to the great book by Nielsen and
Chuang [35].

Quantum mechanics can be described in four axioms or postulates.

The first postulate defines how the quantum states are represented.

######  Postulate 1 (State space).

The state of an isolated quantum system can be fully described by a state
vector, which is a norm-$1$ vector in a Hilbert space, that is, Banach space
with inner product.

In quantum computing we usually consider the Hilbert space
$\mathbb{C}^{2^{n}}$, hence, from now on we only consider these spaces. For
vectors in $\mathbb{C}^{2^{n}}$ we use the Dirac notation consisting of a
binary encoding on vectors. For example,

$\displaystyle\left(\begin{smallmatrix}\frac{\sqrt{3}}{2}\\\
\frac{1}{2}\end{smallmatrix}\right)\in\mathbb{C}^{2}$ is written
$\frac{\sqrt{3}}{2}|{0}\rangle+\frac{1}{2}|{1}\rangle$,
$\displaystyle\mbox{and}\quad\left(\begin{smallmatrix}\frac{1}{\sqrt{3}}\\\
0\\\ \frac{1}{\sqrt{3}}\\\
\frac{1}{\sqrt{3}}\end{smallmatrix}\right)\in\mathbb{C}^{4}$ is written
$\frac{1}{\sqrt{3}}|{00}\rangle+\frac{1}{\sqrt{3}}|{10}\rangle+\frac{1}{\sqrt{3}}|{11}\rangle$.

A generic state vector is written $|{\psi}\rangle$. We also write
$\langle{\psi}|$ to the transpose conjugate of $|{\psi}\rangle$. This way,
$|{\psi}\rangle\langle{\varphi}|$ is a matrix while
$\langle{\psi}||{\varphi}\rangle$ (usually written
$\langle{\psi}|{\varphi}\rangle$) is the inner product
$(|{\psi}\rangle,|{\varphi}\rangle)$.

The second postulate defines how a quantum state evolves over time. We give
its discrete time version, since in quantum computing we usually consider
discrete time.

######  Postulate 2 (Evolution).

The evolution of an isolated quantum system can be described by a unitary
matrix, that is, a matrix $U$ such that $U^{\dagger}=U^{-1}$, where
$U^{\dagger}$ is the conjugate transpose of $U$. If the state of a quantum
system is described by $|{\psi}\rangle$, after the evolution $U$ the new state
is $|{\varphi}\rangle=U|{\psi}\rangle$.

######  Example 2.1.

Let $H=\left(\begin{smallmatrix}\frac{1}{\sqrt{2}}&\frac{1}{\sqrt{2}}\\\
\frac{1}{\sqrt{2}}&\frac{-1}{\sqrt{2}}\end{smallmatrix}\right)$, then

$\displaystyle H|{0}\rangle$
$\displaystyle=\frac{1}{\sqrt{2}}|{0}\rangle+\frac{1}{\sqrt{2}}|{1}\rangle=|{+}\rangle$
$\displaystyle H|{1}\rangle$
$\displaystyle=\frac{1}{\sqrt{2}}|{0}\rangle+\frac{-1}{\sqrt{2}}|{1}\rangle=|{-}\rangle$

where $|{+}\rangle$ and $|{-}\rangle$ are just conventional notations for
these vectors. In particular, notice that $\\{|{+}\rangle,|{-}\rangle\\}$ is
an orthonormal basis of $\mathbb{C}^{2}$ as well as
$\\{|{0}\rangle,|{1}\rangle\\}$. Hence, $H$ is a basis change matrix.

$H$ is known as the Hadamard gate.

The third postulate defines how a quantum system is measured. We give its
general form as Postulate 3, and a way to simplify it in Theorem 2.3.

######  Postulate 3 (Quantum measurement).

The quantum measurement is described by a collection of square matrices
$\\{M_{\\_}i\\}_{\\_}i$, where $i$ is called the output of the measurement,
such that

$\sum_{\\_}iM_{\\_}i^{\dagger}M_{\\_}i=I$

If the state of a quantum system is described by $|{\psi}\rangle$, the
probability of measuring $i$ is given by
$p_{\\_}i=\langle{\psi}|M_{\\_}i^{\dagger}M_{\\_}i|{\psi}\rangle$ and the
state after the measuring $i$ is
$|{\varphi}\rangle=\frac{1}{\sqrt{p_{\\_}i}}M_{\\_}i|{\psi}\rangle$.

######  Example 2.2.

Consider the following measurement: $\\{M_{\\_}0,M_{\\_}1\\}$, with
$M_{\\_}0=|{0}\rangle\langle{0}|$ and $M_{\\_}1=|{1}\rangle\langle{1}|$. That
is, $M_{\\_}0=\left(\begin{smallmatrix}1&0\\\ 0&0\end{smallmatrix}\right)$ and
$M_{\\_}1=\left(\begin{smallmatrix}0&0\\\ 0&1\end{smallmatrix}\right)$, and
let $|{\psi}\rangle=\frac{\sqrt{3}}{2}|{0}\rangle+\frac{1}{2}|{1}\rangle$.

Then,
$p_{\\_}0=\langle{\psi}|{0}\rangle\langle{0}|{0}\rangle\langle{0}|{\psi}\rangle=\frac{3}{4}$
and
$p_{\\_}1=\langle{\psi}|{1}\rangle\langle{1}|{1}\rangle\langle{1}|{\psi}\rangle=\frac{1}{4}$.
The state after measuring $0$ is $|{0}\rangle$ and after measuring $1$ is
$|{1}\rangle$.

The previous example can be taken as a general rule. With these $M_{\\_}0$ and
$M_{\\_}1$, in general, measuring $\alpha|{0}\rangle+\beta|{1}\rangle$ results
in $|{0}\rangle$ with probability $|\alpha|^{2}$ and $|{1}\rangle$ with
probability $|\beta|^{2}$.

Moreover, taking $\\{P_{\\_}b\\}_{\\_}{b\in\\{0,1\\}^{n}}$ with
$P_{\\_}b=|{b}\rangle\langle{b}|$ to measure the state
$|{\psi}\rangle=\sum_{\\_}b\alpha_{\\_}b|{b}\rangle$ results in $|{b}\rangle$
with probability $|\alpha_{\\_}b|^{2}$.

The following theorem states that such a measurement (usually called
“measurement in the computational basis”) is enough for quantum computing.

######  Theorem 2.3.

Any measurement $M=\\{M_{\\_}i\\}_{\\_}i$ can be simulated by a measurement in
the computational basis given by $P=\\{P_{\\_}b\\}_{\\_}{b\in\\{0,1\\}^{n}}$
with $P_{\\_}b=|{b}\rangle\langle{b}|$, and a unitary matrix $U$ in the sense
that measuring $|{\psi}\rangle$ with $M$ is the same as measuring
$U|{\psi}\rangle$ with $P_{\\_}b$ and applying $U^{-1}$ afterwards. ∎

The previous lemma justifies the fact that most quantum programming languages
consider only measurements in the computational basis.

Finally, the fourth postulate defines how to compose quantum systems.

######  Postulate 4 (Composed system).

The state space of a composed system is the tensor product of the state of its
components.

Given $n$ systems in states
$|{\psi_{\\_}1}\rangle,\dots,|{\psi_{\\_}n}\rangle$, the composed system is
described by $|{\psi_{\\_}1}\rangle\otimes\cdots\otimes|{\psi_{\\_}n}\rangle$.

######  Example 2.4.

If
$|{\psi}\rangle=\frac{1}{\sqrt{2}}|{0}\rangle+\frac{1}{\sqrt{2}}|{1}\rangle$
and
$|{\varphi}\rangle=\frac{1}{\sqrt{5}}|{0}\rangle+\frac{2}{\sqrt{5}}|{1}\rangle$,
the composed system $|{\psi}\rangle\otimes|{\varphi}\rangle$ is

$\left(\frac{1}{\sqrt{2}}|{0}\rangle+\frac{1}{\sqrt{2}}|{1}\rangle\right)\otimes\left(\frac{1}{\sqrt{5}}|{0}\rangle+\frac{2}{\sqrt{5}}|{1}\rangle\right)=\frac{1}{\sqrt{10}}|{00}\rangle+\frac{2}{\sqrt{10}}|{01}\rangle+\frac{1}{\sqrt{10}}|{10}\rangle+\frac{2}{\sqrt{10}}|{11}\rangle$

######  Definition 2.5 (qubit).

We call qubit, or quantum bit, to the quantum states in $\mathbb{C}^{2}$ and
$n$-qubit to quantum states in
$\mathbb{C}^{2^{n}}=\mathbb{C}^{2}\otimes\cdots\otimes\mathbb{C}^{2}$.

So, a qubit is written $\alpha|{0}\rangle+\beta|{1}\rangle$ and an $n$-qubit
is $\sum_{\\_}{b\in\\{0,1\\}^{n}}\alpha_{\\_}b|{b}\rangle$.

An important surprisingly consequence of the four postulates is the no-cloning
theorem [53], which states that an unknown quantum state cannot be duplicated.

######  Theorem 2.6.

There is no unitary matrix $U$ such that for some fixed
$|{\varphi}\rangle\in\mathbb{C}^{2^{n}}$ and for all
$|{\psi}\rangle\in\mathbb{C}^{2^{n}}$ we have
$U(|{\varphi}\rangle\otimes|{\psi}\rangle)=|{\psi}\rangle\otimes|{\psi}\rangle$.
∎

##  3 Lineal: A linear algebraic lambda calculus

Lineal, a seminal work by Arrighi and Dowek, first published at [6] and then
extended in [7], starts from the following simple idea: The Church encoding
for booleans, where $\lambda x.\lambda y.x$ represents $\mathsf{true}$ and
$\lambda x.\lambda y.y$ represents $\mathsf{false}$, follows the premise that
in the lambda calculus everything is a function, even the basic data.
Therefore, to consider quantum bits we would need to extend the lambda
calculus with complex linear combinations of lambda terms. This way, the qubit
$\alpha|{0}\rangle+\beta|{1}\rangle$ would be represented by $\alpha.\lambda
x.\lambda y.x+\beta.\lambda x.\lambda y.y$. More generally, we may consider
the infinite-dimensional Hilbert space whose basis is given by the values of
the lambda calculus.

Hence, Lineal proposes the following syntax of terms:

$t:=x\mid\lambda x.t\mid tt\mid\alpha.t\mid t+t\mid\vec{0}$

where $\alpha\in\mathbb{C}$ and the symbol $+$ is considered modulo
associativity and commutativity.

Its operational semantics has four groups of rules.

The beta group:

$(\lambda x.t)b\longrightarrow(b/x)t$

where $b$ is a basis term, that is, a classical value (either a variable or an
abstraction).

The elementary group:

$\begin{array}[]{r@{\ }l@{\qquad\qquad}r@{\ }l@{\qquad\qquad}r@{\
}l}t+\vec{0}&\longrightarrow t&0.t&\longrightarrow\vec{0}&1.t&\longrightarrow
t\\\
\alpha.\vec{0}&\longrightarrow\vec{0}&\alpha.(\beta.t)&\longrightarrow(\alpha\times\beta).t&\alpha.(t+r)&\longrightarrow\alpha.t+\beta.t\end{array}$

The factorization group:

$\begin{array}[]{r@{\ }l@{\qquad\qquad}r@{\ }l@{\qquad\qquad}r@{\
}l}\alpha.t+\beta.t&\longrightarrow(\alpha+\beta).t&\alpha.t+t&\longrightarrow(\alpha+1).t&t+t&\longrightarrow
2.t\end{array}$

The application group:

$\begin{array}[]{r@{\ }l@{\qquad\qquad}r@{\ }l@{\qquad\qquad}r@{\
}l}(t+r)s&\longrightarrow(ts)+(rs)&(\alpha.t)r&\longrightarrow\alpha.(tr)&\vec{0}t&\longrightarrow\vec{0}\\\
s(t+r)&\longrightarrow(st)+(sr)&r(\alpha.t)&\longrightarrow\alpha.(rt)&t\vec{0}&\longrightarrow\vec{0}\end{array}$

This way, for example, if $|{0}\rangle=\lambda x.\lambda y.x$ and
$|{1}\rangle=\lambda x.\lambda y.y$, a term encoding a unitary matrix $U$ will
act as follows:

$U(\alpha.|{0}\rangle+\beta.|{1}\rangle)\longrightarrow(U\alpha.|{0}\rangle)+(U\beta.|{1}\rangle)\longrightarrow^{*}\alpha.U|{0}\rangle+\beta.U|{1}\rangle$

For instance, the Hadamard gate (see Example 2.1) can be encoded as

$H:=\lambda
x.\left\\{x\left[\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{1}{\sqrt{2}}.|{1}\rangle\right]\left[\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{-1}{\sqrt{2}}.|{1}\rangle\right]\right\\}$
(1)

where $[t]:=\lambda x.t$ is a thunk and $\\{t\\}:=t\lambda x.x$ releases the
thunk (i.e. $\\{[t]\\}\longrightarrow^{*}t$).

The thunk is used to stop the linearity. Otherwise,
$H|{0}\rangle\longrightarrow|{0}\rangle\left(\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{1}{\sqrt{2}}.|{1}\rangle\right)\left(\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{-1}{\sqrt{2}}.|{1}\rangle\right)$,
which is just $(\lambda x.\lambda
y.x)\left(\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{1}{\sqrt{2}}.|{1}\rangle\right)\left(\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{-1}{\sqrt{2}}.|{1}\rangle\right)$
would reduce, using the rules at the application group, to

$\frac{1}{2}.(\lambda x.\lambda
y.x)|{0}\rangle|{0}\rangle+\frac{-1}{2}.(\lambda x.\lambda
y.x)|{0}\rangle|{1}\rangle+\frac{1}{2}.(\lambda x.\lambda
y.x)|{1}\rangle|{0}\rangle+\frac{-1}{2}.(\lambda x.\lambda
y.x)|{1}\rangle|{1}\rangle$

and then to

$\frac{1}{2}.|{0}\rangle+\frac{-1}{2}.|{0}\rangle+\frac{1}{2}.|{1}\rangle+\frac{-1}{2}.|{1}\rangle\longrightarrow^{*}\vec{0}$

instead of the expected
$\frac{1}{\sqrt{2}}.|{0}\rangle+\frac{1}{\sqrt{2}}.|{1}\rangle$.

So, the linearity achieved by the rules at the application group can be frozen
with thunks when needed, making Lineal a very expressive calculus of
computation combining matrices and vectors.

There is no measurement in Lineal. In addition, the rules of the operational
semantics have some constraints such as

“rule $\alpha.t+\beta.t\longrightarrow(\alpha+\beta).t$ applies only if $t$ is
closed normal” (2)

These constraints are needed in this untyped case where non-terminating terms
can break confluence. For example, let $\Delta_{\\_}b=\lambda x.(xx+b)$ and
$Y_{\\_}b=\Delta_{\\_}b\Delta_{\\_}b$. Then $Y_{\\_}b\longrightarrow
Y_{\\_}b+b$. If $b$ represents $1$, this $Y_{\\_}b$ can add up to infinity.
Then, since we have infinity and algebraic operations we may run into
undefined forms such as $\infty-\infty$, which here is represented by
$Y_{\\_}b+(-1).Y_{\\_}b$. Indeed, without any restrictions,
$Y_{\\_}b+(-1).Y_{\\_}b\longrightarrow 0.Y_{\\_}b\longrightarrow\vec{0}$, but
also $Y_{\\_}b+(-1).Y_{\\_}b\longrightarrow
Y_{\\_}b+b+(-1).Y_{\\_}b\longrightarrow^{*}b$. Hence, restriction (2) removes
this form of indeterminacy. There are other restrictions, but since we will
consider types in the next section, which ensures strong normalisation, we can
just ignore them.

######  Remark 3.1.

The algebraic linearity of Lineal implies that the no-cloning theorem (Theorem
2.6) is valid using this encoding of unitary matrices. Intuitively, the fact
that
$U(\alpha.|{0}\rangle+\beta.|{1}\rangle)\longrightarrow^{*}\alpha.U|{0}\rangle+\beta.U|{1}\rangle$
means that $\alpha$ and $\beta$ are never duplicated by $U$, and so it is not
possible to construct a term $U$ such that
$U(\alpha.|{0}\rangle+\beta.|{1}\rangle)$ reduce to
$(\alpha.|{0}\rangle+\beta.|{1}\rangle)\otimes(\alpha.|{0}\rangle+\beta.|{1}\rangle)$,
for any encoding of $\otimes$.

##  4 Vectorial: The first typed Lineal

Typing Lineal with simply types, or second order polymorphic types, is
possible by adding the following straightforward typing rules to simply typed
lambda calculus or System F, in order to type the extra constructions:

$\Gamma\vdash\vec{0}:A\qquad\qquad\Gamma\vdash
t+r:A\lx@proof@logical@and\Gamma\vdash t:A\Gamma\vdash
r:A\qquad\qquad\Gamma\vdash\alpha.t:A\Gamma\vdash t:A$

This way, the term $H$ from Equation (1) would be typed with
$(\tau\Rightarrow\tau\Rightarrow\tau)\Rightarrow(\tau\Rightarrow\tau\Rightarrow\tau)$,
for some basic type $\tau$.

A straightforward extension like this excludes from the calculus several valid
interesting terms. For example, let $t$ be a term typed with $\forall
X.A\Rightarrow B$ for some $A$. It could be applied not only to terms typed
with $[C/X]A$, but also to a linear combination
$\sum_{\\_}i\alpha_{\\_}i.r_{\\_}i$ as soon as each $r_{\\_}i$ is typed with
some $[C_{\\_}i/X]A$. Indeed, $t\sum_{\\_}i\alpha_{\\_}i.r_{\\_}i$ reduces to
$\sum_{\\_}i\alpha_{\\_}i.tr_{\\_}i$. However,
$\sum_{\\_}i\alpha_{\\_}i.r_{\\_}i$ may have type $\forall X.A$, but from
there, only one $C_{\\_}i$ can be chosen to type the whole term. A solution to
this lack of expressivity is provided by the Vectorial calculus [5], which
types this term with $\sum_{\\_}i\alpha_{\\_}i.[C_{\\_}i/X]A$.

The Vectorial calculus introduces linear combinations of types, in the same
way as Lineal considers linear combinations of terms. However, due to the
application group of rewrite rules, term variables must be typed only with
types that are not linear combinations of types (here called “unit types”).
Indeed, suppose we admit variables of type $\alpha.U$, so $\lambda x.x+y$ is
typed with $(\alpha.U)\Rightarrow(\alpha.U)+V$, where $V$ is the type of $y$.
Then, if $u$ is typed with $U$, we may expect $\alpha.u$ to be typed with
$\alpha.U$, and so $(\lambda x.x+y)(\alpha.u)$ has type $(\alpha.U)+V$.
However,

$(\lambda x.x+y)(\alpha.u)\longrightarrow\alpha.(\lambda
x.x+y)u\longrightarrow\alpha.(u+y)\longrightarrow\alpha.u+\alpha.y$

so its type should be $\alpha.U+\alpha.V$ instead.

Indeed, the abstracted variable $x$ has been substituted by $u$ and not by
$\alpha.u$ during reduction, and so, the type of the abstraction should
reflect this being just $U\Rightarrow U+V$. Therefore, term variables must be
typed with unit types.

On the other hand, type variables do not always need to be unit types. For
example, we may consider variables $\mathcal{X}$, $\mathcal{Y}$, which can be
substituted only by unit types, and variables $\mathbb{X}$, $\mathbb{Y}$,
which can be substituted by any type.

For instance, the Hadamard term $H$ from Equation (1) may be typed as follows.
Let
$\mathcal{T}=\forall\mathcal{X}.\forall\mathcal{Y}.\mathcal{X}\Rightarrow\mathcal{Y}\Rightarrow\mathcal{X}$
and
$\mathcal{F}=\forall\mathcal{X}.\forall\mathcal{Y}.\mathcal{X}\Rightarrow\mathcal{Y}\Rightarrow\mathcal{Y}$.
Also, if $t$ has type $A$, we let thunks $[t]$ be typed with $[A]$, which is
just a notation for
$(\forall\mathcal{X}.\mathcal{X}\Rightarrow\mathcal{X})\Rightarrow A$. Then,

$\vdash
H:\forall\mathbb{X}.\left(\left[\frac{1}{\sqrt{2}}.\mathcal{T}+\frac{1}{\sqrt{2}}.\mathcal{F}\right]\Rightarrow\left[\frac{1}{\sqrt{2}}.\mathcal{T}+\frac{-1}{\sqrt{2}}.\mathcal{F}\right]\Rightarrow\left[\mathbb{X}\right]\right)\Rightarrow\mathbb{X}$

The full grammar of types is the following.

$\displaystyle A$ $\displaystyle:=U\mid\alpha.A\mid A+A\mid\mathbb{X}$ Types
$\displaystyle U$ $\displaystyle:=\mathcal{X}\mid U\Rightarrow
A\mid\forall\mathcal{X}.U\mid\forall\mathbb{X}.U$ Unit types

where we use $A,B,C$ for types, $U,V,W$ for unit types,
$\mathbb{X},\mathbb{Y},\mathbb{Z}$ for variables, and
$\mathcal{X},\mathcal{Y},\mathcal{Z}$ for unit variables. We use $X,Y,Z$ to
refer to both kinds of variables.

There is also an equivalence between types given by the axioms of vector
spaces as follows.

$\begin{array}[]{r@{\ }l@{\qquad\qquad}r@{\ }l@{\qquad\qquad}r@{\
}l}1.A&\equiv A&\alpha.A+\beta.B&\equiv\alpha.(A+B)&A+B&\equiv B+A\\\
\alpha.(\beta.A)&\equiv(\alpha\beta).A&\alpha.A+\beta.A&\equiv(\alpha+\beta).A&A+(B+S)&\equiv(A+B)+S\end{array}$

There is no general null type $0$, but one type $0$ for each type $A$. So, the
term $\vec{0}$ is typed with the rule

$\Gamma\vdash\vec{0}:0.A\Gamma\vdash t:A$

Taking again the example that started this section, to type
$t\sum_{\\_}i\alpha_{\\_}i.r_{\\_}i$ where $\vdash t:\forall X.A\Rightarrow
B$, and for each $i$, $\vdash r_{\\_}i:[C_{\\_}i/X]A$ we consider an
$\Rightarrow$-elimination typing rule such as

$\Gamma\vdash
tr:\sum_{\\_}i\alpha_{\\_}i.[C_{\\_}i/X]B\lx@proof@logical@and\Gamma\vdash
t:\forall X.A\Rightarrow B\Gamma\vdash
r:\sum_{\\_}i\alpha_{\\_}i.[C_{\\_}i/X]A$

which is not only an $\Rightarrow$-elimination but also a
$\forall$-elimination at the same time.

Next, we also consider that $t$ can be a linear combination of terms, and,
since it is also a $\forall$-elimination, we may have more variables to
replace, which gives us the more general rule

$\Gamma\vdash
tr:\sum_{\\_}i\sum_{\\_}j\alpha_{\\_}i\beta_{\\_}j.[\vec{C}_{\\_}j/\vec{X}]B_{\\_}i\lx@proof@logical@and\Gamma\vdash
t:\sum_{\\_}i\alpha_{\\_}i.\forall\vec{X}.A\Rightarrow B_{\\_}i\Gamma\vdash
r:\sum_{\\_}j\alpha_{\\_}j.[\vec{C}_{\\_}j/\vec{X}]A$

where, as usual, notation $\forall\vec{X}.A$ stands for $\forall
X_{\\_}1.\dots.\forall X_{\\_}n.A$ and $[\vec{C}/\vec{X}]$ for
$[C_{\\_}1/X_{\\_}1]\cdots[C_{\\_}n/X_{\\_}n]$.

The main theorem in [5] is a strong normalisation result for this calculus.
However, subject reduction is proved only to some extent. Indeed, if $t$ has
both types $A$ and $B$, $\alpha.t+\beta.t$ may be typed with
$\alpha.A+\beta.B$, while its reduct, $(\alpha+\beta).t$ cannot. So, a weaker
subject reduction is proved, which states that if $\Gamma\vdash t:A$ and
$t\longrightarrow r$, then $\Gamma\vdash r:B$ with $B$ related to $A$ by an
ad-hoc relation. Later, [36] slightly modifies Vectorial obtaining a proper
subject reduction result, without losing its main properties.

Some fragments of Vectorial are the Scalar type system [4], which only
includes scalars on types but not sums. The Scalar type system can track the
“weight” of a type, defined as the $\ell_{\\_}1$-norm of a term, which is
useful, for example, to define a probabilistic type system out of Lineal, by
enforcing $\ell_{\\_}1$-norm to be equal to $1$ on each term. Another fragment
is the Additive type system [22], with sums but not scalars, which is shown to
be equivalent to System F with pairs.

##  5 Lambda-$\mathcal{S}$: Lineal plus measurement

Lineal takes care of three of the four postulates stated in Section 2.

  * •

Postulate 1, referring to state vectors, can be encoded in several ways in
Lineal. For example, we can take $|{0}\rangle:=\lambda x.\lambda y.x$ and
$|{1}\rangle:=\lambda x.\lambda y.y$, and then make its linear combination to
express any vector in $\mathbb{C}^{2}$. Also, for
$\vec{v}\in\mathbb{C}^{2^{n}}$ it suffices to consider the basis
$\\{\lambda\vec{x}.x_{\\_}1,\dots,\lambda\vec{x}.x_{\\_}{2^{n}}\\}$ where
$\lambda\vec{x}.x_{\\_}i$ stands for $\lambda x_{\\_}1.\dots.\lambda
x_{\\_}{2^{n}}.x_{\\_}i$.

  * •

Postulate 2, referring to unitary matrices, can be encoded easily also. For
example, any
$U=(\alpha_{\\_}{ij})_{\\_}{ij}\in\mathbb{C}^{2}\times\mathbb{C}^{2}$, can be
written as

$U:=\lambda
x.\left\\{x\left[\alpha_{\\_}{00}.|{0}\rangle+\alpha_{\\_}{01}.|{1}\rangle\right]\left[\alpha_{\\_}{10}.|{0}\rangle+\alpha_{\\_}{11}.|{1}\rangle\right]\right\\}$

  * •

Postulate 4, referring to composing systems, can be also represented by taking
the usual Church encoding for pairs, since the linearity given by the
application group of rewrite rules will make these pairs bi-linear (i.e. left
and right linear), as a tensor product.

The only missing postulate is Postulate 3, referring to measurements. Suppose
we want to add a term $\pi$ representing a measurement operator in the
computational basis such that $\pi(\alpha.|{0}\rangle+\beta.|{1}\rangle)$
reduces to $|{0}\rangle$ with probability $|\alpha|^{2}$ and to $|{1}\rangle$
with probability $|\beta|^{2}$ (if $|\alpha|^{2}+|\beta|^{2}=1$, otherwise it
suffices to divide this term by $|\alpha|^{2}+|\beta|^{2}$ before reducing).
The problem is that $\pi$ should not be linear, but then, $\lambda x.\pi x$
would not behave as $\pi$ since

$(\lambda x.\pi
x)(\alpha.|{0}\rangle+\beta.|{1}\rangle)\longrightarrow^{*}\alpha.(\lambda
x.\pi x)|{0}\rangle+\beta.(\lambda x.\pi
x)|{1}\rangle\longrightarrow^{*}\alpha.\pi|{0}\rangle+\beta.\pi|{1}\rangle\longrightarrow^{*}\alpha.|{0}\rangle+\beta.|{1}\rangle$

which is definitely not what we meant to do. Indeed, $(\lambda x.\pi x)r$
should reduce to $\pi r$ whatever $r$ is, even if it is a superposition. This
jeopardises the entire encoding. As we pointed out in Remark 3.1, the
algebraic linearity (i.e. the application group of rewrite rules) is needed to
forbid cloning. An alternative solution, first described in
Lambda-$\mathcal{S}$ [11, 15], is to allow for certain functions to be call-
by-name, that is, $(\lambda x.t)r$ reduces to $(r/x)t$ wherever $r$ is, at the
condition that $x$ appears at most once in $t$, which also forbids
duplication. With this goal in mind, Lambda-$\mathcal{S}$ is typed with simple
types, but adding a new symbol $S$ which marks the “superpositions”, as those
types that forbid duplication. The grammar of types is given by

$\displaystyle\Psi$ $\displaystyle:=\mathbb{B}\mid\Psi\times\Psi\mid S\Psi$
Qubit types $\displaystyle A$ $\displaystyle:=\Psi\mid\Psi\Rightarrow A\mid
A\times A\mid SA$ Types

Since superposition of superpositions is still a superposition, $SSA=SA$, and
since a basis term such as $|{0}\rangle$ can be seen as the superposition of
$1.|{0}\rangle+0.|{1}\rangle$, $A\leq SA$.

Lambda-$\mathcal{S}$ includes constants $|{0}\rangle$ and $|{1}\rangle$,
instead of using Church encodings, as well as an if-then-else construction.
However, the most interesting characteristic, other than the application group
from Lineal, is the fact that there are two beta-reductions, depending on
types. If $b$ is a basis term, then $(\lambda x:\mathbb{B}^{n}.t)b$ reduces to
$(b/x)t$, which is exactly Lineal’s beta-reduction. Instead, $(\lambda
x:S\Psi.t)r$ reduces directly to $(r/x)t$, for any $r$. However, the typing
system ensures that $x$ does not appear more than once in $t$ in this second
case. This way,

$(\lambda
x:\mathbb{B}.t)(\alpha.|{0}\rangle+\beta.|{1}\rangle)\longrightarrow\alpha.(\lambda
x:\mathbb{B}.t)|{0}\rangle+\beta.(\lambda
x:\mathbb{B}.t)|{1}\rangle\longrightarrow^{*}\alpha.(|{0}\rangle/x)t+\beta.(|{1}\rangle/x)t$

while

$(\lambda x:S\mathbb{B}.\pi
x)(\alpha.|{0}\rangle+\beta.|{1}\rangle)\longrightarrow\pi(\alpha.|{0}\rangle+\beta.|{1}\rangle)$

as expected.

The term $H$ from Example 2.1 is still valid, typed with
$\mathbb{B}\Rightarrow S\mathbb{B}$ on this system.

A first denotational semantics (in environment style) is given where the type
$\mathbb{B}$ is interpreted as
$\llbracket\mathbb{B}\rrbracket=\\{|{0}\rangle,|{1}\rangle\\}$ while $SA$ is
interpreted as $\mathsf{Span}\llbracket A\rrbracket$, the vector space
generated by $\llbracket A\rrbracket$. For example, $\llbracket
S\mathbb{B}\rrbracket=\mathbb{C}^{2}$. In [17, 19] a concrete categorical
interpretation is given, where $S$ is considered as a function of an
adjunction between the category $\mathbf{Set}$ and the category
$\mathbf{Vec}$. Explicitly, when we evaluate $S$ we obtain formal linear
combinations of elements of a set with complex numbers as coefficients. The
other functor in the adjunction, $U$ is just the forgetful functor allowing us
to forget its vectorial structure.

Later, in [18], an abstract categorical semantics of Lambda-$\mathcal{S}$ has
been defined. The main structural feature of such a model is that it is
expressive enough to describe the bridge between the property-less elements
such as $\alpha.v+\beta.v$, without any equational theory, and the result of
its algebraic manipulation into $(\alpha+\beta).v$, explicitly controlling its
interaction.

A distinctive design choice of Lambda-$\mathcal{S}$ is that we mark the
superpositions, which are the non-duplicable elements. This is somehow the
opposite of what is done in Linear Logic, where a bang $!$ marks the
duplicable elements. In fact, it is common that intuitionistic linear models
(linear as in linear-logic) are obtained by a monoidal comonad determined by a
monoidal adjunction $(S,m)\dashv(U,n)$, that is, the bang $!$ is interpreted
by the comonad $SU$ (see for example [8]). Instead, a crucial point of our
model of Lambda-$\mathcal{S}$ is to consider the monad $US$ for the
interpretation of $S$, determined by a similar monoidal adjunction. This
implies that on the one hand we have tight control of the Cartesian structure
of the model (i.e. duplication, etc.) and on the other hand superpositions
live in some sense inside the classical world determined externally by
classical rules until we decide to explore it. This is given by the following
composition of maps:

$US\mathbb{B}\times US\mathbb{B}\xrightarrow{n}U(S\mathbb{B}\otimes
S\mathbb{B})\xrightarrow{Um}US(\mathbb{B}\times\mathbb{B})$

######  Remark 5.1.

Lambda-$\mathcal{S}$ includes the four postulates, plus classical computation,
since simply typed lambda calculus is a subset of it. However, the first
postulate is included in a too general way, as with Lineal: any superposition
$\alpha.|{0}\rangle+\beta.|{1}\rangle$ is valid, for any $\alpha$ and $\beta$,
so, instead of taking norm-$1$ vectors (cf. Postulate 1), we are taking any
vectors. Moreover, an abstraction $\vdash\lambda
x:\mathbb{B}.t:\mathbb{B}\Rightarrow S\mathbb{B}$ may not represent a unitary
matrix. For example, $\lambda x:\mathbb{B}.\mathsf{if}\ x\ \mathsf{then}\
|{\psi}\rangle\ \mathsf{else}\ |{\varphi}\rangle$ is typable, but does not
represent a unitary map unless $|{\psi}\rangle\perp|{\varphi}\rangle$. To
ensure unitarity we should add some ad-hoc restrictions to ensure that the
branches of an if-then-else are orthogonal. However, the orthogonality of two
values is not so hard to define, but the orthogonality between arbitrary
programs does not seem to be an easy task.

QML [3] introduced some syntactic judgements of the form $t\perp r$ for a
limited subset of terms. In the next section we see how to produce a calculus
from a model where only norm-$1$ vectors are allowed.

##  6 Realisability to the rescue

From Remark 5.1 it is clear that we need a quite non-standard restriction to
the linear combinations. The fact that not every vector in $\mathbb{C}^{2}$ is
a qubit, but only those in the unitary sphere, is a hard condition to ask in a
type system. For example, in Vectorial (see Section 4) we may restrict types
$\alpha.A+\beta.B$ to the case $|\alpha|^{2}+|\beta|^{2}=1$, but if
$A=B=\forall\mathcal{X}.\mathcal{X}\Rightarrow\mathcal{X}\Rightarrow\mathcal{X}$,
this condition is not enough, for example, this is a valid type for
$\alpha.|{0}\rangle+\beta.|{0}\rangle\longrightarrow(\alpha+\beta).|{0}\rangle$,
which does not have norm $1$ if $|\alpha|^{2}+|\beta|^{2}=1$.

The restriction of Lambda-$\mathcal{S}$ to norm-$1$ vectors has been obtained
in [16] by means of realisability techniques [28, 52, 30, 33], which proved to
be a great method to add any kind of ad-hoc restrictions in a clean and easy
way. The technique can be summarised as follows:

  1. 1.

Take an untyped machine (i.e. a calculus with a fixed strategy). It is
confluent by definition.

  2. 2.

Then, define a grammar of types and give an interpretation $\llbracket
A\rrbracket$ for each type $A$ as a set of values, for example, allow only for
values $v$ such that $\|v\|=1$. So, it has norm-$1$ by definition.

  3. 3.

Then, define that a term $t$ is a realizer of $A$ (notation $t\vDash A$)
whenever $t\longrightarrow^{*}v\in\llbracket A\rrbracket$. A sequent
$\Gamma\vdash t:A$ is defined to be valid if for any valid substitution
$\sigma$ in $\Gamma$, $\sigma t\vDash A$. So, typed terms are strongly
normalising by definition, and subject reduction is also ensured by
definition.

  4. 4.

Finally, a typing rule of the kind

$\Gamma\vdash t:A\Delta\vdash r:B$

is valid as soon as $\Delta\vdash r:B$ implies $\Gamma\vdash t:A$. This way,
typing rules become theorems (potentially infinite many of them).

So, instead of defining typing rules and proving all its desirable properties,
we give the desirable properties by definition and prove the typing rules. Of
course this recipe does not tell us how to statically determine whether
$t\perp r$ for some arbitrary terms $t$ and $r$, but it gives us a way to
check whether any given typing rule is valid, and forces the system to only
let pass whatever terms we want (for example, only allow for terms of type
$S\mathbb{B}\Rightarrow S\mathbb{B}$ if those terms represent unitary maps).

The notation in this system is a bit modified from that of
Lambda-$\mathcal{S}$, so instead of $SA$ we write $\sharp A$ for the set
$\mathsf{Span}\llbracket A\rrbracket\cap\\{v\mid\|v\|=1\\}$ and we even have a
type $\flat A$ which is interpreted as the smallest set $V$ of values such
that $\sharp V$ contains $\llbracket A\rrbracket$. We do not give more details
in this quick overview, since there are many, but it is worth mentioning that
a quantum lambda calculus in the spirit of the QLC [48] is translated into
this calculus in [16].

As mentioned in the step 4 of the above enumeration, the typing rules are
potentially infinite. So, in [20] we extracted a finite fixed type system,
defining Lambda-$\mathcal{S}_{\\_}1$, and gave a categorical interpretation
for it. The model developed has some common grounds with the concrete model of
Lambda-$\mathcal{S}$ [17, 19], however, the chosen categories this time are
not $\mathbf{Set}$ and $\mathbf{Vec}$, but categories that use the fact that
values in this calculus form a “distributive-action space” (an algebraic
structure similar to a vector space, where its additive structure is a
semigroup). The two categories in the constructed adjunction are defined in
terms of $\vec{\mathsf{V}}$, the set of values in the calculus, and their
linear combinations (such a set forms a distributive-action space). Then, the
categories for the adjunction are defined by:

  * •

$\mathbf{Set}_{\\_}{\vec{\mathsf{V}}}$: a category whose objects are the non-
empty parts of $\vec{\mathsf{V}}$, and whose arrows are the arrows in
$\mathbf{Set}$ that can be defined in Lambda-$\mathcal{S}_{\\_}1$. This
category also includes a product $\boxtimes$, which is the set of separable
tensor products.

  * •

$\mathbf{SVec}_{\\_}{\vec{\mathsf{V}}}$: a category whose objects are the sub-
distributive action spaces of $\vec{\mathsf{V}}$, and whose arrows are the
linear maps which can be defined in Lambda-$\mathcal{S}_{\\_}1$. It also
includes a tensor product $\otimes$, which can also be defined as the span of
the product $\boxtimes$.

The main novelty and contribution of [20] is presenting a model for quantum
computing in the quantum control paradigm, which is show to be complete on
qubits in the sense that if two closed terms with qubit types are interpreted
by the same arrows in the model, then those terms are computationally
equivalent.

##  7 Sup: A new connective in Natural Deduction

As mentioned in the introduction, one of the main goals of the quantum control
approach to the lambda calculus is to envisage a quantum computational logic
(i.e. a quantum logic founded by quantum computing and an extension to the
Curry-Howard correspondence). In Section 4 we showed Vectorial, where if $A$
and $B$ are two propositions, so is $\alpha.A+\beta.B$. So, we could restrict
the valid propositions $A$ to those for whom there are valid proof terms $t$
such that $\vdash t:A$ and $t$ represents a quantum state. Vectorial can be
seen as the propositional logic of vector spaces. In Section 5 we gave another
form to the superposition of propositions: if $A$ is a proposition, then $SA$
is a superposition of propositions $A$. In this case the superposition symbol
is unary, and from several proofs $t_{\\_}i$ of $A$ we can construct a proof
$\sum_{\\_}i\alpha_{\\_}i.t_{\\_}i$ of $SA$. Similarly, in Section 6 we not
only gave the superpositions $SA$ (now noted $\sharp A$), but also another
unary symbol $\flat$, from where if $A$ is a proposition, $\flat A$ is the
proposition whose set of proofs is the minimum set such that the unary span of
such a set is the set of proofs of $\sharp A$.

In all these previous works we started from the lambda calculus Lineal, and
worked out a logic (a type system) from it. In [14] we started from the other
end. Starting from Natural Deduction we worked out a new connective for
superpositions, and from there we gave a proof system which can be used to
encode quantum computing on it.

The rest of this section paraphrases the extended abstract of [14] we have
presented at QPL 2021. Two nice video presentations given by Gilles Dowek can
be found at [24, 23].

#### Insufficient, harmonious, and excessive connectives

In natural deduction, to prove a proposition $C$, the elimination rule of a
connective $\vartriangle$ requires a proof of $A\vartriangle B$ and a proof of
$C$ using, as extra hypotheses, exactly the premises needed to prove the
proposition $A\vartriangle B$, with the introduction rules of the connective
$\vartriangle$. This principle of inversion, or of harmony, has been
introduced by Gentzen [26] and developed, among others, by Prawitz [39] and
Dummett [25] in natural deduction, by Miller and Pimentel [32] in sequent
calculus, and by Read [41, 42, 43] for the rules of equality.

For example, to prove the proposition $A\wedge B$, the introduction rule of
the conjunction requires a proof of $A$ and a proof of $B$, hence, to prove a
proposition $C$, the generalised elimination rule of the conjunction [46, 37,
34] requires, a proof of $A\wedge B$ and a proof of $C$, using, as extra
hypotheses, the propositions $A$ and $B$

$\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash A\wedge B\Gamma,A,B\vdash C$

This principle of inversion permits to define a cut elimination process where
the proof

$\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash A\wedge
B\lx@proof@logical@and\Gamma\vdash A\pi_{\\_}1\Gamma\vdash
B\pi_{\\_}2\Gamma,A,B\vdash C\pi_{\\_}3$

reduces to $(\pi_{\\_}1/A,\pi_{\\_}2/B)\pi_{\\_}3$.

In the same way, to prove the proposition $A\vee B$, the introduction rules of
the disjunction require a proof of $A$ or a proof of $B$, hence, to prove a
proposition $C$, the elimination rule of the disjunction requires a proof of
$A\vee B$ and two proofs of $C$, one using, as extra hypothesis, the
proposition $A$ and the other the proposition $B$

$\Gamma\vdash A\vee B\Gamma\vdash A\qquad\qquad\Gamma\vdash A\vee
B\Gamma\vdash B\qquad\qquad\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash
A\vee B\Gamma,A\vdash C\Gamma,B\vdash C$

and a cut elimination process can be defined similarly.

We also can imagine connectives that do not verify this inversion principle,
because the introduction rules require an insufficient amount of information
with respect to what the elimination rule provides, as extra hypotheses, in
the required proof of $C$. An example of such an insufficient connective is
Prior’s tonk [40], with the introduction and elimination rules as follows

$\Gamma\vdash A~{}\mbox{\it tonk}~{}B\Gamma\vdash A\qquad\qquad\Gamma\vdash
C\lx@proof@logical@and\Gamma\vdash A~{}\mbox{\it tonk}~{}B\Gamma,B\vdash C$

where the elimination rule requires a proof of $A~{}\mbox{\it tonk}~{}B$ and a
proof of $C$, using the extra hypothesis $B$, that is not required in the
proof of $A~{}\mbox{\it tonk}~{}B$, with the introduction rule. For such
connectives, cuts tonk-i / tonk-e cannot be reduced.

But, it is also possible that a connective does not verify the inversion
principle because the introduction rules require an excessive amount of
information. An example of such an excessive connective is the connective
$\odot$ that has the introduction rule of the conjunction and the elimination
rule of the disjunction

$\Gamma\vdash A\odot B\lx@proof@logical@and\Gamma\vdash A\Gamma\vdash
B\qquad\qquad\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash A\odot
B\Gamma,A\vdash C\Gamma,B\vdash C$

In this case, cuts can be eliminated. Moreover, several cut elimination
processes can be defined, exploiting, in different ways, the excess of the
connective. For example, the $\odot$-cut

$\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash A\odot
B\lx@proof@logical@and\Gamma\vdash A\pi_{\\_}1\Gamma\vdash
B\pi_{\\_}2\Gamma,A\vdash C\pi_{\\_}3\Gamma,B\vdash C\pi_{\\_}4$

can be reduced to $(\pi_{\\_}1/A)\pi_{\\_}3$, it can be reduced to
$(\pi_{\\_}2/A)\pi_{\\_}4$, it also can be reduced, non-deterministically,
either to $(\pi_{\\_}1/A)\pi_{\\_}3$ or to $(\pi_{\\_}2/A)\pi_{\\_}4$.
Finally, to keep both proofs, we can add a structural rule

$\Gamma\vdash A\lx@proof@logical@and\Gamma\vdash A\Gamma\vdash A$ and reduce
it to $\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash
C(\pi_{\\_}1/A)\pi_{\\_}3\Gamma\vdash C(\pi_{\\_}2/B)\pi_{\\_}4$

#### Information loss

With harmonious connectives, when a proof is built with an introduction rule,
the information contained in the proofs of the premises of this rule is
preserved. For example, the information contained in the proof $\pi_{\\_}1$ is
present in the proof $\pi$

$\Gamma\vdash A\wedge B\lx@proof@logical@and\Gamma\vdash
A\pi_{\\_}1\Gamma\vdash B\pi_{\\_}2$

in the sense that $\pi_{\\_}1$ is a subtree of $\pi$. But it is moreover
accessible, in the sense that, for all $\pi_{\\_}1$, putting the proof $\pi$
in the right context yields a proof that reduces to $\pi_{\\_}1$. And the same
holds for the proof $\pi_{\\_}2$.

The situation is different with an excessive connective: the excess of
information, required by the introduction rule, and not returned by the
elimination rule in the form of an extra hypothesis, in the required proof of
$C$, is lost. For example, the information contained in the proofs
$\pi_{\\_}1$ and $\pi_{\\_}2$ is present in the proof

$\Gamma\vdash A\odot B\lx@proof@logical@and\Gamma\vdash
A\pi_{\\_}1\Gamma\vdash B\pi_{\\_}2$

but its accessibility depends on the way we decide to reduce the cut

$\Gamma\vdash C\lx@proof@logical@and\Gamma\vdash A\odot
B\lx@proof@logical@and\Gamma\vdash A\pi_{\\_}1\Gamma\vdash
B\pi_{\\_}2\Gamma,A\vdash C\pi_{\\_}3\Gamma,B\vdash C\pi_{\\_}4$

If we reduce it systematically to $(\pi_{\\_}1/A)\pi_{\\_}3$, then the
information contained in $\pi_{\\_}1$ is accessible, but that contained in
$\pi_{\\_}2$ is not. If we reduce it systematically to
$(\pi_{\\_}2/A)\pi_{\\_}4$, then the information contained in $\pi_{\\_}2$ is
accessible, but not that contained in $\pi_{\\_}1$. If we reduce it not
deterministically to $(\pi_{\\_}1/A)\pi_{\\_}3$ or to
$(\pi_{\\_}2/A)\pi_{\\_}4$, then the information contained in both
$\pi_{\\_}1$ and $\pi_{\\_}2$ is accessible but non-deterministically. If we
reduce it with parallel, then the information contained in both $\pi_{\\_}1$
and $\pi_{\\_}2$ is inaccessible.

So, while harmonious connectives, that verify the inversion principle, model
information preservation, reversibility, and determinism, these excessive
connectives, that do not verify the inversion principle, model information
erasure, non-reversibility, and non-determinism. Such information erasure,
non-reversibility, and non-determinism, occur, for example, in quantum
physics, where the measurement of the superposition of two states does not
yield both states back.

#### A quantum language with $\odot$

As we have seen in the previous sections, several programming languages have
been designed to express quantum algorithms with quantum control. In
particular, in Lambda $\mathcal{S}$ (see Section 5), the measurement operator
$\pi$ comes together with the rule reducing $\pi(t+r)$ non-deterministically
to $t$ or to $r$.

The superposition $t+r$ can be considered as the pair $\langle t,r\rangle$, as
stated by [22]. Hence, it should have the type $A\wedge A$. In other words, it
is a proof-term of the proposition $A\wedge A$. In System I (first introduced
in [12] and later extended in [13, 50, 21]), various type-isomorphisms have
been introduced, in particular the commutativity isomorphism $A\wedge B\equiv
B\wedge A$, hence $t+r\equiv r+t$. In such a system, where $A\wedge B$ and
$B\wedge A$ are identical, it is not possible to define the two elimination
rules, as the two usual projections rules $\pi_{\\_}1$ and $\pi_{\\_}2$ of the
$\lambda$-calculus. They were replaced with a single projection parametrised
with a proposition $A$: $\pi_{\\_}A$, such that if $t$ is typed by $A$ and $r$
by $B$ then $\pi_{\\_}A(t+r)$ reduces to $t$ and $\pi_{\\_}B(t+r)$ to $r$.
When $A=B$, so $t$ and $r$ both have type $A$, the proof-term
$\pi_{\\_}A(t+r)$ reduces, non-deterministically, to $t$ or to $r$. Thus, this
modified elimination rule behaves like a measurement operator.

These works on Lambda-${\mathcal{S}}$ and System I brought to light the fact
that the pair superposition / measurement, in a quantum programming language,
behaves like a pair introduction / elimination, for some connective, in a
proof language, as the succession of a superposition and a measurement yields
a term that can be reduced. In System I, the assumption was made that this
connective was a commutative conjunction, with a modified elimination rule,
leading to a non-deterministic reduction.

However, as the measurement of the superposition of two states does not yield
both states back, this connective should probably be excessive. Moreover, as,
to build the superposition $a.|{0}\rangle+b.|{1}\rangle$, we need both
$|{0}\rangle$ and $|{1}\rangle$ and the measurement, in the basis
$|{0}\rangle,|{1}\rangle$, yields either $|{0}\rangle$ or $|{1}\rangle$, this
connective should have the introduction rule of the conjunction, and the
elimination rule of the disjunction, that is that it should be the connective
$\odot$.

In [14], we present a propositional logic with the connective $\odot$, a
language of proof-terms, the $\odot$-calculus (read: “the sup-calculus”), for
this logic, and we prove a cut elimination theorem. We then extend this
calculus into the $\odot^{\mathbb{C}}$-calculus (sup-$\mathbb{C}$-calculus),
introducing scalars to quantify the propensity of a proof to reduce to another
and show that its proof language forms the core of a quantum programming
language.

In particular, $\vdash\alpha.*:\top$ making of $\top$ a representation of
$\mathbb{C}$. In addition, while $\top\vee\top$ represent the booleans in the
lambda calculus, $\top\odot\top$ represents the qubits, $\mathbb{C}^{2}$. We
use $+$ to the proof term of the propositions $\odot$, and so
$\vdash:\alpha.*+\beta.*:\top\odot\top$ represents the vector
$\alpha.|{0}\rangle+\beta.|{1}\rangle$.

The elimination of $\odot$ has two proof terms:

$\Gamma\vdash\delta_{\\_}{\odot}^{\parallel}(t,[x]r,[y]s):C\lx@proof@logical@and\Gamma\vdash
t:A\odot B\Gamma,x:A\vdash r:C\Gamma,y:A\vdash r:C$
$\Gamma\vdash\delta_{\\_}{\odot}(t,[x]r,[y]s):C\lx@proof@logical@and\Gamma\vdash
t:A\odot B\Gamma,x:A\vdash r:C\Gamma,y:A\vdash r:C$

The first one reduces with the following rule

$\delta_{\\_}\odot^{\parallel}(\alpha.t+\beta.r,[x]s_{\\_}1,[y]s_{\\_}2)\longrightarrow\alpha.(t/x)s_{\\_}1\parallel\beta.(r/x)s_{\\_}2$

where the $\parallel$ is such that it behaves as a vectorial sum.

The second one reduces with the following rules instead

$\displaystyle\delta_{\\_}\odot(\alpha.t+\beta.r,[x]s_{\\_}1,[y]s_{\\_}2)$
$\displaystyle\longrightarrow(t/x)s_{\\_}1$
$\displaystyle\delta_{\\_}\odot(\alpha.t+\beta.r,[x]s_{\\_}1,[y]s_{\\_}2)$
$\displaystyle\longrightarrow(r/x)s_{\\_}2$

where the first reduction happens with probability
$\frac{|\alpha|^{2}}{|\alpha|^{2}+|\beta|^{2}}$ and the second with
probability $\frac{|\beta|^{2}}{|\alpha|^{2}+|\beta|^{2}}$.

The term $\delta_{\\_}\odot^{\parallel}$ is then used to encode quantum gates
and $\delta_{\\_}\odot$ to encode the measurement. See [14] for more details.

##  8 Towards quantum recursive types

A while language called qGCL with quantum control has been introduced in [45],
and an entire book on the subject has been written by Ying [54]. The idea is
to consider an infinite-dimensional Hilbert space and the while is guarded by
a binary measurement on one qubit, which stops when the outcome is $0$.

In [44], a similar idea of quantum control loop has been taken to the lambda
calculus, by endowing a typed, reversible, algebraic lambda calculus of
structural recursive fixpoints linked to the convergence of sequences in
infinite-dimensional Hilbert spaces. A categorical semantics of this language
is given in [31]. In [10], a language, based on this reversible language, is
typed in $\mu$MALL (linear logic extended with least and greatest fixed
points) allowing inductive and coinductive statements. While the paper [10] is
subtitled “work-in-progress”, it is a firm first step towards quantum
recursive types.

##  9 Some final thoughts

This quick overview aims to give a bird’s eye view on the quest for a quantum
computational logic. There are several clues on how this logic should be.
Either by representing superposition of propositions as $\alpha.A+\beta.B$
(see Section 4), as $SA$ or $\sharp A$ (see Sections 5 and 6) or by $A\odot B$
(see Section 7), the many options present different approaches, but all of
them are founded by the Curry-Howard isomorphism: a proposition is a type and
a proof is a term.

There is still work to do. One may wonder if from $\odot$ we may define a
measurement in Vectorial, for example, where the $+$ symbol at
$\alpha.A+\beta.B$ can be eliminated by a disjunction elimination. Or what is
the meaning of $\odot$ in sequent calculus, what categorical construction may
model it, etc.

All of those are open problems we are willing to investigate.

### Acknowledgements

The author wishes to thank Eduardo Bonelli and Mauricio Ayala-Rincón for the
inclusion of this overview in LSFA 2021 as an invited talk, and for their
useful comments.

## References

  * [1]
  * [2] Gadi Aleksandrowicz et. al. (2019): _Qiskit: An open-source framework for quantum computing_ , 10.5281/zenodo.2562111.
  * [3] Thorsten Altenkirch & Jonathan J. Grattage (2005): _A functional quantum programming language_.  In: Proceedings of LICS-2005, IEEE Computer Society, pp. 249–258, 10.1109/LICS.2005.1.
  * [4] Pablo Arrighi & Alejandro Díaz-Caro (2012): _A System F accounting for scalars_.  Logical Methods in Computer Science 8(1:11), 10.2168/LMCS-8(1:11)2012.
  * [5] Pablo Arrighi, Alejandro Díaz-Caro & Benoît Valiron (2017): _The vectorial $\lambda$-calculus_.  Information and Computation 254(1), pp. 105–139, 10.1016/j.ic.2017.04.001.
  * [6] Pablo Arrighi & Gilles Dowek (2008): _Linear-algebraic $\lambda$-calculus: higher-order, encodings, and confluence_.  In Andrei Voronkov, editor: Rewritting Techniques and Applications (RTA 2008), Lecture Notes in Computer Science 5117, Springer, pp. 17–31, 10.1007/978-3-540-70590-12.
  * [7] Pablo Arrighi & Gilles Dowek (2017): _Lineal: A linear-algebraic lambda-calculus_.  Logical Methods in Computer Science 13(1:8), 10.23638/LMCS-13(1:8)2017.
  * [8] Nick Benton (1994): _A mixed linear and non-linear logic: Proofs, terms and models_.  In Leszek Pacholski & Jerzy Tiuryn, editors: Computer Science Logic (CSL 1994), Lecture Notes in Computer Science 933, Springer, pp. 121–135, 10.1007/BFb0022251.
  * [9] Garrett Birkhoff & John von Neumann (1936): _The logic of quantum mechanics_.  Annals of Mathematics 37(4), pp. 823–843, 10.2307/1968621.
  * [10] Kostia Chardonnet, Alexis Saurin & Benoît Valiron (2020): _Towards a Curry-Howard equivalence for linear, reversible computation_.  In Ivan Lanese & Mariusz Rawski, editors: Reversible Computation (RC 2020), Lecture Notes in Computer Science 12227, Springer, pp. 348–364, 10.1007/978-3-030-52482-18.
  * [11] Alejandro Díaz-Caro & Gilles Dowek (2017): _Typing quantum superpositions and measurement_.  In Carlos Martín-Vide, Roman Neruda & Miguel A. Vega-Rodríguez, editors: Theory and Practice of Natural Computing (TPNC 2017), Lecture Notes in Computer Science 10687, Springer, pp. 281–293, 10.1007/978-3-319-71069-322.
  * [12] Alejandro Díaz-Caro & Gilles Dowek (2019): _Proof normalisation in a logic identifying isomorphic propositions_.  In Herman Geuvers, editor: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 14:1–14:23, 10.4230/LIPIcs.FSCD.2019.14.
  * [13] Alejandro Díaz-Caro & Gilles Dowek (2020): _Extensional proofs in a propositional logic modulo isomorphisms_.  arXiv:2002.03762.
  * [14] Alejandro Díaz-Caro & Gilles Dowek (2021): _A new connective in natural deduction, and its application to quantum computing_.  In Antonio Cerone & Peter Csaba Ölveczky, editors: Theoretical Aspects of Computing (ICTAC 2021), Lecture Notes in Computer Science 12819, Springer, pp. 175–193, 10.1007/978-3-030-85315-011.
  * [15] Alejandro Díaz-Caro, Gilles Dowek & Juan Pablo Rinaldi (2019): _Two linearities for quantum computing in the lambda calculus_.  BioSystems 186, p. 104012, 10.1016/j.biosystems.2019.104012.
  * [16] Alejandro Díaz-Caro, Mauricio Guillermo, Alexandre Miquel & Benoît Valiron (2019): _Realizability in the unitary sphere_.  In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), pp. 1–13, 10.1109/LICS.2019.8785834.
  * [17] Alejandro Díaz-Caro & Octavio Malherbe (2019): _A concrete categorical semantics for Lambda-S_.  In Beniamino Accattoli & Carlos Olarte, editors: Logical and Semantic Frameworks with Applications (LSFA’18), Electronic Notes in Theoretical Computer Science 344, Elsevier, pp. 83–100, 10.1016/j.entcs.2019.07.006.
  * [18] Alejandro Díaz-Caro & Octavio Malherbe (2020): _A categorical construction for the computational definition of vector spaces_.  Applied Categorical Structures 28(5), pp. 807–844, 10.1007/s10485-020-09598-7.
  * [19] Alejandro Díaz-Caro & Octavio Malherbe (2021): _A concrete model for a linear algebraic lambda calculus_.  arXiv:1806.09236.
  * [20] Alejandro Díaz-Caro & Octavio Malherbe (2021): _Quantum control in the unitary sphere: Lambda- $\mathcal{S}_{\\_}1$ and its categorical model_.  arXiv:2012.05887.
  * [21] Alejandro Díaz-Caro & Pablo E. Martínez López (2015): _Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of $\lambda^{+}$_.  In: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages (IFL 2015), ICPS Proceedings, ACM, pp. 9:1–9:11, 10.1145/2897336.2897346.
  * [22] Alejandro Díaz-Caro & Barbara Petit (2012): _Linearity in the non-deterministic call-by-value setting_.  In Luke Ong & Ruy de Queiroz, editors: Logic, Language, Information and Computation (WoLLIC 2012), Lecture Notes in Computer Science 7456, pp. 216–231, 10.1007/978-3-642-32621-916.
  * [23] Gilles Dowek (2021): _Presentation of[14] at ICTAC 2021_.  Available at https://drive.google.com/file/d/1E1DLQfTUg48jC325kOCNnftVgBe_k01A/view.
  * [24] Gilles Dowek (2021): _Presentation of[14] at QPL 2021_.  Available at https://www.youtube.com/watch?v=au0TDDp5qSw.
  * [25] Michael Dummett (1991): _The logical basis of metaphysics_.  Duckworth.
  * [26] Gerhard Gentzen (1935): _Untersuchungen über das logische Schließen_.  Mathematische Zeitschrift 39, pp. 176–210, 10.1007/BF01201353.
  * [27] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger & Benoît Valiron (2013): _Quipper: a scalable quantum programming language_.  ACM SIGPLAN Notices (PLDI’13) 48(6), pp. 333–342, 10.1145/2491956.2462177.
  * [28] Stephen C. Kleene (1945): _On the interpretation of intuitionistic number theory_.  The Journal of Symbolic Logic 10(4), pp. 109–124, 10.2307/2269016.
  * [29] Emanuel H. Knill (1996): _Conventions for quantum pseudocode_.  Technical Report LA-UR-96-2724, Los Alamos National Laboratory, 10.2172/366453.
  * [30] Jean-Louis Krivine (2009): _Realizability in classical logic_.  Panoramas et synthèses: Interactive models of computation and program behaviour 27, pp. 197–229.  Available at hal-00154500.
  * [31] Louis Lemonnier, Kostia Chardonnet & Benoît Valiron (2021): _Categorical semantics of reversible pattern-matching_.  arXiv:2109.05837.
  * [32] Dave Miller & Elaine Pimentel (2013): _A formal framework for specifying sequent calculus proof systems_.  Theoretical Computer Science 474, pp. 98–116, 10.1016/j.tcs.2012.12.008.
  * [33] Alexandre Miquel (2011): _A survey of classical realizability_.  In Luke Ong, editor: Typed Lambda Calculi and Applications (TLCA 2011), Lecture Notes in Computer Science 6690, pp. 1–2, 10.1007/978-3-642-21691-61.
  * [34] Sara Negri & Jan von Plato (2008): _Structural Proof Theory_.  Cambridge University Press.
  * [35] Michael Nielsen & Isaac Chuang (2000): _Quantum Computation and Quantum Information_.  Cambridge University Press., 10.1017/CBO9780511976667.
  * [36] Francisco Noriega & Alejandro Díaz-Caro (2020): _The Vectorial Lambda Calculus Revisited_.  arXiv:2007.03648.
  * [37] Michel Parigot (1991): _Free deduction: An analysis of “Computations” in classical logic_.  In A. Voronkov, editor: Logic Programming, Lecture Notes in Computer Science 592, Springer, pp. 361–380, 10.1007/3-540-55460-227.
  * [38] Jennifer Paykin, Robert Rand & Steve Zdancewic (2017): _QWIRE: A Core Language for Quantum Circuits_.  In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, ACM, pp. 846–858, 10.1145/3009837.3009894.
  * [39] Dag Prawitz (1965): _Natural deduction. A proof-theoretical study_.  Almqvist & Wiksell.
  * [40] Arthur N. Prior (1960): _The runabout inference-ticket_.  Analysis 21(2), pp. 38–39, 10.1093/analys/21.2.38.
  * [41] Stephen Read (2004): _Identity and harmony_.  Analysis 64(2), pp. 113–119, 10.1093/analys/64.2.113.
  * [42] Stephen Read (2010): _General-elimination harmony and the meaning of the logical constants_.  Journal of Philosophical Logic 39, pp. 557–576, 10.1007/s10992-010-9133-7.
  * [43] Stephen Read (2014): _Identity and harmony revisited_.  Available at https://www.st-andrews.ac.uk/~slr/identity_revisited.pdf.  Informal publication.
  * [44] Amr Sabry, Benoît Valiron & Juliana Kaizer Vizzotto (2018): _From Symmetric Pattern-Matching to Quantum Control_.  In Christel Baier & Ugo Dal Lago, editors: Foundations of Software Science and Computation Structures (FoSSaCS 2018), Lecture Notes in Computer Science 10803, Springer, pp. 348–364, 10.1007/978-3-319-89366-219.
  * [45] Jeff W. Sanders & Paolo Zuliani (2000): _Quantum programming_.  In Roland Backhouse & José Nuno Oliveira, editors: Mathematics of Program Construction (MPC 2000), Lecture Notes in Computer Science 1837, Springer, pp. 80–99, 10.1007/107220106.
  * [46] Peter Schroeder-Heister (1984): _A natural extension of Natural deduction_.  The Journal of Symbolic Logic 49(4), pp. 1284–1300, 10.2307/2274279.
  * [47] Peter Selinger (2004): _Towards a quantum programming language_.  Mathematical Structures in Computer Science 14(4), pp. 527–586, 10.1017/S0960129504004256.
  * [48] Peter Selinger & Benoît Valiron (2006): _A lambda calculus for quantum computation with classical control_.  Mathematical Structures in Computer Science 16(3), pp. 527–552, 10.1017/S0960129506005238.
  * [49] Morten Heine Sørensen & Paweł Urzyczyn (1998): _Lectures on the Curry-Howard isomorphism_.  Studies in Logic and the Foundations of Mathematics 149, Elsevier.
  * [50] Cristian Sottile, Alejandro Díaz-Caro & Pablo E. Martínez López (2020): _Polymorphic System I_.  In: Proceedings of the 32nd Symposium on the Implementation and Application of Functional Programming Languages (IFL 2020), ICPS Proceedings, ACM, pp. 127–137, 10.1145/3462172.3462198.
  * [51] Microsoft Quantum Team (2017): _The Q $\sharp$ programming language_.  Available at {https://docs.microsoft.com/en-us/quantum/quantum-qr-intro?view=qsharp-preview}.
  * [52] Jaap van Oosten (2008): _Realizability. An introduction to its categorical side_.  Studies in Logic and the Foundations of Mathematics 152, Elsevier.
  * [53] William K. Wootters & Wojciech H. Zurek (1982): _A single quantum cannot be cloned_.  Nature 299, pp. 802–803, 10.1038/299802a0.
  * [54] Mingsheng Ying (2016): _Foundations of Quantum Programming_.  Elsevier.