Traditional logic programming is well-suited to describing relations on
terms defined using inference rules, but it does not do so well when we
terms may contain variables and binding. Although the
higher-order abstract syntax technique can often help with this
situation, it also has limitations: two important examples are the
difficulty of dealing with open terms (terms with an unknown number of
free variables), and the difficulty of developing sound induction
principles on higher-order encodings that simulate informal syntactic
proof techniques.
Gabbay and Pitts have developed a new approach to dealing with syntax
involving names/variables and binding which is essentially first-order,
and treats names as an abstract data type. Besides representing
bound variables in programming language syntax, such names can be used
to represent free names in open terms, channel names in concurrency
calculi, nonces in security protocols, and vertex/state names in
graph/automata constructions. This approach has no problem
dealing with open terms and is semantically much simpler that
higher-order abstract syntax, and comes with useful induction
principles built-in.
I (in collaboration with C. Urban) have developed a logic programming
language called alpha-Prolog, based on the Gabbay-Pitts name
theory. In this talk I will describe unification and execution in
alpha-Prolog, focusing on two examples: typechecking in the
lambda-calculus (a familiar example for which HOAS already works fine)
and constructing automata from regular expressions (for which HOAS
provides no support). Along the way I will discuss an important
technical challenge yet to be overcome: the form of unification needed
to find all possible answers
for alpha-Prolog queries is NP-complete.