## A Linearization of the Lambda-Calculus and Consequences

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 | |

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] | |

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 | |

dc.publisher | Boston University Computer Science Department | en_US |

dc.relation.ispartofseries | BUCS Technical Reports;BUCS-TR-1996-021 | |

dc.title | A Linearization of the Lambda-Calculus and Consequences | en_US |

dc.type | Technical Report | en_US |

### This item appears in the following Collection(s)