|
Assaf J. Kfoury
A linearization of the
lambda-calculus
J. Logic Comput., 10(3):411-436, 2000
Special issue on Type Theory and Term Rewriting. Kamareddine and Klop
(editors)
We embed the standard lambda-calculus, denoted Lambda,
into two larger lambda-calculi,
denoted Lambda/\ and &Lambda/\.
The standard notion of beta-reduction for Lambda
corresponds to two new notions of reduction,
beta/\ for Lambda/\ and
&beta/\ for &Lambda/\. A distinctive
feature of our new calculus Lambda/\
(resp., &Lambda/\) is that, in every function
application, an argument is used at most once (resp.,
exactly once) in the body of the function. We establish
various connections between the three notions of reduction,
beta, beta/\ and &beta/\. As a
consequence, we provide an alternative framework to study
the relationship between beta-weak normalization and
beta-strong normalization, and give a new proof of the
oft-mentioned equivalence between beta-strong
normalization of standard lambda-terms and typability in
a system of “intersection types''.
[ bib |
.ps.gz |
.pdf.gz |
.pdf |
.html ]
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.
|
