The $K_\infty$ Homotopy $\lambda$-Model

TL;DR

This paper extends Dana Scott's $D_ Infty$ to a new model $K_ Infty$, providing a framework that distinguishes certain higher-order $eta ext{eta}$-conversions of $ lambda$-terms.

Contribution

It introduces the $K_ Infty$ homotopy $ lambda$-model, a novel extension with properties that differentiate higher conversions.

Findings

$K_ Infty$ is a complete weakly ordered Kan complex.

The model guarantees non-equivalence of some higher $eta ext{eta}$-conversions.

It provides a new semantic framework for analyzing $ lambda$-term conversions.

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 $\beta\eta$-conversions of $\lambda$-terms.