Claudia Faggian (Paris, France), Geometry of Interaction and Quantum Circuits
Schedule
- Feb. 20, 2012, 16:20 - 17:00
Abstract
(joint work with Ugo Dal Lago)
Since the very first work on quantum programming languages (both by Van Tonder and by Selinger), it has been clear that there is a strong relationships between linear logic and quantum computation. This relationship has played a major role in all developments since;
we still lack however a true correspondence between linear logic as a proof theory and quantum computation as a computational model.
We describe ongoing work which investigates the relationships between quantum computation and linear logic, driven by Geometry of Interaction (GoI).. There are two guiding ideas behind our approach. On one side is the quest for a model which should be concrete and should allow for an efficient encoding of quantum computation (ideally, GoI should eventually be able to talk about the computational complexity of the calculus). On the other side, we aim for a proof-theoretical account of both quantum information and computation (i.e. quantum data and algorithms).
In its original formulation, the GoI gives a dynamic interpretation of computation as a flow of information circulating around a net. This flow of information can be formulated both as a token-based interactive machine, or as an algebra of bounded operators on the infinite dimension Hilbert space, which is the canonical state space for quantum computation models.
Here we exploit both aspects.
We introduce a logical system, QMLL, which extends MLL with a quantum modality, and whose design has been guided by intuitions on the underlying “quantum GoI” interpretation.
QMLL is shown able to capture all unitary quantum circuits. Conversely, any proof is shown to compute, through a concrete GoI interpretation, some quantum circuits. A key ingredient in the proof is an interactive abstract machine.
(joint work with Ugo Dal Lago)
Since the very first work on quantum programming languages (both by Van Tonder and by Selinger), it has been clear that there is a strong relationships between linear logic and quantum computation. This relationship has played a major role in all developments since; we still lack however a true correspondence between linear logic as a proof theory and quantum computation as a computational model.
We describe ongoing work which investigates the relationships between quantum computation and linear logic, driven by Geometry of Interaction (GoI).. There are two guiding ideas behind our approach. On one side is the quest for a model which should be concrete and should allow for an efficient encoding of quantum computation (ideally, GoI should eventually be able to talk about the computational complexity of the calculus). On the other side, we aim for a proof-theoretical account of both quantum information and computation (i.e. quantum data and algorithms).
In its original formulation, the GoI gives a dynamic interpretation of computation as a flow of information circulating around a net. This flow of information can be formulated both as a token-based interactive machine, or as an algebra of bounded operators on the infinite dimension Hilbert space, which is the canonical state space for quantum computation models. Here we exploit both aspects.
We introduce a logical system, QMLL, which extends MLL with a quantum modality, and whose design has been guided by intuitions on the underlying “quantum GoI” interpretation. QMLL is shown able to capture all unitary quantum circuits. Conversely, any proof is shown to compute, through a concrete GoI interpretation, some quantum circuits. A key ingredient in the proof is an interactive abstract machine.