Towards a homotopy domain theory

Detalhes bibliográficos
Ano de defesa: 2022
Autor(a) principal: RIVILLAS, Daniel Orlando Martínez
Orientador(a): QUEIROZ, Ruy José Guerra Barretto
Banca de defesa: Não Informado pela instituição
Tipo de documento: Tese
Tipo de acesso: Acesso aberto
Idioma: eng
Instituição de defesa: Universidade Federal de Pernambuco
Programa de Pós-Graduação: Programa de Pos Graduacao em Ciencia da Computacao
Departamento: Não Informado pela instituição
País: Brasil
Palavras-chave em Português:
Link de acesso: https://repositorio.ufpe.br/handle/123456789/49221
Resumo: Solving recursive domain equations over a Cartesian closed 0-category is a way to find extensional models of the type-free λ-calculus. In this work we seek to generalize these equa- tions to “homotopy domain equations”; to be able to set about a particular Cartesian closed “(0,∞)-category”, which we call the Kleisli ∞-category, and thus find higher λ-models, which we call “λ-homotopic models”. To achieve this purpose, we had to previously generalize c.p.o’s (complete partial orders) to c.h.p.o’s (complete homotopy partial orders); complete ordered sets to complete (weakly) ordered Kan complexes, 0-categories to (0,∞)-categories and the Kleisli bicategory to a Kleisli ∞-category. Continuing with the semantic line of λ-calculus, the syntactical λ-models (e.g., the set D∞), defined on sets, are generalized to “homotopic syntactical λ-models” (e.g., the Kan complex “K∞”), which are defined on Kan complexes, and we study the relationship of these models with the homotopic λ-model. Finally, from the syntactic point of view, what the theory of an arbitrary homotopic λ-model would be like is explored, which turns out to contain a theory of higher λ-calculus, which we call Homotopy Type-Free Theory (HoTFT); with higher βη-contractions and thus with higher βη-conversions.