Peter Møller Neergaard and Morten Heine B.
Sørensen
Conservation and
uniform normalization in lambda-calculi with erasing
reductions
Information and Computation, 178(1):149-179, October 2002
(c)This paper is Copyright Elsevier.
For a notion of reduction in a lambda-calculus
one can ask whether a term satisfies
conservation and uniform
normalization. Conservation means that single-step
reductions of the term preserve infinite reduction
paths from the term. Uniform normalization means
that either the term will have no reduction paths
leading to a normal form, or all reduction paths
will lead to a normal form. In the classical
conservation theorem for LambdaI the
distinction between the two notions is not clear:
uniform normalization implies conservation, and
conservation also implies uniform normalization. The
reason for this is that LambdaI is closed under
reduction, due to the fact that reductions never
erase terms in LambdaI. More generaly for
non-erasing reductions, the two notions are
equivalent on a set closed under reduction. However,
when turning to erasing reductions the distinction
becomes important as conservation no longer implies
uniform normalization.
This paper presents a
new technique for finding uniformly normalizing
subsets of a lambda-calculus. This is done by
combining a syntactic and a semantic criterion. The
technique is demonstrated by several
applications. The technique is used to present a new
uniformly normalizing subset of the pure
lambda-calculus; this subset is a superset
of LambdaI and thus contains erasing
K-redexes. The technique is also used to
prove strong normalization from weak normalization
of the simply typed lambda-calculus extended with
pairs; this is an extension of techniques developed
recently by Sørensen and Xi. Before presenting
the technique the paper presents a simple proof of a
slightly weaker form of the characterization of
perpetual redexes by Bergstra and Klop; this is a
stepping for the later applications of the
technique.
[ bib |
.ps.gz |
.pdf.gz |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
