The αProlog Project: Logic Programming with Names and Binding
αProlog is a logic programming language with built-in names, fresh
name generation, name binding, and unification up to α-equivalence
(that is, consistent renaming of bound names.) Though still in development,
its ultimate aim is to provide a better way of both writing and reasoning
about programs that rely heavily on names and binding, such as compilers,
interpreters, and theorem provers.
αProlog has the following features shared by other logic and
functional programming languages:
In addition, αProlog has several new features for programming with names
- Built-in basic types like integers, lists, strings, and so on
- Definite clause grammars
- Static typechecking and polymorphic types/data structures
- Names a, b are concrete data inhabiting name types.
- Names can be bound within terms using an abstraction construction n\t inhabiting abstraction types tn\tt.
- Names can be swapped with each other, and though there is no built-in notion of substitution of terms for names, capture-avoiding substitution can be defined for object languages.
- Term equality and unification are modulo alpha-equivalence.
- Fresh names are generated automatically as needed during execution, instead of explicitly (and imperatively) by the programmer.
- Freshness is an explicit built-in predicate a # t that can hold
between a name and a term
As an example of the style of nameful programming which αProlog supports,
consider the following declarations and clauses which describe the syntax and
capture-avoiding substitution operation of the lambda-calculus:
For example, we can encode the identity function as
id : name_type.
exp : type.
var : id -> exp.
app : (exp,exp) -> exp.
lam : id\exp -> exp.
lam (a\var a).
The standard approach to writing the same code in Prolog or Mercury would require maintaining a source of fresh names (such as an increasing integer tag) throughout the program, and writing more constraints forcing variables to be distinct.
However, in αProlog, capture-avoiding substitution can be written as
func subst(exp,exp,id) = exp.
subst(var(x),E,x) = E.
subst(var(y),E,x) = var(y).
subst(app(E1,E2),E,x) = app(subst(E1,E,x),subst(E2,E,x)).
subst(lam(y\E1),E,x) = lam(y\subst(E1,E,x)) :- y # E.
This behaves essentially the same as the explicit version, but the αProlog version is much simpler. There is no need for the programmer to keep track of the details of how names are generated. Instead, name parameters like x and y stand for arbitrary names (including fresh ones).
Secondly, in the var case, instead of testing whether the identifiers with which X and Y are instantiated are the same using if-then-else, we just specify what happens if the two identifiers are the same (the first clause) or different (the second clause). In αProlog, two distinct names are assumed to be semantically distinct, so the first and second clauses don't overlap.
Finally, in αProlog, we can use the built-in binding syntax to express the third clause. Instead of always renaming the bound variable, we just say that the bound name had better not conflict with any free variables in the substituted term E. This provides added generality: it might be possible to prove (through program analysis) that a fresh name is not necessary, thus saving the cost of renaming. Also, the execution order of the clauses is no longer fixed by the program, so, an implementation is free to execute them in any order (or in parallel). This was not the case with the traditional version, because there is a data dependency between (for example) the first and second call to
subst in the
Here are the example programs distributed with version 0.3:
αProlog is "alpha" software (no pun intended). The author cannot be held responsible for any problems with this software.
αProlog requires Objective Caml version 3.08 or greater.
The next version, version 0.4 will be released as soon as some specific known bugs are fixed. Here is a prerelease version:
The previous stable version of αProlog is 0.3.
Nolog, the predecessor of αProlog, is available here:
The current draft of the user's guide and language reference can be viewed online here.
Printable versions (pdf, ps)
The following papers cover technical aspects of αProlog and nominal abstract syntax, as well as related issues such as nominal logic, nominal/equivariant unification, implementing nominal abstract syntax in Haskell, and reasoning about nominal abstract syntax in Isabelle/HOL.
- Nominal Logic Programming, James Cheney and Christian Urban. Under review.
- Mechanized Metatheory Model-Checking, James Cheney and Alberto Momigliano, PPDP 2007 (ACM)
- The Semantics of Nominal Logic Programs, James Cheney. ICLP 2006, p. 361 - 375. (Errata) (Springer)
Completeness and Herbrand theorems for nominal logic, James Cheney, Journal of Symbolic Logic, 71(1), 299-320, 2006.
- Towards a General Theory of Names, Binding and Scope, MERLIN 2005. pp 33-40. (ACM)
- Scrap your Nameplate (Functional Pearl), James Cheney, ICFP 2005.
- Relating Higher-Order Pattern Unification and Nominal Unification, James Cheney, UNIF 2005
- Avoiding Equivariance in Alpha-Prolog, Christian Urban and James Cheney, TLCA 2005
- Equivariant Unification, James Cheney, RTA 2005
- A Simpler Proof Theory for Nominal Logic, James Cheney, FOSSACS 2005.
- Nominal Logic Programming, James Cheney, PhD dissertation, Cornell University, August 2004. (PDF)
- Alpha-Prolog: a logic programming language with names, binding
and alpha-equivalence, James Cheney and Christian Urban. ICLP 2004.
- A Sequent Calculus for Nominal Logic, Murdoch Gabbay and James Cheney. LICS 2004, p. 139-148.
- The Complexity of Equivariant Unification, James Cheney. ICALP 2004.
- System Description: alpha-Prolog, a Fresh Approach to Logic Programming Modulo alpha-Equivalence, James Cheney and Christian Urban. 2003 Workshop on Unification, Valencia, Spain, 2003.
The following papers provide important background material concerning nominal logic, the Gabbay-Pitts formalism, and nominal unification.
- A. M. Pitts, Alpha-Structural Recursion and Induction, Journal of the ACM 53(2006)459-506.
- C. Urban, A. M. Pitts and M.J. Gabbay, Nominal Unification, Theoretical Computer Science 323(2004) 473-497.
- A. M. Pitts, Nominal logic, a first-order theory of names and binding, Information and Computation 186 (2003) 165-193
- M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing 13 (2002) 341-363.
FreshML is an implementation of ML that includes user-defined "bindable"
(atomic) types and a type constructor <A>T of values of type
T abstracted by bindable type A. FreshML is based on the
same underlying Gabbay-Pitts theory of names as αProlog uses.
An extension to Isabelle/HOL to provide support for reasoning about nominal terms.
The Computational Applications of Nominal Sets project is investigating efficient algorithms such as unification and pattern matching for nominal terms.
Cαml is a preprocessing tool/frontend for Objective Caml that
takes a specification of the binding structure of a language (described using OCaml-like type definitions) as input and produces OCaml modules that provide traversals and other useful operations for this language. Interestingly, it provides support for pattern-match and mutual recursion binding structure.
Qu-Prolog is a logic programming language that includes "object-level" names,
substitutions, and unification up to α-equivalence. Though there are some
similarities to αProlog, there are major differences: Qu-Prolog's
underlying theory is much more complex (based on a classical treatment with
built-in capture-avoiding substitution) and its type system is much
more like traditional, dynamically-typed Prolog.
Lambda-Prolog is a very powerful higher-order logic programming language. Higher-order logic programming permits advanced programming techniques for module, data abstraction, natural language parsing, and higher-order abstract syntax. Lambda-Prolog has several mature implementations including an interpreter and compiler.
Twelf is an implementation of the (Edinburgh) Logical Framework (or LF).
In LF, judgments such as provability, reduction relations, and typability
can be encoded as (dependent) types inhabited by proofs or derivations.
Twelf includes advanced mode-checking and termination-checking facilities
for showing meta-properties of such relations, as well as a theorem prover
capable of proving theorems such as type preservation and cut elimination
author: j c h e n e y at inf dot ed dot ac dot uk