Nominal terms (computer science)
Encyclopedia
Nominal terms are a metalanguage
for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence
(equivalence up to a permutative renaming of bound names). Nominal terms came out of a programme of research into nominal sets
, and have a concrete semantics in those sets.
Nominal unification is efficiently decidable. This fact led to the development of alphaProlog, a Prolog
-like logic programming
language with facilities for binding names in terms, where Prolog's standard first-order unification algorithm is replaced with nominal unification.
Nominal term embeddings may be seen as alternatives to de Bruijn encodings
and higher-order abstract syntax
, where the latter uses the simply typed lambda calculus
as a metalanguage.
, the lambda-binder from the lambda-calculus, and the pi-binder from the pi-calculus
are all examples of name-binding constructs.
Computer scientists often need to manipulate abstract syntax trees. For instance, compiler
writers perform many manipulations of abstract syntax trees during the various optimisation and elaboration phases of compiler execution. In particular, when working with abstract syntax trees with name binding constructs, we often want to work on alpha-equivalence classes, implement capture-avoiding substitutions, and make it easy to generate fresh names. How best to do this, in a bug free and reliable manner, motivates a large amount of research.
Prior attempts at solving this problem include 'nameless approaches' such as de Bruijn indices and levels, and higher-order approaches such as higher-order abstract syntax. Nominal terms are another, relatively new, approach that retain explicit names for bound variables like higher-order abstract syntax, whilst retaining the first-order flavour (and first-order computational properties) of de Bruijn encodings.
. This motivates the search for subsets of lambda-terms that enjoy a computationally well-behaved unification procedure. Higher-order patterns, proposed by Miller, are one such set.
Higher-order patterns are lambda-terms
where the arguments of a free variable are all distinct bound variables. They possess an efficiently decidable unification procedure, and as a result, have been widely implemented, notably in the logic programming language lambdaProlog.
A recent body of work has investigated the connections between nominal terms and higher-order patterns, and consequently between nominal unification and higher-order pattern unification. Cheney proposed an extension of nominal terms called nominal patterns. He then provided a translation between nominal patterns and higher-order patterns which preserved unifiers
. Later, Levy and Villaret demonstrated a translation between nominal terms and higher-order patterns that preserves the notion of unifiability. That is, if two nominal terms are unifiable, then their translated pattern counterparts are also unifiable.
Dowek and Gabbay later sharpened Levy and Villaret's translation, proving that in some sense their translation is the best that there can be, and proved that the improved translation preserves unifiers. That is, if two nominal terms are unifiable by some substitution, then the corresponding higher-order pattern unification problem under the translation is solved by the translated substitution. For their proof, Dowek and Gabbay used a variation of nominal terms called permissive nominal terms. However, a translation from permissive nominal terms and back again also exists, completing the translation between nominal terms and higher-order patterns.
Metalanguage
Broadly, any metalanguage is language or symbols used when language itself is being discussed or examined. In logic and linguistics, a metalanguage is a language used to make statements about statements in another language...
for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
(equivalence up to a permutative renaming of bound names). Nominal terms came out of a programme of research into nominal sets
Nominal techniques
Nominal techniques are a range of techniques, based on nominal sets, for handling names and binding, e.g. in abstract syntax. Research into nominal sets gave rise to nominal terms, a metalanguage for embedding object languages with name binding constructs into....
, and have a concrete semantics in those sets.
Nominal unification is efficiently decidable. This fact led to the development of alphaProlog, a Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
-like logic programming
Logic programming
Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
language with facilities for binding names in terms, where Prolog's standard first-order unification algorithm is replaced with nominal unification.
Nominal term embeddings may be seen as alternatives to de Bruijn encodings
De Bruijn index
In mathematical logic, the De Bruijn index is a notation invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms in the λ calculus with the purpose of eliminating the names of the variable from the notation. Terms written using these indexes are invariant with respect...
and higher-order abstract syntax
Higher-order abstract syntax
In computer science, higher-order abstract syntax is a technique for the representation of abstract syntax trees for languages with variable binders.-Relation to first-order abstract syntax:...
, where the latter uses the simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
as a metalanguage.
Motivation
Many interesting calculi, logics and programming languages that are commonly seen in computer science feature name binding constructs. For instance, the universal quantifier from first-order logicFirst-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
, the lambda-binder from the lambda-calculus, and the pi-binder from the pi-calculus
Pi-calculus
In theoretical computer science, the π-calculus is a process calculus originally developed by Robin Milner, and David Walker as a continuation of work on the process calculus CCS...
are all examples of name-binding constructs.
Computer scientists often need to manipulate abstract syntax trees. For instance, compiler
Compiler
A compiler is a computer program that transforms source code written in a programming language into another computer language...
writers perform many manipulations of abstract syntax trees during the various optimisation and elaboration phases of compiler execution. In particular, when working with abstract syntax trees with name binding constructs, we often want to work on alpha-equivalence classes, implement capture-avoiding substitutions, and make it easy to generate fresh names. How best to do this, in a bug free and reliable manner, motivates a large amount of research.
Prior attempts at solving this problem include 'nameless approaches' such as de Bruijn indices and levels, and higher-order approaches such as higher-order abstract syntax. Nominal terms are another, relatively new, approach that retain explicit names for bound variables like higher-order abstract syntax, whilst retaining the first-order flavour (and first-order computational properties) of de Bruijn encodings.
Relation with higher-order patterns
Higher-order unification is known to be undecidableUndecidable problem
In computability theory and computational complexity theory, an undecidable problem is a decision problem for which it is impossible to construct a single algorithm that always leads to a correct yes-or-no answer....
. This motivates the search for subsets of lambda-terms that enjoy a computationally well-behaved unification procedure. Higher-order patterns, proposed by Miller, are one such set.
Higher-order patterns are lambda-terms
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
where the arguments of a free variable are all distinct bound variables. They possess an efficiently decidable unification procedure, and as a result, have been widely implemented, notably in the logic programming language lambdaProlog.
A recent body of work has investigated the connections between nominal terms and higher-order patterns, and consequently between nominal unification and higher-order pattern unification. Cheney proposed an extension of nominal terms called nominal patterns. He then provided a translation between nominal patterns and higher-order patterns which preserved unifiers
Unification
Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal...
. Later, Levy and Villaret demonstrated a translation between nominal terms and higher-order patterns that preserves the notion of unifiability. That is, if two nominal terms are unifiable, then their translated pattern counterparts are also unifiable.
Dowek and Gabbay later sharpened Levy and Villaret's translation, proving that in some sense their translation is the best that there can be, and proved that the improved translation preserves unifiers. That is, if two nominal terms are unifiable by some substitution, then the corresponding higher-order pattern unification problem under the translation is solved by the translated substitution. For their proof, Dowek and Gabbay used a variation of nominal terms called permissive nominal terms. However, a translation from permissive nominal terms and back again also exists, completing the translation between nominal terms and higher-order patterns.