弱约化的超发展
Superdevelopments for Weak Reduction
摘要：
我们研究了Cagman和Hindley的弱λ演算的超发展，这是标准弱λ演算的一个融合变体，其中禁止将λ演算还原到λ以下。与发展相反，从一个术语M的超发展不仅允许减少M中的赎回权的残差，而且还允许一些新创建的残差。在λ演算中，有三种方法可以创建新的redex;在弱λ演算中，一种新形式的redex创建是可能的。给出了弱λ演算超发展的标号约简公式和同时约简公式，并证明了它们的等价性.
英文摘要：
We study superdevelopments in the weak lambda calculus of Cagman and Hindley, a confluent variant of the standard weak lambda calculus in which reduction below lambdas is forbidden. In contrast to developments, a superdevelopment from a term M allows not only residuals of redexes in M to be reduced but also some newly created ones. In the lambda calculus there are three ways new redexes may be created; in the weak lambda calculus a new form of redex creation is possible. We present labeled and simultaneous reduction formulations of superdevelopments for the weak lambda calculus and prove them equivalent.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
