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. |