Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
复制标题
名词技术的基础：抽象语法中变量的逻辑和语义
作者：
M. Gabbay
我们已经习惯了计算机对数字进行操作的想法，然而另一种数据同样重要：形式语言的语法，变量，绑定和alpha等价。名词性技术的最初应用，也是本文最突出的应用，是对具有变量和约束的形式句法的推理。变量可以以多种方式建模：例如，作为数字（因为我们通常会取可数的变量）;作为链接（因为它们可能“指向”术语中的绑定位点，即它们绑定的位置）;或者作为函数（因为它们经常（尽管不总是）表示“未知数”）。这些模型都不是完美的。在上述模型的每一种情况下，当试图将它们用作对形式语言进行完全形式化的机械处理的基础时，都会出现问题。这些问题是实际的，但其根本原因可能是数学。问题不在于形式语法是否存在，因为它显然存在，而在于它是什么样的数学结构。为了通过模仿来说明这一点，逻辑推导可以使用哥德尔编码来建模（即，注入自然数）。由此得出结论说证明论是数论的一个分支，可以用皮亚诺公理来理解，这是错误的。同样，事实证明，从变量可以被编码的事实得出结论是错误的，例如，作为数字，有约束力的语法理论可以理解为无约束力的语法理论，加上数字理论（或者，将其推向逻辑极端，纯粹是数字理论）。它不能;还有别的东西在发生。那别的东西是什么，还没有完全被理解。在名义技术中，变量是名称的实例，而名称是数据。我们使用urelemente对名字进行建模，这些属性在世纪上半叶由Fraenkel和Mostowski进行了研究，目的与建模形式语言完全不同。这个模型真正有趣的地方在于，它给出了与形式语法的有用逻辑和编程原则相关的独特属性。自最初的出版物，在数学和演示文稿的进展已被介绍零碎的文献。本文提供了一个单一的访问文件的名义技术的基础的最新发展。这使读者很容易获得更新的结果和新的证明，否则他们将不得不在两个或更多的论文中搜索找到，以及在其他出版物中可能被省略的完整证明。我们还包括一些其他地方没有出现的新材料。
Abstract We are used to the idea that computers operate on numbers, yet another kind of data is equally important: the syntax of formal languages, with variables, binding, and alpha-equivalence. The original application of nominal techniques, and the one with greatest prominence in this paper, is to reasoning on formal syntax with variables and binding. Variables can be modelled in many ways: for instance as numbers (since we usually take countably many of them); as links (since they may ‘point’ to a binding site in the term, where they are bound); or as functions (since they often, though not always, represent ‘an unknown’). None of these models is perfect. In every case for the models above, problems arise when trying to use them as a basis for a fully formal mechanical treatment of formal language. The problems are practical—but their underlying cause may be mathematical. The issue is not whether formal syntax exists, since clearly it does, so much as what kind of mathematical structure it is. To illustrate this point by a parody, logical derivations can be modelled using a Gödel encoding (i.e., injected into the natural numbers). It would be false to conclude from this that proof-theory is a branch of number theory and can be understood in terms of, say, Peano's axioms. Similarly, as it turns out, it is false to conclude from the fact that variables can be encoded e.g., as numbers, that the theory of syntax-with-binding can be understood in terms of the theory of syntax-without-binding, plus the theory of numbers (or, taking this to a logical extreme, purely in terms of the theory of numbers). It cannot; something else is going on. What that something else is, has not yet been fully understood. In nominal techniques, variables are an instance of names, and names are data. We model names using urelemente with properties that, pleasingly enough, turn out to have been investigated by Fraenkel and Mostowski in the first half of the 20th century for a completely different purpose than modelling formal language. What makes this model really interesting is that it gives names distinctive properties which can be related to useful logic and programming principles for formal syntax. Since the initial publications, advances in the mathematics and presentation have been introduced piecemeal in the literature. This paper provides in a single accessible document an updated development of the foundations of nominal techniques. This gives the reader easy access to updated results and new proofs which they would otherwise have to search across two or more papers to find, and full proofs that in other publications may have been elided. We also include some new material not appearing elsewhere.