Show simple item record

dc.contributor.authorKfoury, A.J.en_US
dc.date.accessioned2011-10-20T04:37:41Z
dc.date.available2011-10-20T04:37:41Z
dc.date.issued1996-08-19en_US
dc.identifier.citationKfoury, 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.urihttps://hdl.handle.net/2144/1597
dc.description.abstractIf 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.sponsorshipNational Science Foundation (CCR-9417382)en_US
dc.language.isoen_USen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-1996-021en_US
dc.titleA Linearization of the Lambda-Calculus and Consequencesen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record