dc.contributor.author Kfoury, A.J. en_US dc.date.accessioned 2011-10-20T04:37:41Z dc.date.available 2011-10-20T04:37:41Z dc.date.issued 1996-08-19 en_US dc.identifier.citation Kfoury, A.J.. "A Linearization of the Lambda Calculus and Consequences", Technical Report BUCS-1996-021, Computer Science Department, Boston University, August 19, 1996. [Available from: http://hdl.handle.net/2144/1597] en_US dc.identifier.uri https://hdl.handle.net/2144/1597 dc.description.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). en_US dc.description.sponsorship National Science Foundation (CCR-9417382) en_US dc.language.iso en_US en_US dc.publisher Boston University Computer Science Department en_US dc.relation.ispartofseries BUCS Technical Reports;BUCS-TR-1996-021 en_US dc.title A Linearization of the Lambda-Calculus and Consequences en_US dc.type Technical Report en_US
﻿