Perpetuality in a named lambda calculus with explicit substitutions
Perpetuality in a named lambda calculus with explicit substitutions
复制标题
具有显式替换的命名 lambda 演算中的永续性
DOI：
10.1017/s0960129500003248
复制
发表时间：
2001
影响因子：
0.5
通讯作者：
E. Bonelli
中科院分区：
文献类型：
--
作者：
E. Bonelli
我们研究显式替换λx演算中的永久性。如果一个约简保持了无穷约简序列的可能性，则它被称为永久约简。然后，我们看看这项研究的应用：λ x-强正规化项的归纳特征，λx的两个永久约简策略，最后证明了具有显式替换Fes的多态lambda演算的强正规化。为了完成研究的Fes，属性的主题减少持有扩展类型分配的类型规则，以允许非纯类型（类型与可能发生的类型替换运算符）。
We study perpetuality in the calculus of explicit substitutions λx. A reduction is called perpetual if it preserves the possibility of infinite reduction sequences. We then take a look at applications of this study: an inductive characterization of the λx-strongly normalizing terms, two perpetual reduction strategies for λx and finally a proof of strong normalization of a polymorphic lambda calculus with explicit substitutions Fes. To complete the study of Fes, the property of subject reduction is shown to hold by extending type assignments of the typing rules to allow non-pure types (types with possible occurrences of the type substitution operator).