[Next] [Up] [Previous] [Contents]
Next: Running Prolog Up: Tutorial Previous: Definitions   Contents


Now let's take on a harder problem: defining capture-avoiding substitution. We'll define substitution as a function since we usually want to run it ``forward'' (i.e., given a term and a substitution, construct the result) rather than ``reverse''.

To declare a function write (in tutorial.apl):

func subst(tm,[(id,tm)]) = tm.
This expresses that $ subst$ is a function symbol taking two arguments: a term and a list of identifier-term pairs (i.e., the subsitution), and producing a term. Now let's define cases. Clauses for function definitions are of the form $ f(t_1,\ldots,t_n) = t \mathrel{:-} G$, where $ f$ is the function being defined, the $ t_i$ are the inputs for which the clause defines a value, $ t$ is the value, and $ G$ is a subgoal that must be solved for the clause to apply. For example
subst(var(A),S)     = T                           :- mem((A,T),S).
subst(var(A),S)     = var A                       :- not(mem(A,_),S).
subst(app(T1,T2),S) = app(subst(T1,S),subst(T2,S)).
subst(lam(x\T),S)   = lam(x\subst(T,S))           :- x # S.
The first clause asserts that if $ A$ is bound to a term $ T$ in $ S$ then $ T$ is the result. The second, that if $ A$ is not so bound, then $ var(A)$ is the result. The third clause just propagates $ subst$ past an application. The final clause propagates $ subst$ past a $ lam$, provided the bound variable $ x$ is not mentioned in $ S$. Since $ x$ appears only in an abstraction, it is always possible to satisfy this constraint by renaming $ x$ (although at times renaming may not be necessary). In fact, this is what $ \alpha $Prolog does by default.

Is this definition really correct? Let's try some examples.

?- X = subst(var(a), [(a,var(b))]).
X = var b
?- X = subst(lam(a\var(a)), [(a,var(b))]).
X = lam (a\var(a))
?- X = subst(lam(b\var(a)), [(a,var(b))]).
X = lam (b1\var(b))
Note that in the final case, the bound variable $ b$ has been freshened to $ b_1$. Remember that when a name is used in an abstraction, we lose control over its specific value since the abstraction really represents an equivalence class of $ \alpha $-equivalent terms. The last example also verifies that a simple form of variable capture is actually impossible. That is, it's not the case that $ subst$ happens to get the right answer the first time it succeeds; in fact, no alternative wrong answers are possible.

Now this definition of $ subst$ has some disadvantages: for example the first two clauses overlap and may repeat the membership test $ mem ((A,V),S)$. We can make this more efficient using $ \alpha $Prolog's ``if-then-else'' construct:

subst(var A,S) = T :- mem ((A,V),S) -> T = V | T = var(A).
Similarly, we can collapse the other two clauses into one completely general case using disjunction:
subst(T,A) = T' :- ( T = var(A), 
                     if mem((A,V),S) 
                     then T = V 
                     else T = var(A)
                   ; T = app(T1,T2), 
                     T' = app(subst(T1,S),subst(T2,S)))
                   ; T = lam(x\T1), 
                     x # S, 
                     T' = lam(x\subst(T1,S)))

Another alternative would be to replace the call to $ mem$ with a substitution-specific $ lookup$ function:

func lookup(id,[(id,exp)]) = exp.
lookup(A,[]) = var A.
lookup(A,[(A,V)|S]) = V.
lookup(A,[(B,V)|S]) = lookup(A,S).
subst(var A,S) = lookup(A,S).

Both this and the earlier definition have the potential disadvantage that if duplicate bindings are present in a substitution (e.g., $ s = [(a,t_1),(a,t_2)]$), then $ lookup$ or $ mem$ can succeed with multiple possible answers. We therefore regard substitutions to be well-formed only if there are no such duplicates.

[Next] [Up] [Previous] [Contents]
Next: Running Prolog Up: Tutorial Previous: Definitions   Contents
James Cheney 2003-10-23