Remarks on the equational theory of non-normalizing pure type systems

Abstract

Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped $\lambda$ -abstractions (i.e. of the form $\lambda{x}.{M}$ ); and domain-free systems with typed $\lambda$ -abstractions (i.e. of the form $\lambda{x}{A}{M}$ ). Both flavours of systems are related by an erasure function $\er{.}$ that removes types from $\lambda$ -abstractions. Preservation of Equational Theory , which states the equational theories of both systems coincide through the erasure function, is a property of functional and normalizing PTSs. In this paper we establish that Preservation of Equational Theory fails for some non-normalizing PTSs, including the PTS with $\ast:\ast$. The gist of our argument is to exhibit a typable expression $Y_H$ whose erasure $\er{Y}$ is a fixpoint combinator, but which is not a fixpoint combinator itself.