Built-in Data and Types

Many of the built-in datatypes of $\alpha$Prolog are familiar from Prolog-like and ML-like languages. They include booleans (written "tt" and "ff"), integers ("-1","0","1","2",...), character constants ("'a'","'b'","'c'"), string constants ("abc"), the unit type (with the sole value "()"), pairs ("(1,2)", "('a',1)"), and lists ("[]", "1::[2]", "[1,2,3]", "[1|[2,3]]").

In addition, $\alpha$Prolog supports name and abstraction types. There are no built-in name types, but new name types can be declared as follows:

id : name_type.

This says that "id" is a name type. Name types are inhabited by infinitely many distinct but ``indeterminate'' names. We can always come up with a new name of type "id", just by writing down an unused (lower-case) identifier in a place where an "id" is expected. In addition to being placed in user-defined data structures, names can be used in transpositions, abstractions, and freshness tests.

A transposition is a term of the form (a~b) T where "a", "b" are names (of the same type) and T is an arbitrary term. The result is a term with all occurrences of "a" and "b" swapped. Any variables in "T" will be annotated with the transposition as well, indicating that once the variable is instantiated the delayed transposition should be applied to it. For example,

?- X = (a~b) (a,b,c) 
Yes.
X = (b,a,c)

An abstraction is a term of the form a\T where "a" is a name and "T" is a term. Abstractions describe a set of $\alpha$-equivalent terms (that is, equivalent up to consistent renaming). Two abstractions are equal if they describe the same such set. For example,

?- a\a = b\b.
Yes.
?- a\b = b\b.
No.
?- a\b = c\b.
Yes.

It is important to point out that logic variables are not allowed on the left hand side of an abstraction, or as the names in a transposition. Thus, terms like X\X and "(X Y)X" are not well-formed.