问题描述
所以我得到了下面的替代函数，我试图用它替换 b 中的教堂数字 0 示例术语：
\a。 \X。 (\y.a) x b
*Main> 替换“b”（数字 0）示例
目前正在给我：
\c. \一种。 (\b. c) a (\f. \x. x)
但是我希望答案是：
\c. \一种。 (\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 中是 free，所以用 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,... 最后一个是 \b，因为它是偶数次更改后的最后一个。
无论如何，只要您与您的变量重命名一致，您使用哪个名称都没有关系。无论如何，最终结果将是正确的。
就我个人而言，我喜欢更加保守并避免使用 alpha 转换变量，除非有必要这样做，这样可以避免乒乓效应，但这只是个人喜好问题。