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

Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped gimel-abstractions (i.e. of the form gimelx : A. M); and domain-free systems with typed gimel-abstractions (i.e. of the form gimelx : A. M). Both flavours of systems are related by an erasure function \.\ that removes types from gimel-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 * : *. The gist of our argument is to exhibit a typable expression Y-H whose erasure \Y\ is a fixpoint combinator, but which is not a fixpoint combinator itself.