论文标题
纯模式微积分àlade bruijn
Pure Pattern Calculus à la de Bruijn
论文作者
论文摘要
在编程语言领域中众所周知，处理可变名称和绑定器的处理可能会导致冲突，例如实施口译员或编译器时不希望的捕获。通过诉诸于calculi的de bruijn指数来克服这种情况，在该指数中，Binders仅捕获一个变量名称，例如$λ$ -Calculus。这种方法的优点取决于以下事实：与指数一起工作时，所谓的$α$等效性变为句法平等。 近年来，鉴于它们的表现力，模式的计算引起了很大的关注。事实证明，他们很方便地研究现代功能编程语言的基础建模功能，例如模式匹配，路径多态性，模式多态性等。但是，在处理$α$ conversion和binders捕获同时捕获几个可变名称的$α$ contression和绑定器时，文献却不足。纯模式微积分（PPC）就是这种情况：$λ$ -calculus的自然扩展，几乎可以抽象任何术语。 本文扩展了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.
