To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Remarks on the equational… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

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

Journal article
Authors G. Barthe
Thierry Coquand
Published in Journal of Functional Programming
Volume 16
Issue 2
Pages 137-155
ISSN 09567968 (ISSN)
Publication year 2006
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 137-155
Language en
Subject categories


Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped λ-abstractions (i.e. of the form λx. M); and domain-free systems with typed λ-abstractions (i.e. of the form λx :A. M). Both flavours of systems are related by an erasure function |.| that removes types from λ-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 YH whose erasure |Y| is a fixpoint combinator, but which is not a fixpoint combinator itself.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?