Fundamentos Homotópicos

Prévia do material em texto

Fundamentos Homotópicos da Teoria da
Computação
Pré-Projeto de Mestrado
Orientador: Ruy José Guerra B. de Queiroz
Descrição
Uma ampla frente de pesquisa nos fundamentos da matemática começou a ser explo-
rada em 2005 por matemáticos como Vladimir Voevodsky (Medalha Fields, 2002)
(falecido em 2017) e Steve Awodey na tentativa de construir uma ponte entre a te-
oria construtiva de tipos de Per Martin-Löf (1973) e a teoria da homotopia, princi-
palmente através da estrutura de grupóide revelada no contramodelo de Hofmann–
Streicher (1994) ao princı́pio da Unicidade de Provas de Identidade (UIP). Isso tem
aberto caminho para, nas palavras de Awodey, “uma nova e surpreendente conexão en-
tre Geometria, Álgebra, e Lógica, que tem vindo à tona recentemente na forma de uma
interpretação da teoria construtiva de tipos de Per Martin-Löf na teoria da homotopia,
resultando em novos exemplos de certas estruturas algébricas que são importantes em
topologia”[Awodey].
Motivados por um olhar sobre as igualdades em teoria de tipos como surgindo da
existência de caminhos computacionais entre dois objetos formais, nosso propósito é
oferecer uma nova perspectiva sobre o papel e o poder da noção de igualdade proposi-
cional tal qual formalizada na chamada interpretação funcional de Curry–Howard [Ra-
mosPhD, RdeQdeO, RdeQdeO2, RdeQdeO3, deQdeO]. Em trabalhos recentes, usamos
essa abordagem dos caminhos computacionais para construir o espaço de caminhos dos
números naturais, assim como para calcular o grupo fundamental de estruturas como o
cı́rculo, o torus, o cilindro, o plano projetivo, a fita de Möbius [DeV1,DeV2,DeV3], e
a garrafa de Klein. Engajado em uma linha de pesquisa no mesmo espı́rito que o pro-
grama de Voevodsky e Awodey, buscamos revisitar os métodos clássicos de cálculo de
grupos de homotopia (a saber, os teoremas de Seifert–VanKampen, Hurewicz, Blaker–
Massey, o teorema da suspensão de Freudenthal, assim como o método da sequen-
cia exata longa de grupos de homotopia de uma fibração), de modo a encontrar uma
formulação mais alinhada com as técnicas desenvolvidas no contexto da teoria cons-
trutiva de tipos.
Numa outra vertente do projeto de buscar as conexões entre a teoria construtiva
de tipos e a teoria da homotopia, a ideia é encontrar uma generalização da teoria de
domı́nios de Dana Scott (que provê fundamentos topológicos à noção de função com-
putável) de tal forma que a estrutura básica seria a de ∞-grupóides ao invés de complete
partial orders (cpo), e para isso está em construção um framework apropriado para a
construção de modelos do λ-cálculo com estrutura de ∞-grupóides, que são chamados
de modelos λ-homotópicos através do uso de ∞-categorias de complexos de Kan com
fecho cartesiano e uma quantidade suficiente de pontos [MartinezPhD,MartinezdeQ1,
MartinezdeQ2,MartinezdeQ3,MartinezdeQ4].
Referências Bibliográficas:
[Awodey] Awodey, Steve (2012). “Type theory and homotopy”. In Dybjer, P.; Lindström,
Sten; Palmgren, Erik; et al. Epistemology versus Ontology. Logic, Epistemology, and
the Unity of Science. Springer. pp. 183–201. doi:10.1007/978-94-007-4435-6 9. ISBN
978-94-007-4434-9.
[Hofmann–Streicher94]. Hofmann, Martin; Streicher, Thomas (1994). “The groupoid
model refutes uniqueness of identity proofs”. In LICS’94, pp. 208–212
[Hofmann–Streicher98]. Hofmann, Martin; Streicher, Thomas (1998). “The groupoid
1
Ms.C Emmanuel Lins
Ms.C Emmanuel Lins
Ms.C Emmanuel Lins
interpretation of type theory”. In Sambin, G.; Smith, J.M. Twenty Five Years of Cons-
tructive Type Theory. Clarendon Press. pp. 83–112. ISBN 978-0-19-158903-4.
[MartinezPhD] Martı́nez-Rivillas, D.O. 2022. Towards a homotopy domain theory.
PhD thesis, Centro de Informática, UFPE (November 2022). Centro de Informática,
Universidade Federal de Pernambuco, Recife, Brazil.
https://repositorio.ufpe.br/handle/123456789/49221
[MartinezdeQ1] Martı́nez-Rivillas, D.O., de Queiroz, R.J.G.B. Towards a homotopy
domain theory. Arch. Math. Logic 62, 559–579 (2023).
https://doi.org/10.1007/s00153-022-00856-0
[MartinezdeQ2] Martnez-Rivillas, Daniel O., de Queiroz, R. J. G. B. The ∞-groupoid
generated by an arbitrary topological λ-model. Logic Journal of the IGPL, Volume
30, Issue 3, June 2022, Pages 465–488, https://doi.org/10.1093/jigpal/jzab015. Also
1906.05729, Jul 2019 (current version: May 2020).
[MartinezdeQ3] Martnez-Rivillas, Daniel O., de Queiroz, R. J. G. B. Solving Homo-
topy Domain Equations. Apr 2021. https://arXiv:2104.01195 .
[MartinezdeQ4] Martı́nez-Rivillas, D. O., & de Queiroz, R. J. G. B. (2023). The The-
ory of an Arbitrary Higher λ-Model. Bulletin of the Section of Logic, 52(1), 39–58,
2023. https://doi.org/10.18778/0138-0680.2023.11.
[deQdeO]. Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira, Arthur Ramos. Propositi-
onal equality, identity types, and direct computational paths. South American Journal
of Logic, 2:245–296, 2016. Also arXiv:1107.1901v3, Jul 2011 (current version: Aug
2013), https://arxiv.org/abs/1107.1901.
[RamosPhD] Ramos, A.F. 2018. Explicit computational paths in type theory. PhD
thesis, CIn-UFPE (August 2018). Centro de Informática, Universidade Federal de Per-
nambuco, Recife, Brazil.
https://repositorio.ufpe.br/handle/123456789/32902 (Abstract in: Ramos, A. (2019).
Explicit Computational Paths in Type Theory.
[RdeQdeO]. Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oli-
veira. Computational Paths and Identity Types. arXiv:1609.05079, September 2016,
https://arxiv.org/abs/1609.05079.
[RdeQdeO2]. Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira.
On the identity type as the type of computational paths. Logic Journal of the IGPL
25(4):562–584, 2017.
[RdeQdeO3]. Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira,
Tiago M. L. de Veras. Explicit Computational Paths. South American Journal of Logic
4(2):441–484, 2018.
[DeV1] de Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira,
A. G. On the calculation of fundamental groups in homotopy type theory by means of
computational paths. April 2018. https://arxiv.org/abs/1804.01413.
[DeV2] de Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A.
G. A Topological Application of Labelled Natural Deduction. Jun 2019. To appear in
South American Journal of Logic. https://arxiv.org/abs/1906.09105.
[DeV3] de Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira,
A. G. Computational Paths – A Weak Groupoid. Journal of Logic and Computa-
tion, exad071, https://doi.org/10.1093/logcom/exad071 Published: 24 November 2023.
Also arXiv:1906.09105.
2