In this section we develop an example Prolog program which demonstrates how to encode a simple language with names, binding, and capture-avoiding substitution.

For our first example, consider the typed -calculus (a notation for
anonymous function definitions). Its syntax is summarized by the
following grammar

where expression variables and type variables are drawn from disjoint, countably infinite sets. We can encode the syntax of -terms using declarations

id : name_type. exp : type. var : id -> exp. app : (exp,exp) -> exp. lam : id\exp -> exp. tid : name_type. ty : type. tvar : tid -> type. arrow : (ty,ty) -> ty.

Since identifiers, expressions, and types are just terms, Prolog can be used to define interesting functions and relations among such terms. These definitions tend to be significantly closer to their ``paper'' presentations than is usual for either functional or logic languages. For example, the following rules express the syntax and typability relation for simply-typed -terms:

pred of([(id,ty)],exp,ty) of(Gamma,var(X),A) :- mem((X,A),Gamma). of(Gamma,app(M,N),B) :- of(Gamma,M,arrow(A,B)), of(Gamma,N,A). of(Gamma,lam(x\M),arrow(A,B)) :- x # Gamma, of([(x,A)|Gamma],M,B).

In Prolog, we might instead encode a binding as a term ``x''``x'', that is, using strings or some other data for variables. In Prolog, we think of as a term constructor mapping abstraction terms to . This view of the world is somewhat similar to that adopted in higher-order abstract syntax, where is (somewhat circularly) defined as a constructor with type . But although there are similarities (for example, both function variables and abstracted names admit equality up to -equivalence), the abstraction type is quite distinct from the function type: for example, there is no built-in application of abstractions, and names are ground terms that can escape the scope of abstractions in limited ways (as does "x" in the last clause of "of").

Another interesting relation (or function) on -terms is
*substitution*. For example,
.
In the -calculus, we ask that
substitution not essentially change the ``meaning'' of a term (as a function).
To illustrate this point, consider the following flawed
definiton of substitution:

Under this definition, substituting for in the term could result in , which is a different function. This can be seen by -renaming to , in which substituting for results in . The reason is that in the obvious approach to substitution, variables can be ``captured'' when substitution passes under a binding (as is when we pass under the binder).

The classical approach to this problem is to assume that bound variables are
always ``renamed away'' from the all free variables (this is called
Barendregt's variable convention). Subject to this convention, the above naive
definition becomes correct: equivalently, we can write the fourth clause as

However, this is not precise enough for a Prolog program to implement, because the implicit, highly nondeterministic ``renaming away'' step needs to be made explicit. Renaming itself also needs to avoid variable capture, so for a mechanical implementation of substitution it is necessary to write down explicitly how to rename/substitute without capture. A typical definition of ``capture-avoiding'' substitution uses a rule

This definition renames aggressively, picking a fresh variable whenever a binding is encountered.

However, there are problems with turning this definition into a Prolog-style declarative program. For example, the choice of is very open-ended, and to choose fresh variables efficiently it is necessary to maintain a ``store'' of unused variable names. This store is passed as an extra argument and return value of . Also, this definition causes multiple passes to be made over the term because of the renaming. To reduce this to a single pass, we would have to add an additional argument mapping renamed variables to their renamings.

In Prolog, on the other hand, we are able to write a definition that is essentially the same as the declarative definition, yet correct:

func subst(exp,exp,id) = exp. subst(var(x),E,x) = E. subst(var(y),E,x) = var(y) :- y # x. subst(app(E1,E2),E,x) = app(subst(E1,E,x),subst(E2,E,x)). subst(lam(y\E1),E,x) = lam(y\subst(E1,E,x)) :- y # E, y # x.where we read as and as . In fact, in Prolog, syntactically distinct name identifiers like are assumed to denote distinct names, so the constraints are redundant. On the other hand, we cannot assume that bound variables always are distinct from other variables in scope, so we must check in the fourth clause. Because unification in Prolog is up to -equivalence, the implicit renaming step from the declarative definition remains implicit.

[Next] [Up] [Previous] [Contents]