Defining New Types

Let's define a type representing simple $\lambda$-expressions. Since you can't enter declarations at the toplevel, we need to put this into a file. Call it "tutorial.apl".

To reflect the expression syntax, we need to define two types: a name type for variable identifiers, and the datatype of expressions.

id : name_type
exp : type.

This says that "id" is a name type and "exp" is a datatype.

Now we want to define the constructors for exp.

var : id -> exp.
app : (exp,exp) -> exp.
lam : (id\exp) -> exp.

This declares function symbols var, app, and lam with the corresponding types. Thus, given an identifier "v", we can construct an expression by applying the constructor "var" to it; similarly given expressions "E1" and "E2" we can form expression "app(E1, E2)" and given an expression E and a name a we can form an expression lam(a\E).

Now save the file and start $\alpha$Prolog as follows:

$ aprolog tutorial.apl

You should see:

alpha-Prolog 0.3
Reading file tutorial.apl...
?-

Try entering a few $\lambda$-terms (with or without meta-variables) and comparing them for equality or testing freshness.

?- lam (a\var a) = lam (b\var b).
Yes.
?- lam (a\var A) = lam (b\var A).
Yes.
a # A
b # A