Pós-Graduação em Ciência da Computação – UFPE
Defesa de Tese de Doutorado Nº 585
Aluno: Daniel Orlando Martínez Rivillas
Orientador: Prof. Ruy José Guerra Barretto de Queiroz
Título: Towards a Homotopy Domain Theory
Data: 15/12/2022
Hora/Local: 10h – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinadora:
Prof. Edward Hermann Haeusler (PUC/RJ/Departamento de Informática)
Prof. Benjamin René Callejas Bedregal (UFRN/ Depto de Informática e Matemática Aplicada)
Profa. Alejandra Martins da Silva Depto. de Ciência da Computação / Cornell Universit)
Prof. António Mário da Silva Marcos Florido (Universidade do Porto/Depto de Ciência de Computadores)
Prof. Dr. Hugo Luiz Mariano (USP / Instituto de Matemática e Estatística)
RESUMO:
A resolução das equações de domínio recursivas sobre uma 0-categoria Cartesiana fechada
é uma maneira de encontrar modelos extensionais do 𝜆-cálculo com Type-free. Neste trabalho
buscamos generalizar estas equações para “equações de domínio de homotopia”; definidas sobre uma determinada “(0, ∞)-categoria” fechada Cartesiana, que chamamos de Kleisli ∞-category, e assim encontrar 𝜆-modelos superiores, que nós chamar “𝜆-modelos ho-motópicos”. Para atingir este propósito, tivemos que generalizar previamente c.p.o’s (ordens
parciais completos) para c.h.p.o’s (ordens parciais de homotopia completos); conjuntos or-
denados completos para complexos de Kan ordenados (fracamente) completos, 0-categorias
para (0, ∞)-categorias e a bicategoria Kleisli para uma Kleisli ∞-categoria. Continuando com
a linha semântica de 𝜆-cálculo, os 𝜆-modelos sintáticos (e.g., o conjunto 𝐷∞ ), definidos sobre
conjuntos, são generalizados para “𝜆-modelos sintáticos homotópicos” (e.g., o complexo de
Kan “𝐾∞ “), que são definidos em complexos de Kan, e estudamos a relação desses modelos
com os 𝜆-modelos homotópicos. Finalmente, do ponto de vista sintático, explora-se como seria
a teoria de um 𝜆-modelo arbitrário, que acaba por conter uma teoria de 𝜆-cálculo superior,
a qual chamamos Teoria não-tipada de Homotopia; com 𝛽𝜂-contrações superiores e daí com
𝛽𝜂-conversões superiores.
Palavras-chave: Complexo de Kan fracamente ordenado. Ordem parcial de homotopia completo. 𝜆-Modelo sintáctico homotópico. 𝜆-Modelo homotópico . Equação de domínio de homotopia. Teoria no-tipada de homotopia.
Comentários desativados