Calculation of Fundamental Groups via Computational Paths
Resumo
We address the question as to how to formalise the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. The intention is to demonstrate the use of a term rewriting system in performing computations with these computational paths, establishing equalities between equalities, and further higher equalities, in particular, in the calculation of fundamental groups of surfaces such as the circle, the torus and the real projective plane.
Palavras-chave:
fundamental groups, type theory, computational paths, identity type
Referências
de Oliveira, A. G. (1995). Proof transformations for labelled natural deduction via term rewriting. Master’s thesis, Informa ́tica, UFPE, Recife, Brazil, April 1995.
de Queiroz, R. J. G. B., de Oliveira, A. G., and Gabbay, D. M. (2011). The Functional Interpretation of Logical Deduction. World Scientific.
de Queiroz, R. J. G. B., de Oliveira, A. G., and Ramos, A. F. (2016). Propositional equality, identity types, and direct computational paths. Sth Am.J.Log., 2(2):245–96.
de Queiroz, R. J. G. B. and Gabbay, D. M. (1994). Equality in labelled deductive systems and the functional interpretation of propositional equality. In Proc. 9th Amsterdam Coll., pages 547–565. ILLC/Dept of Phil. Univ Amsterdam.
Martin-Lo ̈f, P. (1975). An intuitionistic theory of types: Predicative part. In Rose, H. and Shepherdson, J., editors, Proc. Logic Colloquium ’73, pages 73 – 118. Elsevier.
Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2017). On the identity type as the type of computational paths. Logic Journal of IGPL, 25(4):562–584.
Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2019). A topological application of labelled natural deduction. arXiv:1906.09105.
Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., Silva, T. D. O., and de Oliveira, A. G. (2020). Computational paths – a weak groupoid. arXiv: 2007.07769.
de Queiroz, R. J. G. B., de Oliveira, A. G., and Gabbay, D. M. (2011). The Functional Interpretation of Logical Deduction. World Scientific.
de Queiroz, R. J. G. B., de Oliveira, A. G., and Ramos, A. F. (2016). Propositional equality, identity types, and direct computational paths. Sth Am.J.Log., 2(2):245–96.
de Queiroz, R. J. G. B. and Gabbay, D. M. (1994). Equality in labelled deductive systems and the functional interpretation of propositional equality. In Proc. 9th Amsterdam Coll., pages 547–565. ILLC/Dept of Phil. Univ Amsterdam.
Martin-Lo ̈f, P. (1975). An intuitionistic theory of types: Predicative part. In Rose, H. and Shepherdson, J., editors, Proc. Logic Colloquium ’73, pages 73 – 118. Elsevier.
Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2017). On the identity type as the type of computational paths. Logic Journal of IGPL, 25(4):562–584.
Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2019). A topological application of labelled natural deduction. arXiv:1906.09105.
Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., Silva, T. D. O., and de Oliveira, A. G. (2020). Computational paths – a weak groupoid. arXiv: 2007.07769.
Publicado
18/07/2021
Como Citar
VERAS, T. M. L. de; RAMOS, A. F.; QUEIROZ, R. J. G. B. de; OLIVEIRA, A. G. de.
Calculation of Fundamental Groups via Computational Paths. In: ENCONTRO DE TEORIA DA COMPUTAÇÃO (ETC), 6. , 2021, Evento Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2021
.
p. 17-21.
ISSN 2595-6116.
DOI: https://doi.org/10.5753/etc.2021.16370.
