Quantitative approaches (20 – 24 February)

Talk list

Lectures

  • Thomas Ehrhard (Paris, France), Extensional collapse of the relational semantics of Linear Logic, and applications.

    We present a model of Classical Linear Logic whose objects can be understood as triples made of the relational interpretation of a type, the interpretation of the same type as a prime-algebraic lattice (Scott interpretation) and a realizability predicate between these interpretations. We prove that, in this model, all types with parameters have a least fix-point in some sense, and hence that this model contains many models of the pure lambda-calculus (in CBN and CBV).

    In the relational semantics, where the exponential is non-idempotent, proving sensibility results of models (theorems of the kind: if the interpretation of a term is non-empty, then this term normalizes in some sense) by purely combinatorial means is possible. Indeed, such results boil down to normalization in a suitable promotion-free resource lambda-calculus whose term denote derivations of the fact that a given point of the model belong to the interpretation of a term (aka intersection typing).

    We show how to use our collapse model for transferring such results to Scott models, where these combinatorial methods are not available, and where such sensibility results are obtained by syntactic reducibility methods only. This approach applies to many situations in a completely uniform way: in some sense, all the realizability structure needed to prove results of this kind has been encapsulated in the construction of the model, once and for all.

    • Thursday 23, 9:00
  • Elham Kashefi (Edinburgh, UK), Tutorial on quantum computing.
    • Monday 20, 10:40
    • Tuesday 21, 10:40
  • Prakash Panangaden (Montréal, Canada), Markov processes as function transformers: bisimulation and approximation.
    • Monday 20, 9:00 — Part I: Overview and Categories of Cones
    • Tuesday 21, 9:00 — Part II: Functorial View of Expectation Values
    • Wednesday 22, 9:00 — Part III: Bisimulation, minimal realization and approximation
  • Christine Tasson (Paris, France), From quantitative semantics to syntaxes.
    • Wednesday 22, 10:40
    • Friday 24, 9:00

Invited talks

  • Pablo Arrighi (Grenoble, France), The physical Church-Turing thesis and the principles of quantum theory.

    (joint work with Gilles Dowek)

    Notoriously, quantum computation shatters complexity theory, but is innocuous to computability theory. Yet several works have shown how quantum theory as it stands could breach the physical Church-Turing thesis. We draw a clear line as to when this is the case, in a way that is inspired by Gandy. Gandy formulates postulates about physics, such as homogeneity of space and time, bounded density and velocity of information --- and proves that the physical Church-Turing thesis is a consequence of these postulates. We provide a quantum version of the theorem. Thus this approach exhibits a formal non-trivial interplay between theoretical physics symmetries and computability assumptions.

    • Tuesday 21, 15:20
  • Rick Blute (Ottawa, Canada), Homological algebra and differential linear logic.
    • Friday 24, 14:00
  • Robin Cockett (Calgary, Canada), What is a Differential PCA?.

    (joint work with Jonathan Gallagher)

    There is a tight correspondence between partial combinatory algebras (PCAs) and Turing categories. This correspondence can be used to help develop an answer to the question of the title: for one would hope to be able to maintain this correspondence as one adds differential structure. The talk will consider this correspondence at three different levels, namely, for ordinary Turing categories, left additive Turing categories, and differential Turing categories.

    For ordinary Turing categories the ability to split idempotents is a crucial aspect of their description. In particular, the "recognition theorem" for these categories relies on this ability. An important example of an idempotent, which must be present in all PCAs and must split in the associated Turing category, is the pairing combinator. A complication, as one moves to left-additive or differential Turing categories, is that the ability to split -- while retaining the property of being left-additive or differential category -- arbitrary idempotents is lost. The structure of these settings is, therefore, linked to the question of which idempotents can still be split.

    In fact, in the movement from left-additive to differential Turing categories, the question of which idempotents can be split becomes significantly more delicate. The talk presents a solution to these issues and, thus, (albeit implicitly) an answer to the question in the title.

    • Friday 24, 15:20
  • Ross Duncan (Brussels, Belgium), Interacting Observables in Categorical Quantum Mechanics.

    One of the most shocking features of quantum mechanics is the possibility that quantum observables may be incompatible: when one property is well-defined, another cannot have a definite value assigned to it. This is most clearly seen in the case of complementary observables, such as the spin along the X and Z axes. Perfect knowledge of the X spin implies complete ignorance of the Z spin. Historically complementarity has been viewed as a negative property, a failure of some classical behaviour; however, from a different point of view a positive attitude is possible.

    Non-degenerate quantum measurements are equivalent to coalgebras whose action is to copy and delete the eigenstates associated with the observable; in this way we may view each observable as embedding a classical data type in the quantum world. When two complementary observables are considered together, they jointly form a structure closely related to a Hopf algebra. These interacting algebras give rise to much of the equational structure exploited in quantum computing. Further, all of the axiomatisation can be performed in an abstract categorical setting, and a beautiful, highly legible graphical notation results.

    I will introduce the basic ideas of categorical quantum mechanics, and the the various algebra structures and demonstrate some applications in concerning quantum circuits and measurement-based quantum computing.

    • Monday 20, 14:00
  • Jean Goubault-Larrecq (Paris, France), Probability and Nondeterminism in Domain Theory, Part II.

    As the title indicates, this is a follow-up on Daniele Varacca's talk. We shall first talk about the very intuitive denotational model of probabilistic choice given by so-called continuous random variables, and will explain the relation to indexed valuations, as seen in Part I. We shall then explore a few solutions to the problem of giving semantics to mixed non-deterministic and probabilistic higher-order functional programs. While indexed valuations and continuous random variables solve the problem by changing the model of probabilistic choice, previsions and the Mislove-Ouaknine-Worrell and Tix-Kleimel-Plotkin models solve it by changing the model of non-deterministic choice to convex non-determinism. We shall conclude by returning to some of the goals stated at the beginning of Part I, and shall establish a few full abstraction results for variants of PCF with choice, exhibiting the differences in observable properties that each model exhibits.

    • Thursday 23, 15:20
  • Alexander Green (Dalhousie University, Canada), Functional Quantum Programming.

    Within the realm of computer science, it is common to use higher-level structures to simplify the design of algorithms, and abstract away from all the low-level details. For example, computers run at the lowest level on bits, but computer programmers use high-level languages to abstract away from simple logic gates acting on these individual bits. This talk looks at how we can extend these ideas within the realm of quantum computation, and looks at how we can model a low-level quantum mechanical system in terms of a higher-level language, or in terms of higher level constructs within a quantum programming language. In particular, we will focus on ideas that have arisen within the functional paradigm, and see that the side-effects inherent in the measurement aspects of quantum computation play nicely with constructs from pure functional languages, such as Monads in Haskell, that are used to give explicit access to effects.

    • Tuesday 21, 14:00
  • Aleks Kissinger (Oxford, UK), Picturing Non-locality: Generalised Mermin Arguments in Categorical Quantum Mechanics.

    One might ask if the apparent non-locality of quantum mechanics is simply a side affect of local (i.e. classical) statistical correlations in physical quantities that we cannot measure directly. However, Bell's theorem showed that quantum mechanics produced statistical correlations that could not be explained with any local hidden variable model. In a remarkable thought experiment in 1990, Mermin strengthened result by picturing an experimental setup where not a single local hidden state could reproduce the predictions of quantum mechanics with non-zero probability. Whereas Bell's theorem relies on specific probabilities of outcomes to rule out locality, Mermin's only relies on possibilities.

    While this argument is compelling, it only hints at the structural elements of quantum mechanics at play in the manifestation of non-locality. Perhaps the most crucial of these elements is the notion of complementary observables. These are physical quantities where maximal knowledge of one implies minimal knowledge of the other (c.f. position and momentum), and especially a particular kind of complementary observables which we call "strongly complementary observables". The features of strong complementarity can be totally represented in the abstract context of dagger-monoidal categories, and provides a vehicle for constructing a completely abstract version of the Mermin argument. Perhaps the most striking feature of this translation comes from the use of graphical language for monoidal categories, wherein conceptual notions like locality, measurement, and parity of outcomes are evident in the topology of string diagrams.

    • Monday 20, 15:20
  • Daniele Varacca (Paris, France), Probability and Nondeterminism in Domain Theory, Part I.

    I will first introduce the notion of continuous valuations, used by Jones and Plotkin to represent probabilities in domain theory. I will in particular discuss the Splitting Lemma which gives an intuition about the way valuations are ordered. I will then explain why the valuations are "troublesome" (as defined by Jung and Tix): no cartesian closed category of continuous domains is known to be preserved by the valuations functor, and therefore they cannot be used in the semantics of functional programming languages, like a probabilistic extension of PCF.

    Valuations are troublesome also because they do not combine well with the nondeterminisitic models of domain theory. I will show why and I will introduce another probabilistic model that is designed to solve this problem: the indexed valuations. I will show how the Splitting Lemma translates within indexed valuations. Indexed valuations also pave the way towards random variables will be presented by Jean Goubault-Larrecq in Part II.

    Fear not. Only very lightweight notions of category theory and of universal algebra will be used in this talk.

    • Thursday 23, 14:00

Contributed talks

  • Geoff Cruttwell (Ottawa, Canada), Reconsidering Cartesian differential categories.

    (joint work with Robin Cockett)

    Blute, Cockett and Seely defined Cartesian differential categories as a beginning for the study of the categorical semantics of Ehrhard and Regnier’s differential λ-calculus. As we shall see, however, several small problems with the definition mean that it is less robust than desired. For one example, while smooth maps between Cartesian spaces are an example of a Cartesian differential category, smooth maps between open subsets of Cartesian spaces are not. Through a slight generalization of the definition of Cartesian differential categories, we shall show that this and other problems can be resolved. In particular, following work by Cockett and Seely, we will show that the resulting generalized Cartesian differential categories are comonadic over cartesian categories, providing a wealth of new examples.

    • Friday 24, 11:20
  • Alejandro Díaz-Caro (Villetaneuse, France), Equivalence on propositions and proofs.

    (Joint work with Gilles Dowek)

    We know that the propositions A∧B and B∧A are equiprovable: one is provable if and only if the other is, but they do not have the same proofs. Here we design a proof system such that they have the same proofs, i.e. we take the quotient of the set of propositions by the relation generated by the commutativity of conjunction, and define proofs for elements in this quotient. The calculus obtained is similar to the additive fragment of the algebraic lambda-calculi plus a non-deterministic projector.

    • Thursday 23, 10:40
  • Claudia Faggian (Paris, France), Geometry of Interaction and Quantum Circuits .

    (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.

    • Monday 20, 16:20
  • Benoît Valiron (Philadelphia, US), On denotational semantics of quantum computation.

    (joint work with Michele Pagani and Peter Selinger)

    If denotational semantics of strictly linear quantum computation is relatively well understood using the category CPM of completely positive maps, the relation between duplicable and non-duplicable data is yet to be analyzed. In this talk I will present an approach for understanding duplicable objects in quantum computation. The technique I will present extends the well-known category CPM using the general constructions of the exponential "!" that can be used in relational models of linear logic.

    • Friday 24, 10:40