λ演算的Letrec表示
Expressibility in the Lambda Calculus with Letrec
摘要：
我们调查之间的关系，有限项的Lenda-letrec，与letrec的λ演算，和无限的lambda条款，他们表示。由于有一些简单的例子，λ-项，直观上，是不是展开的条款在λ-letrec，我们考虑的问题：如何可以这些无限的lambda条款的特点是λ-letrec-表达的意义上，他们可以获得无限展开的条款在λ-letrec？为了通过在项的头部进行的重复“实验”来“观察”无限的子项，我们引入了两个重写系统（具有重写关系）-reg->和-reg+->，它们分解项，并在两个概念中产生“生成的子项”。因此，可以观察步骤的种类以及其目标，生成的子项。在这两个系统中，都有四种分解步骤：-lambda-> steps（分解一个抽象），-@0>和-@1> steps（将应用程序分解为它的函数和参数），以及-del-> steps（定义抽象的作用域，对于-reg->）和-S->（定义作用域，对于-reg+->）。这些步骤发生在无限的抽象项上，这些抽象项带有一个前导前缀，用于收集以前遇到的抽象项，并保持生成的子项关闭。我们称一个无限的可达项为“正则”/“强正则”，如果它的-reg-> -reachable / -reg-> -reachable生成子项的集合是有限的。此外，我们还用“结合-捕获链”的概念分析了非线性项的结合结构。使用这些概念，我们回答了上面的问题，提供两个特征的可表达性。对所有无穷多项M，下列陈述是等价的：（i）M是可表示的;（ii）M是强正则的;（iii）M是正则的，并且它只有有限的结合-捕获链。
英文摘要：
We investigate the relationship between finite terms in lambda-letrec, the lambda calculus with letrec, and the infinite lambda terms they express. As there are easy examples of lambda-terms that, intuitively, are not unfoldings of terms in lambda-letrec, we consider the question: How can those infinite lambda terms be characterised that are lamda-letrec-expressible in the sense that they can be obtained as infinite unfoldings of terms in lambda-letrec? For 'observing' infinite lambda-terms through repeated 'experiments' carried out at the head of the term we introduce two rewrite systems (with rewrite relations) -reg-> and -reg+-> that decompose the term, and produce 'generated subterms' in two notions. Thereby the sort of the step can be observed as well as its target, a generated subterm. In both systems there are four sorts of decomposition steps: -lambda-> steps (decomposing a lambda-abstraction), -@0> and -@1> steps (decomposing an application into its function and argument), and respectively, -del-> steps (delimiting the scope of an abstraction, for -reg->), and -S-> (delimiting of scopes, for -reg+->). These steps take place on infinite lambda-terms furnished with a leading prefix of abstractions for gathering previously encountered lambda-abstractions and keeping the generated subterms closed. We call an infinite lambda-term 'regular'/'strongly regular' if its set of -reg-> -reachable / -reg-> -reachable generated subterms is finite. Furthermore, we analyse the binding structure of lambda-terms with the concept of 'binding-capturing chain'. Using these concepts, we answer the question above by providing two characterisations of lambda-letrec-expressibility. For all infinite lambda-terms M, the following statements are equivalent: (i) M is lambda-letrec-expressible; (ii) M is strongly regular; (iii) M is regular, and it only has finite binding-capturing chains.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
