Foundations of nominal techniques: logic and semantics of variables in abstract syntax

Bulletin of Symbolic Logic 17 (2):161-229 (2011)

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
Keywords Nominal techniques   logic and set theory   nominal abstract syntax   atoms-abstraction   names   variable binding   inductive syntax up to binding   alpha-equivalence
Categories (categorize this paper)
DOI 10.2178/bsl/1305810911
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,865
Through your library

References found in this work BETA

The Lambda Calculus. Its Syntax and Semantics.H. P. Barendregt - 1984 - Journal of Symbolic Logic 49 (1):301-303.
Quantifiers in Formal and Natural Languages.Dag Westerståhl - 1989 - In Dov Gabbay & Franz Guenthner (eds.), Handbook of Philosophical Logic. Kluwer Academic Publishers. pp. 1--131.
Completeness and Herbrand Theorems for Nominal Logic.James Cheney - 2006 - Journal of Symbolic Logic 71 (1):299 - 320.

View all 9 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Completeness and Herbrand Theorems for Nominal Logic.James Cheney - 2006 - Journal of Symbolic Logic 71 (1):299 - 320.
What is Context For? Syntax in a Non-Abstract World.Tom Sgouros - 2005 - Journal of Logic, Language and Information 14 (2):235-251.
The Abstract Variable-Binding Calculus.Don Pigozzi & Antonino Salibra - 1995 - Studia Logica 55 (1):129 - 179.
Provability with Finitely Many Variables.Robin Hirsch, Ian Hodkinson & Roger D. Maddux - 2002 - Bulletin of Symbolic Logic 8 (3):348-379.
Variables as Stacks.C. F. M. Vermeulen - 2000 - Journal of Logic, Language and Information 9 (2):143-167.
Axiomatic Inscriptional Syntax. Part II: The Syntax of Protothetic.Frederick Rickey - 1973 - Notre Dame Journal of Formal Logic 14 (1):1-52.
Separating Syntax and Combinatorics in Categorial Grammar.Reinhard Muskens - 2007 - Research on Language and Computation 5 (3):267-285.

Analytics

Added to PP index
2011-05-20

Total views
30 ( #286,222 of 2,266,104 )

Recent downloads (6 months)
1 ( #855,138 of 2,266,104 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature