A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations
A Fine-Grained Notation for Lambda Terms and Its Use in Intensional Operations
复制标题
Lambda 项的细粒度表示法及其在内涵运算中的应用
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
G. Nadathur
中科院分区：
文献类型：
--
作者：
G. Nadathur
我们讨论了相关的实际使用的情况下，这些条款的内涵，必须操纵以前提出的符号lambda条款的问题。这种表示法使用de Bruijn的“无名”方案，包括用于编码术语的表达式以及对它们执行的替换，并包含用于组合这种替换的机制，以便它们可以在公共结构遍历中实现。组合机制是一种通用机制，因此很难实现。我们提出了一个简化，它保留其功能的情况下，通常发生在β还原。然后，我们描述了一个系统，用于注释术语，以确定它们是否会受到外部β收缩产生的替换的影响。这些注释可以通过允许在某些情况下简单地执行替换来节省约简实现中的空间和时间。使用由此产生的符号在减少和比较的条款进行检查。头部正规形式和头部减少序列的概念定义在其上下文中，并示出是有用的等式计算。我们的头减少序列概括了通常的lambda条款，使他们subconstitute的各种图形和环境为基础的减少程序的lambda演算产生的条款序列。因此，它们可以用于此类过程的正确性论证。这一事实和我们的符号的功效说明在我们提出的一个特定的还原过程的上下文中。本讨论的相关性的lambda项的统一也概述。
We discuss issues relevant to the practical use of a previously proposed notation for lambda terms in contexts where the intensions of such terms have to be manipulated. This notation uses the `nameless' scheme of de Bruijn, includes expressions for encoding terms together with substitutions to be performed on them and contains a mechanism for combining such substitutions so that they can be effected in a common structure traversal. The combination mechanism is a general one and consequently difficult to implement. We propose a simplification to it that retains its functionality in situations that occur commonly in beta reduction. We then describe a system for annotating terms to determine if they can be affected by substitutions generated by external beta contractions. These annotations can lead to a conservation of space and time in implementations of reduction by permitting substitutions to be performed trivially in certain situations. The use of the resulting notation in the reduction and comparison of terms is examined. Notions of head normal forms and head reduction sequences are defined in its context and shown to be useful in equality computations. Our head reduction sequences generalize the usual ones for lambda terms so that they subsume the sequences of terms produced by a variety of graph- and environment-based reduction procedures for the lambda calculus. They can therefore be used in correctness arguments for such procedures. This fact and the efficacy of our notation are illustrated in the context of a particular reduction procedure that we present. The relevance of the present discussions to the unification of lambda terms is also outlined.