Pure Pattern Calculus à la de Bruijn
Pure Pattern Calculus à la de Bruijn
摘要：
在程序设计语言领域中众所周知的是，处理变量名和绑定器可能导致冲突，诸如在实现解释器或编译器时的不期望的捕获。这种情况已经通过求助于de Bruijn索引来克服，其中绑定器仅捕获一个变量名，如$λ$ -演算。这种方法的优点在于，当使用索引时，所谓的$α$ -等价变成了语法上的相等。近年来，模式演算由于其表现力而获得了相当大的关注。他们原来是出了名的方便，研究现代函数式程序设计语言的基础建模功能，如模式匹配，路径多态性，模式多态性等，但是，文献不足，当涉及到处理$α$转换和绑定器同时捕获几个变量名。纯模式演算（PPC）就是这种情况：它是$λ$的自然扩展--允许抽象几乎任何术语的演算。本文扩展了de Bruijn的思想，以适当地克服多绑定问题，通过引入一种新的表示PPC的二维索引，在努力实现一个原型的类型化函数式程序设计语言的基础上PPC，捕获路径多态性。
英文摘要：
It is well-known in the field of programming languages that dealing with variable names and binders may lead to conflicts such as undesired captures when implementing interpreters or compilers. This situation has been overcome by resorting to de Bruijn indices for calculi where binders capture only one variable name, like the $λ$-calculus. The advantage of this approach relies on the fact that so-called $α$-equivalence becomes syntactical equality when working with indices. In recent years pattern calculi have gained considerable attention given their expressiveness. They turn out to be notoriously convenient to study the foundations of modern functional programming languages modeling features like pattern matching, path polymorphism, pattern polymorphism, etc. However, the literature falls short when it comes to dealing with $α$-conversion and binders capturing simultaneously several variable names. Such is the case of the Pure Pattern Calculus (PPC): a natural extension of $λ$-calculus that allows to abstract virtually any term. This paper extends de Bruijn's ideas to properly overcome the multi-binding problem by introducing a novel presentation of PPC with bidimensional indices, in an effort to implement a prototype for a typed functional programming language based on PPC that captures path polymorphism.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
