AlphaProlog 0.3 releae announcement

James Cheney <jcheney@cs.cornell.edu> · 24 Oct 2003 17:08:54 -0400

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

I am pleased to announce the initial public release of AlphaProlog,
version 0.3.

What is AlphaProlog?
--------------------

AlphaProlog is a logic programming language with built-in names, fresh
name generation, name binding, and unification up to alpha-equivalence
(that is, consistent renaming of bound names). Though still in
development, its ultimate aim is to provide a better way of both writing
and reasoning about programs that rely heavily on names and binding,
such as compilers, interpreters, and theorem provers.

AlphaProlog supports a declarative, stateless approach to programming 
with names, based on FM, a permutation-based theory of abstract syntax 
and binding developed by Gabbay and Pitts and used in the FreshML 
programming language, and, more directly, on Pitts's nominal
logic and Urban, Pitts, and Gabbay's nominal unification algorithm.

Languages like Twelf, Qu-Prolog, and Lambda-Prolog also support encoding
names and binding using built-in meta-level variables and bindings. 
These languages are semantically much richer and more complex than
AlphaProlog, which is essentially first-order.  While these languages
are more mature and provide some features which AlphaProlog lacks, there
are some kinds of programs which are difficult to express using
higher-order encodings but easy to express in AlphaProlog.  Examples
include computations involving open terms, fresh name generation, or
varying numbers of bound variables. 

This makes AlphaProlog a very useful tool for prototyping languages, 
type systems, operational semantics, and logics that sometimes play 
the square peg to higher-order encoding techniques' round hole.  
Some examples that are included with the AlphaProlog distribution 
include:

    * The operational semantics of the pi-calculus in its original form
    * Regular expression-to-automata translation
    * An object calculus and its translation from the lambda-calculus
    * A closure-conversion translation
    * First-order unification and MiniML type inference
    * A natural deduction calculus for Dynamic Logic with proof terms

Features
--------

AlphaProlog has the following features shared by other logic and 
functional programming languages:

    * Built-in basic types like integers, lists, strings, and terms
    * First order Horn clause and definite clause grammar programming
    * Static typechecking and polymorphic types and data structures

In addition, AlphaProlog has several new features for programming with 
names and binding:

    * Names are concrete data inhabiting name types.
    * Names can be bound within terms using an abstraction construction 
      inhabiting abstraction types (distinct from function types).
    * Names can be swapped with each other, and though there is no 
      built-in notion of substitution of terms for names,
      capture-avoiding substitution operations are definable.
    * Term equality and unification are modulo alpha-equivalence.
    * Fresh names are generated automatically as needed during
      execution, instead of explicitly (and imperatively) by the
      programmer.
    * Freshness is an explicit built-in predicate relating names and terms.

Where can I get AlphaProlog?
----------------------------

A source distribution as well as more information about AlphaProlog, 
including examples and (draft) documentation, is available at

    http://www.cs.cornell.edu/People/jcheney/aprolog/

Questions, comments, and bug reports should be direted to the author at

    jcheney@cs.cornell.edu

Related Information
-------------------

More information about FM, nominal logic/unification, and FreshML can 
be found at:

    http://www.freshml.org/

    http://www.cl.cam.ac.uk/~cu200/Unification

--James