Background

$\alpha$Prolog is a logic programming language with a built-in notion of names, name binding, and equivalence up to renaming. $\alpha$Prolog is based on a logical theory of names and binding called nominal logic, that has its own semantics independent of logic programming. In this logic, it is possible to define relations that express precisely what we intuitively mean when we write programs that manipulate names, without giving up on determinism and ease of reasoning about programs. The clauses and goals allowed in $\alpha$Prolog are a simple subset of this logic, corresponding to Horn clauses and goals extended with a few additional operators. These operators include a freshness predicate $a \mathrel\char93 t$, which checks that a name $a$ does not occur in a term $t$, and a new-quantifier $\reflectbox{\sf N}a. \phi$, which expresses that $a$ is a new name in $\phi$ (that is, $a$ only appears in $\phi$ where it is explicitly mentioned; it cannot be ``hidden'' in any of $\phi$'s free variables).

$\alpha$Prolog also has a non-standard view of equality and unification. Terms in $\alpha$Prolog include a variable-binding operator $a\backslash t$, which expresses that the name $a$ is bound (or abstracted) in term $t$. This is not $\lambda$-abstraction; that is, the resulting term is not a function. Instead, however, terms are considered equal if corresponding abstractions can be renamed to be syntactically equal (without capturing any other variables). Thus, $a \backslash (a,b) = c \backslash (c,b)$ is true in $\alpha$Prolog; in fact, there is no way to distinguish the terms; on the other hand, $a \backslash (a,b) = b \backslash(b,b)$ does not hold, because the terms have different binding structure. This form of ``equality up to (safe) renaming'' is usually referred to as ``$\alpha$-equivalence'', and that is where the $\alpha$ in $\alpha$Prolog comes from.