• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >A Syntactical Analysis of Normalization
【24h】

A Syntactical Analysis of Normalization

机译：归一化的句法分析

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Some λ-terms exhibit the following alternation property: whenever a redex having the shape (λx.P)(λy.Q) is created in a reduction path starting with the contraction of M N, then either λx appears in M and λy in N, or λx appears in N and λy in M. In this paper, we investigate the alternation property and we establish its relevance in the context of typed caculi. In particular, we prove that the alternation property implies normalization. To this aim, we use a simple technique based on labels. The intended meaning of the labelling is to give information about the minimal number of contractions needed by a variable to be substituted during the reduction process. Further, we apply this result to obtain new normalization proofs for Curry's simply typed lambda calculus and, similarly, for terms typable with intersection types.
机译：一些λ项表现出以下交替性质：每当从MN的收缩开始在还原路径中创建形状为（λx.P）（λy.Q）的redex时，则λx出现在M中，而λy出现在N中，或λx出现在N处，而λy出现在M处。在本文中，我们研究了交替性质，并在类型化的轻晶下建立了它的相关性。特别是，我们证明了交替属性暗示着归一化。为此，我们使用了一种基于标签的简单技术。标记的预期含义是提供有关在还原过程中要替换的变量所需的最小收缩次数的信息。此外，我们将这个结果应用于针对Curry的简单类型的lambda演算以及类似地可用于交集类型的项的新归一化证明。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号