Conversão de Termos, Homotopia, e Estrutura de Grupóide
Resumo
A relação de conversão entre termos dada por Church, que determina a igualdade entre termos, diz que dois λ-termos são o mesmo se forem conversíveis um ao outro. Em outras palavras, um caminho entre dois termos, o que sugere a possibilidade de uma semântica com base em homotopia.
Palavras-chave:
Caminhos computacionais, Estrutura de Groupoide, Sistema de Reescrita, Homotopia
Referências
Awodey, S. (2010). Category theory. Oxford University Press.
Awodey, S. (2012). Type theory and homotopy. In Dybjer, P., Lindstrom, S., Palmgren, ¨ E., and Sundholm, G., editors, Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 183–201. Springer Netherlands.
Awodey, S. (2017). A proposition is the (homotopy) type of its proofs. arXiv:1701.02024.
de Oliveira, A. G. (1995). Proof transformations for labelled natural deduction via term rewriting. Master’s thesis. Depto. Informatica, UFPE, Recife, Brazil, April 1995.
de Oliveira, A. G. and de Queiroz, R. J. G. B. (1999). A normalization procedure for the equational fragment of labelled natural deduction. Logic J. of IGPL, 7(2):173–215.
de Queiroz, R. J. G. B. and de Oliveira, A. G. (1994). Term rewriting systems with labelled deductive systems. In Proc. Brazilian Symp. on Artif. Intellig., pages 59–72.
de Queiroz, R. J. G. B. and de Oliveira, A. G. (2014). Natural deduction for equality: The missing entity. In Pereira, L. C., Haeusler, E., and de Paiva, V., editors, Advances in Natural Deduction - A Celebration of Dag Prawitz’s Work, pages 63–91. Springer.
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 equa lity, identity types, and direct computational paths. South American Journal of Logic,2(2):245–296. Special Issue A Festschrift for Francisco Miraglia, M. E. Coniglio, H. L. Mariano and V. C. Lopes (Guest Editors).
de Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2018). On the calculation of fundamental groups in homotopy type theory by means of com putational paths. arXiv 1804.01413.
de 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.
Hindley, J. R. and Seldin, J. P. (2008). Lambda-calculus and combinators: an introduc tion. Cambridge University Press.
Hofmann, M. and Streicher, T. (1994). The groupoid model refutes uniqueness of identity proofs. In Logic in Computer Science, 1994. LICS’94. Proceedings., Symposium on, pages 208–212. IEEE.
Martınez-Rivillas, D. O. and de Queiroz, R. J. G. B. (2020). Towards a homotopy domain theory. arXiv:2007.15082.
Martınez-Rivillas, D. O. and de Queiroz, R. J. G. B. (2021). Solving homotopy domain equations. arXiv:2104.01195.
Martinez-Rivillas, D. O. and de Queiroz, R. J. G. B. (2021 (to appear) (preprint arXiv:1906.05729)). The groupoid generated by an arbitrary topological λ-model. Logic Journal of IGPL.
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 the IGPL, 25(4):562–584.
Ramos, A. F., de Queiroz, R. J. G. B., de Oliveira, A. G., and De Veras, T. M. L. (2018). Explicit computational paths. South American Journal of Logic, 4(2):441–484. Proceedings of the XVIII Brazilian Logic Conference.
Shulman, M. (2019). Homotopy type theory: a high-level language for invariant mathe matics. Slides from a colloquium talk at Indiana Univ, 2019.
Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.
Voevodsky, V. (2011). Univalent foundations of mathematics. In Beklemishev, L. D. and de Queiroz, R., editors, Logic, Language, Information, and Computation. 18th Inter national Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, Proceedings, volume 6642 of LNAI, page 4. Springer.
Awodey, S. (2012). Type theory and homotopy. In Dybjer, P., Lindstrom, S., Palmgren, ¨ E., and Sundholm, G., editors, Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 183–201. Springer Netherlands.
Awodey, S. (2017). A proposition is the (homotopy) type of its proofs. arXiv:1701.02024.
de Oliveira, A. G. (1995). Proof transformations for labelled natural deduction via term rewriting. Master’s thesis. Depto. Informatica, UFPE, Recife, Brazil, April 1995.
de Oliveira, A. G. and de Queiroz, R. J. G. B. (1999). A normalization procedure for the equational fragment of labelled natural deduction. Logic J. of IGPL, 7(2):173–215.
de Queiroz, R. J. G. B. and de Oliveira, A. G. (1994). Term rewriting systems with labelled deductive systems. In Proc. Brazilian Symp. on Artif. Intellig., pages 59–72.
de Queiroz, R. J. G. B. and de Oliveira, A. G. (2014). Natural deduction for equality: The missing entity. In Pereira, L. C., Haeusler, E., and de Paiva, V., editors, Advances in Natural Deduction - A Celebration of Dag Prawitz’s Work, pages 63–91. Springer.
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 equa lity, identity types, and direct computational paths. South American Journal of Logic,2(2):245–296. Special Issue A Festschrift for Francisco Miraglia, M. E. Coniglio, H. L. Mariano and V. C. Lopes (Guest Editors).
de Veras, T. M. L., Ramos, A. F., de Queiroz, R. J. G. B., and de Oliveira, A. G. (2018). On the calculation of fundamental groups in homotopy type theory by means of com putational paths. arXiv 1804.01413.
de 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.
Hindley, J. R. and Seldin, J. P. (2008). Lambda-calculus and combinators: an introduc tion. Cambridge University Press.
Hofmann, M. and Streicher, T. (1994). The groupoid model refutes uniqueness of identity proofs. In Logic in Computer Science, 1994. LICS’94. Proceedings., Symposium on, pages 208–212. IEEE.
Martınez-Rivillas, D. O. and de Queiroz, R. J. G. B. (2020). Towards a homotopy domain theory. arXiv:2007.15082.
Martınez-Rivillas, D. O. and de Queiroz, R. J. G. B. (2021). Solving homotopy domain equations. arXiv:2104.01195.
Martinez-Rivillas, D. O. and de Queiroz, R. J. G. B. (2021 (to appear) (preprint arXiv:1906.05729)). The groupoid generated by an arbitrary topological λ-model. Logic Journal of IGPL.
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 the IGPL, 25(4):562–584.
Ramos, A. F., de Queiroz, R. J. G. B., de Oliveira, A. G., and De Veras, T. M. L. (2018). Explicit computational paths. South American Journal of Logic, 4(2):441–484. Proceedings of the XVIII Brazilian Logic Conference.
Shulman, M. (2019). Homotopy type theory: a high-level language for invariant mathe matics. Slides from a colloquium talk at Indiana Univ, 2019.
Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.
Voevodsky, V. (2011). Univalent foundations of mathematics. In Beklemishev, L. D. and de Queiroz, R., editors, Logic, Language, Information, and Computation. 18th Inter national Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, Proceedings, volume 6642 of LNAI, page 4. Springer.
Publicado
18/07/2021
Como Citar
RAMOS, Arthur F.; QUEIROZ, Ruy J. G. B. de; OLIVEIRA, Anjolina G. de.
Conversão de Termos, Homotopia, e Estrutura de Grupóide. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 2. , 2021, Evento Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2021
.
p. 33-40.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2021.15776.
