αML is a functional-logic programming language with special features for prototyping inductive definitions involving binding. The syntax of αML resembles that of traditional functional programming languages but includes features for proof search and unification from logic programming and techinques from nominal abstract syntax for dealing with abstract syntax modulo α-equivalence.
For example, a declaration of datatypes for encoding λ-terms might look like:
nametype var;; datatype lam = V of var | A of lam * lam | L of [var]lam;;
The first line declares a type of bindable names which will be used to represent variables. The second line declares a datatype of λ-terms. The argument type of the L constructor is an abstraction type, which represents the binding of a variable in a term. Abstraction types are inhabited by expressions <e>e', so the term λx.x could be represented as L <x>(V x).
Functions can be defined by recursion over such datatypes. The capture-avoiding substitution t'[t/x] can be implemented as an αML function sub of type term -> var -> term -> term, as follows.
let rec sub (t':lam) (x:var) (t:lam) : lam = case t' of
V y -> (x=y & t) || (x#y & V y)
| A w -> let t1 = w.1 in let t2 = w.2 in
A((sub t1 x t),(sub t2 x t))
| L z -> unbind z as <y>t'':[var]lam in
y#(x,t) & L<y>(sub t'' x t);;
The clause for variables uses branching and equality/freshness constraints to mimic an if-then-else construct for name equality. In the λ clause, a syntactic sugar is used to unbind the abstraction by generating a new meta-variable and asserting some freshness constraints explicitly. This captures the precise set of names that the bound name must be disjoint from.
The sub function can now be used to define other functions and relations. To specify single-step reduction of λ-terms, we first declare a relation symbol REDUCE:
relation REDUCE <: lam * lam;;
and then define the relation via a set of schematic rules.
yes
------------------------------------ [reduce_beta where x:var, t,t',t'':lam]
REDUCE(A((L<x>t),t'),(sub t' x t))
REDUCE(t,t'')
--------------------------- [reduce_app where t,t',t'':lam]
REDUCE(A(t,t'),A(t'',t'))
The first of these is the standard β-reduction rule. This syntax is intended to closely resemble informal practice in operational semantics, and the compiler automatically expands these definitions into αML code.
The design of the language and the underlying theory were developed as joint work with Andrew Pitts. The work was supported by UK EPSRC grant EP/D000459/1 (Computational Applications of Nominal Sets).
The most recent version of αML (version 0.3) is available for download here:
The source distribution has been compiled successfully on Linux, Mac OS X and Windows Vista. The following are prerequisites for compiling the source:
αML is released under the terms of the GNU General Public License, version 3.
The source and binary distributions both contain documentation including build instructions and a reference to the concrete syntax of the language. This documentation is reproduced here for online reading.