Objectives and learning outcomes
The development of quantum information and computation entails the need for formal tools to model, verify and reason rigorously about quantum programs. This course explores the connection between (quantum) computation, (resource-sensitive) logic, and category theory, given by the Curry-Howard-Lambek correspondence, which identifies propositions with types and proofs with programs, and formalizes the model space as a (monoidal) category.
Thus, in the end, students will be able to apply to the development of quantum programs a solid and operative knowledge in
-
semantics and logics for quantum programs.
NEW: List of Research Exercises
All information available
HERE
Syllabus
- Categories for quantum computing
- Categories, funtors, and natural transformations.
- Universal properties and adjunctions.
- Monoidal categories; Aplications: (categories of) relations, matrices, and Hilbert spaces.
- Diagramatic reasoning in monoidal categories
- Diagramatic representations of monoidal categories. String diagrams.
- Computational interpretation of quantum mechanics; associated categorical structures: monoidal (composition), compact closed (entanglement), adjunctions (internal product), biproduts (non deterministic branching).
- Quantum processes.
- The Curry-Howard-Lambek correspondence.
- Introduction to intuitionistic and linear logic.
- Introduction to the simply-typed lambda-calculus.
- Quantum lambda-calculus.
- The Curry-Howard-Lambek correspondence for classical computation.
- The Curry-Howard-Lambek correspondence for quantum computation.
Summaries (2021-22)
T Lectures
-
Feb 15 (11-13h):
Introduction to the course: objectives, learning outcomes, organisation.
Categories: definition and worked examples.
-
Feb 22 (11-13h):
Functors: definition and worked examples.
-
Mar 03 (09-11h):
Introduction to universal properties. Initial and final objects. Products: definitions, examples, properties.
-
Mar 08 (11-13h):
Duality. Coproducts: definitions, examples, properties.
-
Mar 15 (11-13h):
Naturality, the last corner of the categorical imperative (Functoriality, Universality, Naturality). Examples of natural transformations. Composition. Equivalence of categories.
-
Mar 22 (11-13h):
Processes and diagrams. Monoidal categories and representation of process theories. Introduction to diagramatic reasoning.
-
Mar 29 (11-13h):
String diagrams. Non-separability. Representing transpose, trace, adjoint, conjugate and inner product.
-
Abr 5 (11-13h):
Unitary processes and projectors in string diagrams. Expressing quantum phenomena in theories interpreted over string diagrams (e.g. non cloning; teleportation). Dagger compact-closed categories.
-
Abr 19 (11-13h):
The process theory of linear maps: properties and constructions.
-
Abr 26 (11-13h):
F
-
May 03 (11-13h):
Introduction to the ZX-calculus. Examples.
[Tutorial by John van de Wetering (2020)]
-
May 17 (11-13h):
Untyped lambda-calculus: Examples. Dicussion of the research projects.
-
May 17 (14-16h):
Introduction to intuitionistic logic.
-
May 24 (11-13h):
Revisiting Cartesian-closed categories. The exponential object. The Curry-Howard-Lambek correspondence for classical computation.
TP Lectures
-
Feb 18 (08-10h):
Familiar and less familiar examples of categories. Exercises on defining / checking the strucutre of a category. Exercises on rephrasing well-known, pointwise results in the language of categories: Isomorphisms, monomorphisms and epimorphisms.
-
Feb 24 (09-11h):
Exercises on functors. Full and faithful functors. The categories CAT and Cat. Isomorphisms between categories.
-
Mar 10 (09-11h):
Product and coproduct: examples and properties.
-
Mar 24 (09-11h):
Quantum walks: introduction and open problems (lecture by Dr Bruno Chagas) [slides]
-
Mar 31 (09-11h):
Exercises on string diagrams.
-
Abr 7 (9-11h):
Basis and sums in string diagrams --- towards a process theory of linear maps. From processes to matrices and back.
-
Abr 21 (9-11h):
The process theory of linear maps. Exercises. Categorial foundations: introducing sums through enriched categories.
-
Abr 21 (15-16h):
Extra non-formal lecture on "Categorical composable cryptography" by Martti Karvonen [slides].
-
Abr 28 (9-11h):
From linear maps to (pure) quantum maps. Process doubling.
-
May 5 (9-11h):
Introduction to the Curry-Howard-Lambek correspondence. The untyped lambda-calculus.
-
May 19 (9-11h):
Simply typed lambda-calculus. The Curry-Howard correspondence with intuitionistic logic.
Support
Lecture Notes / Exercises
Reference papers
Bibliography
-
S. Abramsky and N. Tzevelekos. Introduction to categories and categorical logic. In B. Coecke,
editor, New Structures for Physics, pages 3–94. Springer Lecture Notes on Physics
(813), 2011.
-
J. Baez and M. Stay. Physics, topology, logic and computation: A Rosetta stone. In B. Coecke,
editor, New Structures for Physics, pages 95–172. Springer Lecture Notes on Physics
(813), 2011.
-
B. Coecke and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum
Theory and Diagrammatic Reasoning . Cambridge University Press, 2017.
-
C. Heunen and J. Vicary. Categories for Quantum Theory. Oxford Graduate Texts in Mathematics, 2019.
Complementary Bibliography
-
S. Awodey. Category Theory. Oxford Logic Guides. Oxford University Press, 2006.
-
Emily Riehl. Category Theory in Context. Aurora - Dover Modern Math Originals, 2019.
-
J. R. Hindley and J. P. Seldin Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, 2008.
-
S. Abramsky and B. Coecke. Categorical quantum mechanics. In Kurt Engesser, Dov Gabbay,
and Daniel Lehmann, editors, Handbook of Quantum Logic and Quantum Structures,
pages 261–324. North-Holland, Elsevier, 2011.
-
... other references will be suggested according to the lecturing scheduling.
Research blogs
- nLab -- A wiki-lab for collaborative work on Mathematics, Physics and Philosophy in so far as these subjects are usefully treated with tools and notions of category theory.
- Graphical Linear Algebra -- Pawel Sobocinski's blog about rediscovering linear algebra in a compositional way, with string diagrams.
- The n-Category Café -- A group blog on math, physics and philosophy.
Links
Pragmatics
Lecturer
Assessment
- Individual resolution of exercises along the semester and final written essay
- Exercise 1 (Exercise 11, Lecture 2 on functors): due 10 March
- Exercise 2 (Exercises 13 and 14, Lecture 3 on universal properties): due 30 March
- Exercise 3 (Exercises 15 and 17, Lecture 8 on string diagrams): due 30 May
- Written essay (research project): due 22 June
Contacts
- Lectures: T - Tuesday, 11-13 (Ed.3, 1.02)| TP Thursday 09-11 (Ed.1 1.22)
- Appointments: Wed, 18:00-20:00 (please send an email the day before)
- Email: lsb arroba di ponto uminho ponto pt
- Last update: 2022.05.23