Nominal logic programming

Names, name-binding, and equivalence of expressions up to “safe” renaming of bound names are often encountered in programming tasks, especially in writing programs that manipulate symbolic data such as mathematical expressions or other programs. Most programming languages provide no support for programming with names and binding, so operations like renaming and substitution must be written by hand, on an application-by-application basis. been developed by Gabbay and Pitts, based on defining concepts like name-binding and substitution in terms of more primitive concepts including name-swapping and freshness. We call this approach nominal This dissertation investigates nominal logic programming, or logic programming using nominal logic. The contributions of this dissertation are as follows. A nominal logic programming language called αProlog is presented, along with examples of programs that are particularly convenient to write in αProlog. A revised form of nominal logic that provides a suitable foundation for nominal logic programming is developed. Both operational and denotational semantics for nominal logic programming are given, and soundness and completeness properties are proved. The unification and other nominal constraint problems that must be solved during execution of nominal logic programs are identified, and the complexity of and algorithms for solving these constraints are investigated. techniques for programming with names and binding, notably higher-order is both simpler and more expressive than HOAS: in particular, HOAS cannot easily handle open terms, or terms with an unknown number is no problem with open terms. These contributions support the contention that nominal logic programming is a powerful technique for programming with names and binding.