The Theory of an Arbitrary Higher $\lambda$-Model

Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz

One takes advantage of some basic properties of every $\lambda$-homotopic model (e.g.\ reflexive Kan complex) to explore two types of higher $\beta\eta$-conversions: the first, from the higher $\beta\eta$-contractions (we denoted those by $(n+1)$-$\beta\eta$-contractions) of a lower $\beta\eta$-conversion. Second, starting from the classical conversions, $\lambda^n$-terms are introduced inductively by application and abstraction of lower $\beta\eta$-conversions, to get other types of higher $\beta\eta$-contractions (we denoted those by $(\beta\eta)_{n+1}$-contractions) between those $\lambda^n$-terms already defined.

picture_as_pdf flag

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment