Calculation of Fundamental Groups via Computational Paths
ResumoWe 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.
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.