# αML

α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.
**Feedback and bug reports are greatly appreciated - please send them
to my email address.**

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).

## Download

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.

## Documentation

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.
`manual.pdf` - detailed build instructions and language reference.
`README` - quick build instructions.

There are also several published papers on the subject of αML - see my
main web page for more information.

Last modified: Sun Sep 11 17:45:04 MDT 2011