纯模式演算的 de Bruijn 风格表示
计算机科学中的逻辑
2021-10-29 v2 编程语言
摘要
在程序设计语言领域，众所周知，处理变量名和绑定子在实现解释器或编译器时可能导致诸如意外捕获等冲突。对于绑定子仅捕获一个变量名的演算（如 -演算），这种情况已通过采用 de Bruijn 指标得以克服。这种方法的优势在于，当使用指标时，所谓的 -等价变成了语法相等。近年来，模式演算因其表达力而获得了相当大的关注。它们被证明在研究现代函数式编程语言的基础时极为便利，能够对模式匹配、路径多态、模式多态等特性进行建模。然而，文献在处理 -转换以及同时捕获多个变量名的绑定子方面尚显不足。纯模式演算（PPC）正是这种情况：它是 -演算的一种自然扩展，允许对几乎任意项进行抽象。本文扩展了 de Bruijn 的思想，通过引入一种具有二维指标的新颖 PPC 表示，恰当地克服了多绑定问题，旨在实现一个基于 PPC 的类型化函数式编程语言原型，以捕获路径多态。
引用
@article{arxiv.2006.07674,
title = {Pure Pattern Calculus \`a la de Bruijn},
author = {Alexis Martín and Alejandro Ríos and Andrés Viso},
journal= {arXiv preprint arXiv:2006.07674},
year = {2021}
}