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
Sitemap
To content Read more about how we use cookies on gu.se

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
Links dx.doi.org/10.1017/S095679680300472...
Subject categories

Abstract

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
Share:

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?