Towards a Homotopy Domain Theory
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.
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.