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(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
Is this definition really correct? Let's try some examples.
?- X = subst(var(a), [(a,var(b))]). Yes. X = var b ?- X = subst(lam(a\var(a)), [(a,var(b))]). Yes. X = lam (a\var(a)) ?- X = subst(lam(b\var(a)), [(a,var(b))]). Yes. X = lam (b1\var(b)) ; No.Note that in the final case, the bound variable
Now this definition of has some disadvantages: for example the
first two clauses overlap and may repeat the membership test
.
We can make this more efficient using
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 with a
substitution-specific
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.,
),
then
or
can succeed with multiple possible answers.
We therefore regard substitutions to be well-formed only if there
are no such duplicates.