Cornell University

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.

Principles
of Programming Seminars

Wednesday, April 14, 2004

3:30 p.m.

Wean Hall 8220