所以我得到了下面的替换函数，我试图用它来替换中Church数字0的b示例术语：
\a。\x。(y.a(x b
*Main>替换"；b"；(数字0(示例
目前给我的是：
\c。\a。(\b.c(一个(\f.x.x(
然而，我期待的答案是：
\c。\a。(\a.c(a(\f.\x.x(
你能告诉我我在这里做错了什么吗，那是用新鲜的吗？？这里的替换函数似乎没有将这里的"a"视为新变量，因为它已经被用作之前x的替换？有什么办法绕过这个吗？
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
其中
used :: Term -> [Var]
used (Variable z) = [z]
used (Lambda z n) = merge [z](used n)
used (Apply n m) = merge (used n)(used m)
和
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
和
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
从lambda演算的角度来看，b在a. x. (y. a) x b中是自由的，因此用0代替b得到a. x. (y. a) x 0，如果0=f. x. x，则它是
a. x. (y. a) x (f. x. x)
===
c. x. (y. c) x (f. x. x)
===
c. x. (b. c) x (f. x. x)
你显然得到了
c. a. (b. c) a (f. x. x)
其中是相同的lambda项，直到alpha转换(一致捕获避免变量重命名(。
所以没有错误。
您的new_z以一种相当保守的方式被选择为新鲜的，因为您总是生成一个全新的变量名，并且永远不要重用术语中已经出现的变量，即使该变量可以重用而不会引起不必要的捕获。
更详细地说，当您替换y. a中的某个内容时，即使没有冲突，您也会将y更改为其他内容。
现在，由于Lambda用例的工作方式，您需要执行多个替换(注意嵌套的substitute x n (substitute y (Variable new_z) m)(。
所以，我想，当您将a重命名为c时，您的y. a将首先被alpha转换为a. c，正如您所期望的那样。然而，您应用的第二个替换将再次将a更改为其他内容(在您的情况下为b(，因此您最终将使用b. c。
可能，您的代码在那里执行了总体偶数的替换，这使得变量更改如下y, a, b, a, b, ...，最后一个是b，因为它是偶数次更改后的最后一个。
无论如何，使用哪个名称并不重要，只要您与变量重命名一致即可。无论如何，最终结果都是正确的。
就我个人而言，我喜欢更保守，避免阿尔法转换变量，除非有必要这样做，这样可以避免乒乓效应，但这只是品味的问题。