Viewing λ-terms through Maps
Viewing λ-terms through Maps
复制标题
通过地图查看 λ 项
DOI：
10.1016/j.indag.2013.08.003
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
T. Sakurai
中科院分区：
文献类型：
--
作者：
M. Sato;R. Pollack;H. Schwichtenberg;T. Sakurai
在本文中，我们介绍了映射的概念，它是语法表达式（例如公式或 λ 项）中符号出现的集合的表示法。我们使用 0 和 1 上的二叉树作为映射，但需要一些格式良好的条件。我们使用映射开发 lambda 项的表示。该表示是具体的（可在 HOL 或构造类型理论中归纳定义）和规范的（每个 λ 项有一个代表）。我们定义了映射表示的替换，并证明该表示在替换中与名义逻辑 λ 项和 de Bruijn 无名项保持同构。这些证明分别在 Isabelle/HOL 和 Minlog 中进行机械检查。地图表示具有良好的属性。替换不需要调整结合信息：既不需要被替换的身体的α转换，也不需要被植入的术语的de Bruijn提升。我们有 λ 演算的替换引理的自然证明，不需要新名称或索引操作。使用映射的概念，我们研究传统的原始 λ 语法。例如，我们给出并证明了正确的原始 λ 项的 α 等价性决策过程，不需要新名称。我们最后给出了地图术语 β 约简的定义、对我们当前工作局限性的一些讨论以及对未来工作的建议。
In this paper we introduce the notion of map, which is a notation for the set of occurrences of a symbol in a syntactic expression such as a formula or a λ term. We use binary trees over 0 and 1 as maps, but some well-formedness conditions are required. We develop a representation of lambda terms using maps. The representation is concrete (inductively definable in HOL or Constructive Type Theory) and canonical (one representative per λ term). We define substitution for our map representation, and prove the representation is in substitution preserving isomorphism with both nominal logic λ terms and de Bruijn nameless terms. These proofs are mechanically checked in Isabelle/HOL and Minlog respectively. The map representation has good properties. Substitution does not require adjustment of binding information: neither α conversion of the body being substituted into, nor de Bruijn lifting of the term being implanted. We have a natural proof of the substitution lemma of λ calculus that requires no fresh names, or index manipulation. Using the notion of map we study conventional raw λ syntax. Eg we give, and prove correct, a decision procedure for α equivalence of raw λ terms that does not require fresh names. We conclude with a definition of β reduction for map terms, some discussion on the limitations of our current work, and suggestions for future work.