Departamento de Informática (UM)

Lógica Quântica

14924 [ME80ME8002006774]

Mestrado em Engenharia Física [MEF]

S2

Luís Manuel Dias Coelho Soares Barbosa

Objetivos

Tratando-se de uma Unidade Curricular dedicada aos fundamentos logico-matemáticos da Computação Quântica, o programa proposto cobre com detalhe os conceitos e resultados base na área em linha com o que é ensinado em cursos similares noutras Universidades europeias. Uma atenção particular é dada à introdução à teoria das categorias monoidais que constitui a ferramenta base de trabalho e, infelizmente ainda não faz parte da formação base em matemática no 1º ciclo. De facto, o papel desempenhado pela teoria das categorias é tão fundamental que se justifica inteiramente o espaço (cerca de um terço) do esforço lectivo. O curso inclui um tópico de aplicações da semântica à especificação e verificação de programas, com suporte computacional, que visa operacionalizar os conceitos, resultados e técnicas estudados.

Programa

1. Fundamentos: modelos semânticos categoriais
a. Revisão da noção de categoria, functor, transformação natural, limites e colimites
b. Propriedades universais e adjunções
c. Categorias monoidais. Aplicações: (categorias de) relações, matrizes e espaços de Hilbert
2. Lógicas computacionais e semântica para a computação quântica
a. O que é uma lógica? Lógica e computação: lógica intuicionista, modal e linear
b. Interpretação computacional dos postulados básicos da mecânica quântica; Estruturas categoriais correspondentes: monoidal (composição), compacta fechada (entanglement), adjunções (produto interno), biprodutos (ramificação não determinística)
c. O lambda-calculus linear e a correspondência de Curry-Howard-Lambek para a computação quântica. Variantes
d. Raciocínio diagramáticos para a derivação e modelação de algoritmos quânticos
e. Modelação e verificação de algoritmos quânticos; ferramentas

Bibliografia

Livros
Heunen, C., Vicary, J. (2019). Categories for Quantum Theory: An Introduction. Oxford Graduate Texts in Mathematics.

Coecke, B., Kissinger, A. (2017). Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press.

Awodey, S. (2006). Category Theory. Oxford: Claredon Press.

Outros Textos
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.

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.

Resultados da aprendizagem

O desenvolvimento da informação e computação quânticas requer ferramentas formais que permitam raciocinar rigorosamente sobre sistemas quânticos. Esta unidade curricular explora a ligação entre a computação (quântica) e as lógicas (sensíveis aos recursos) dada pela correspondência de Curry-Howard-Lambek — que identifica proposições com tipos e provas com programas — e a ligação à semântica formalizada como uma categoria (monoidal).
Assim, no final, os alunos serão capazes de:
1. Aplicar ao desenvolvimento de programas quânticos um conhecimento sólido e operativo em semântica da programação quântica e cálculos de programas no paradigma quântico
2. Dominar os fundamentos, métodos e ferramentas para a especificação e verificação de programas quânticos

Método de avaliação

• Apresentação e discussão em grupo de um estudo de caso (15%)
• Desempenho nas aulas teórica-práticas (15%)
• Teste escrito (70%)

Funcionamento

Turno: T 1; Docente: Luís Manuel Dias Coelho Soares Barbosa; Dep.: DI; Horas: 30.
Turno: TP 1; Docente: Norihiro Yamada; Dep.: DI; Horas: 30.