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 program semantics as a (monoidal) category;
-
the specification of quantum algoritms and protocols in the (diagramatic) language of monoidal categories.
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.
Syllabus
- Module 1: The Curry-Howard-Lambek correspondence for classical and quantum computation.
- The Curry-Howard-Lambek isomorphism for intuitionistic logic.
- The Curry-Howard-Lambek isomorphism for linear logic.
- The Curry-Howard-Lambek isomorphism for quantum logic.
- Module 2: Specifying and reasoning about quantum programs in monoidal categories
- Monoidal categories and 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 ZX-calculus.
Summaries (2023-24)
T Lectures
| Feb 06 (11:00 - 13:00) |
Introduction to the course: objectives, learning outcomes, organisation. Logic and (quantum) computation.
|
| Feb 13 (11:00 - 13:00) |
CARNIVAL
|
| Feb 20 (11:00 - 13:00) |
Intuitionistic logic: formulae, sequents and proofs; natural deduction for intuitionistic logic; admissibility.
|
| Feb 27 (11:00 - 13:00) |
Untyped lambda-calculus:(untyped) terms; alpha-equivalence; substitution; beta-reduction.
|
| Mar 5 (11:00 - 13:00) |
Simply-typed lambda-calculus: types; (typed) terms; Curry-Howard-isomorphisms; beta-reduction; eta-reduction;
subject reduction; confluence; strong normalisation.
|
| Mar 12 (11:00 - 13:00) |
Category theory: categories; monos and epis; isomorphisms; initial and terminal objects; products;
exponents; functors; natural transformations.
|
| Mar 19 (11:00 - 13:00) |
Category theory (continued), categorical logic and intuitionistic linear logic: Yoneda lemma; adjoints; categorical semantics of simply-typed lambda calculus in Cartesian closed categories; soundness and completeness; intuitionistic linear logic.
|
| Apr 2 (11:00 - 13:00) |
Linear and quantum lambda-calculi and monoidal categories: linear and quantum lambda-calculi; symmetric monoidal closed categories; categorical semantics of linear and quantum lambda-calculi.
|
| Apr 9 (11:00 - 13:00) |
Linear and quantum lambda-calculi and monoidal categories: conclusion of the previous lecture. Closing of the course Module 1.
|
| Apr 16 (11:00 - 13:00) |
Introduction to module 2. Diagrams and categories. Diagramatic languages for processes.
Circuits [lecture notes].
String diagrams: definitions, examples, constructions [lecture notes].
|
| Apr 24 (16:00 - 18:00) |
The process theory of linear maps. Matricial representation. Completeness for string diagrams. [lecture notes] .(Room DI 1.20)
|
| Apr 30 (11:00 - 11:00) |
The process theory of pure quantum maps. Doubling to retrieve probabilities as scalars and get rid of global phases. [lecture notes] .
|
| May 14 (11:00 - 11:00) |
Quantum processes: adding discarding and non determinism. [lecture notes] .
|
TP Lectures
| Feb 06 (09:00 - 11:00) |
Premiliminaries on logic and quentum computation. |
| Feb 13 (09:00 - 11:00) |
CARNIVAL
|
| Feb 20 (09:00 - 11:00) |
Intuitionistic logic: how to write proofs in natural deduction; how to show the admissibility of a rule.
|
| Feb 27 (09:00 - 11:00) |
Untyped lambda-calculus: how to check if an expression is (not) a term; how to execute alpha-conversion and
beta-reduction.
|
| Mar 5 (09:00 - 11:00) |
Simply-typed lambda-calculus: how to construct a term; how to execute beta- and eta-reductions.
|
| Mar 12 (09:00 - 11:00) |
Category theory: how to prove that a concrete structure is a category; how to show that initial and
terminal objects as well as products are unique.
|
| Mar 19 (09:00 - 11:00) |
Category theory (continued), categorical logic and intuitionistic linear logic: how to interpret some concrete terms; how to prove that a concrete structure is an adjoint; how to prove that exponents are right adjoints to products.
|
| Apr 2 (09:00 - 11:00) |
Linear and quantum lambda-calculi and monoidal categories: how to write examples of linear and quantum terms; how to interpret examples of linear and quantum terms; how to prove an instance of a coherence theorem for monoidal categories.
|
| Apr 9 (09:00 - 11:00) |
Linear and quantum lambda-calculi and monoidal categories: conclusion of the previous lecture.
|
| Apr 16 (09:00 - 11:00) |
Exercises on circuits and string diagrams.
|
| Apr 23 (09:00 - 11:00) |
The ZX calculus [Wetering, 2020]
|
| Apr 30 (09:00 - 11:00) |
Exercises with linear maps
|
| May 14 (09:00 - 11:00) |
Exercises. Project review.
|
Support
Bibliography
-
A. Pitts. Categorical logic. in
Handbook of Logic in Computer Science (IV), Oxford University Press.
(pdf)
-
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.
(pdf)
-
P. Selinger Lecture Notes on the Lambda Calculus . 2013.
(link)
-
B. Coecke and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum
Theory and Diagrammatic Reasoning . Cambridge University Press, 2017.
Complementary Bibliography
-
A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2012.
-
C. Heunen and J. Vicary. Categories for Quantum Theory. Oxford Graduate Texts in Mathematics, 2019.
-
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.
-
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. (pdf)
-
... 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
Lecturers
Assessment
- Module 1: 6 take-home exercises (pdf) + 1 written essay
- Module 2: 2 take-home exercises (pdf) + 1 PyZX application essay
- Fianl grades (here)
Contacts
- Lectures: T - Tuesday, 11-13 (Building 2, 1.09)| TP Tuesday 09-11(Building 2, 2.04)
- Appointments (Luís): Wed, 18:00-20:00 (please send an email the day before)
- Email: lsb arroba di ponto uminho ponto pt
- Appointments (Nori): Wed, 15:30-17:30 (please send an email the day before)
- Email: norihiro1988 arroba gmail ponto com
- Last update: 2024.06.26