The $K_\infty$ Homotopy $λ$-Model
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
TL;DR
The paper addresses the problem that classical domain models like $D_∞$ yield trivial higher homotopy groups and thus collapse higher βη-conversions. It develops a Homotopy Domain Theory within Cartesian closed ∞-categories, introducing complete homotopy partial orders (CHPO) and the ∞-category CHPO, then constructs a nontrivial Kan complex $K_∞$ as a fixed point of an ω-continuous endofunctor using h-projection pairs. It proves that $K_∞$ is a nontrivial reflexive homotopy λ-model satisfying $K_∞\simeq [K_∞\rightarrow K_∞]$, and demonstrates a concrete interpretation in which the β-contraction and η-contraction are not equivalent, signaling nontrivial higher βη-conversions. The work thus provides a framework for nontrivial higher-order λ-calculus models based on homotopy-domain semantics and sets the stage for CHPO-based type theories with richer equality notions.
Abstract
We extend the complete ordered set Dana Scott's $D_\infty$ to a complete weakly ordered Kan complex $K_\infty$, with properties that guarantee the non-equivalence of the interpretation of some higher conversions of $βη$-conversions of $λ$-terms.