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.

Features

αProlog has the following features shared by other logic and functional programming languages: In addition, αProlog has several new features for programming with names and binding:

Examples

The lambda-calculus

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:
id : name_type.
exp : type.

var : id -> exp.
app : (exp,exp) -> exp.
lam : id\exp -> exp.
For example, we can encode the identity function as 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 follows:
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 app case.

More Examples

Here are the example programs distributed with version 0.3:

Download

αProlog is "alpha" software (no pun intended).  The author cannot be held responsible for any problems with this software.

Requirements

αProlog requires Objective Caml version 3.08 or greater.

Source

Current version
The next version, version 0.4 will be released as soon as some specific known bugs are fixed. Here is a prerelease version:
Previous versions
The previous stable version of αProlog is 0.3. Nolog, the predecessor of αProlog, is available here:

User's Guide

The current draft of the user's guide and language reference can be viewed online here.

Printable versions (pdf, ps)

HTML archive

Related publications

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.

Background reading

The following papers provide important background material concerning nominal logic, the Gabbay-Pitts formalism, and nominal unification.

Links

FreshML

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.

Nominal Datatype Package

An extension to Isabelle/HOL to provide support for reasoning about nominal terms.

The CANS project

The Computational Applications of Nominal Sets project is investigating efficient algorithms such as unification and pattern matching for nominal terms.

Cαml

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

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

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

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 automatically.
author: j c h e n e y  at  inf  dot  ed  dot  ac  dot  uk