alpha Prolog: A logic programming language with names, binding and alpha-equivalence

By James Cheney and Christian Urban, from ICLP2004, available from the alphaProlog website:

There are two well-known approaches to programming with names, binding, and alpha-equivalence up to consistent renaming: representing names and bindings as concrete identifiers in a first-order language (such as Prolog), or encoding names and bindings as variables and abstractions in a higher-order language (such as Lambda-Prolog). However, both approaches have drawbacks: the former often involves stateful name-generation and requires manual definitions for alpha-equivalence and capture-avoiding substitution, and the latter is semantically very complicated, so reasoning about programs written using either approach can be very difficult.

Gabbay and Pitts have developed a new approach to encoding abstract syntax with binding based on primitive operations of name-swapping and freshness. This paper presents alphaProlog, a logic programming language that uses this approach, along with several illustrative example programs and an operational semantics.

Example programs, and more, are available from the alphaProlog website.

0 Responses to “alpha Prolog: A logic programming language with names, binding and alpha-equivalence”



  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: