A linearization of the Lambda-calculus and consequences
A linearization of the Lambda-calculus and consequences
复制标题
Lambda 演算的线性化和结果
DOI：
--
复制
发表时间：
1996
影响因子：
0.7
通讯作者：
A. Kfoury
中科院分区：
文献类型：
--
作者：
A. Kfoury
如果一个连续项M中的每一个连续抽象至多绑定一个变量出现，则称M是“线性的”。许多关于线性项的问题相对容易回答，例如它们都是β-强正规化的，并且都是简单类型的。我们将标准的可达演算L的语法扩展到满足线性条件的非标准可达演算L^，从而在标准情况下推广了该概念。具体地说，在L中，项M的子项Q可以应用于几个子项R1，.，Rk并行，我们写为（Q。R1楔形...楔形Rk）。对于微积分L^的β-归约β ^的适当概念是这样的，如果Q是λ-抽象（λ x.P），x的有界出现次数为mgeq 0，则可以在k = max（m，1）的条件下进行归约。因此，L^中的每个M都是β ^-SN。我们以几种不同的方式将标准β-归约和非标准β ^-归约联系起来，并得出几个结论，例如，一个新的简单证明，证明标准项M是β-SN当且仅当M可以被赋予一个所谓的"相交“类型（不允许”顶“类型）。
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 mgeq 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).