Prolog is a logic programming language with a built-in notion of
names, name binding, and equivalence up to renaming.
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
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
, which
checks that a name
does not occur in a term
, and a
new-quantifier
, which expresses that
is a new name
in
(that is,
only appears in
where it is explicitly
mentioned; it cannot be ``hidden'' in any of
's free variables).
Prolog also has a non-standard view of equality and unification.
Terms in
Prolog include a variable-binding operator
, which
expresses that the name
is bound (or abstracted) in term
. This is
not
-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,
is true
in
Prolog; in fact, there is no way to distinguish the terms; on the other
hand,
does not hold, because the
terms have different binding structure. This form of ``equality up to
(safe) renaming'' is usually referred to as ``
-equivalence'', and
that is where the
in
Prolog comes from.