Title: A Linearization of the Lambda Calculus and Consequences
Author: A.J. Kfoury, Computer Science, Boston University
Date: August 19, 1996
Abstract:
If every lambda-abstraction in a lambda-term M binds at most one
variable occurrence, then M is said to be "linear". Many questions
about linear lambda-terms are relatively easy to answer, e.g.
they all are beta-strongly normalizing and all are simply-typable.
We extend the syntax of the standard lambda-calculus L to a non-standard
lambda-calculus L^ satisfying a linearity condition generalizing the
notion in the standard case. Specifically, in L^ a subterm Q of a term
M can be applied to several subterms R1,...,Rk in parallel, which we
write as (Q. R1 \wedge ... \wedge Rk). The appropriate notion of beta-
reduction beta^ for the calculus L^ is such that, if Q is the lambda-
abstraction (\lambda x.P) with m\geq 0 bound occurrences of x, the
reduction can be carried out provided k = max(m,1). Every M in L^ is
thus beta^-SN. We relate standard beta-reduction and non-standard
beta^-reduction in several different ways, and draw several consequences,
e.g. a new simple proof for the fact that a standard term M is beta-SN
iff M can be assigned a so-called ``intersection'' type (``top'' type
disallowed).