Capture-avoiding substitution function — Lambda calculus

Question

So I got below substitute function with which I'm trying to replace b for Church numeral 0 in example term:

\a. \x. (\y. a) x b

*Main> substitute "b" (numeral 0) example

which is currently giving me:

\c. \a. (\b. c) a (\f. \x. x)

however I was expecting answer to be :

\c. \a. (\a. c) a (\f. \x. x)

Could you advise me what I am getting wrong here, is that the use of fresh ?? Substitute function here seems to be not considering 'a' here as a fresh variable as it's already used as a replacement to what was previously x? Is there any way to get around this ?

substitute :: Var -> Term -> Term -> Term
substitute x n (Variable y)| y == x = n
                           | otherwise = (Variable y)
substitute x n (Lambda y m)| y == x = (Lambda y m)
                           | otherwise = (Lambda new_z m')
                                 where
                                  new_z = fresh([x] `merge` (used m) `merge`(used n))
                                  m' = substitute x n (substitute y (Variable new_z) m)
substitute x n (Apply m1 m2) = (Apply new_m1 new_m2)
                                 where new_m1 = substitute x n m1
                                       new_m2 = substitute x n m2

where

used :: Term -> [Var]
used (Variable z) = [z]
used (Lambda z n) = merge [z](used n)
used (Apply n m) = merge (used n)(used m)

and

fresh :: [Var] -> Var
fresh st = head (filterVariables variables st)

variables :: [Var]
variables = [s:[]| s <- ['a'..'z']] ++ [s: show t | t <- [1..],s <- ['a'..'z'] ]

filterVariables :: [Var] -> [Var] -> [Var]
filterVariables s t = filter (`notElem` t) s

and

merge :: Ord a => [a] -> [a] -> [a]
merge xs [] = xs
merge [] ys = ys
merge (x:xs) (y:ys)
    | x == y    = x : merge xs ys
    | x <= y    = x : merge xs (y:ys)
    | otherwise = y : merge (x:xs) ys

user_849891 · Answer

From the lambda calculus perspective, b is free in \a. \x. (\y. a) x b, so substituting 0 for b gives \a. \x. (\y. a) x 0, and if 0 = \f. \x. x then it is

\a. \x. (\y. a) x (\f. \x. x)
===
\c. \x. (\y. c) x (\f. \x. x)
===
\c. \x. (\b. c) x (\f. \x. x)

and you apparently get

\c. \a. (\b. c) a (\f. \x. x)

which is the same lambda term, up to alpha-conversion (consistent capture-avoiding renaming of variables).

So there is no error.

user_3234959 · Answer

Your new_z is chosen to be fresh in a rather conservative way, in the sense that you always generate a completely new variable name, and never reuse a variable that already occurs in the term, even when that variable could be reused without causing unwanted captures.

More in details, when you substitute something inside \y. a you will change y into something else, even if there are no clashes.

Now, due to how your Lambda case works, you perform multiple substitutions (note the nested substitute x n (substitute y (Variable new_z) m)).

So, I guess that when you rename a to c, your \y. a is first alpha-converted to \a. c as you expect. However, the second substitution you apply to that will again change a to something else (b, in your case) so you end up to \b. c.

Probably, your code performs an overall even number of substitutions there, which makes the variable change as follows \y, \a, \b, \a, \b, ... the last being \b since it's the last after an even number of changes.

Anyway, it does not matter which name you use as long as you are consistent with your variable renaming. The final result will be correct anyway.

Personally, I like to be more conservative and to avoid alpha-converting variables unless there's a need to do so, which avoids that ping-pong effect, but that's only a matter of taste.

Capture-avoiding substitution function — Lambda calculus

2 Answers