无法在 Haskell 中获得完全的 beta 减少

Question

我目前正在尝试在 Haskell 中实现 beta 缩减，但遇到了一个小问题。我已经设法弄清楚其中的大部分，但是现在我在测试时遇到了一个小错误，我不知道如何解决它。

代码使用了我预先定义的自定义数据类型 Term 和替换函数，这两个都将在下面。

--Term datatype
data Term = Variable Var | Lambda Var Term | Apply Term Term

--Substitution function
substitute :: Var -> Term -> Term -> Term
substitute x n (Variable m)
    |(m == x) = n
    |otherwise = (Variable m)
substitute x n (Lambda m y)
    |(m == x) = (Lambda m y)
    |otherwise = (Lambda z (substitute x n (rename m z y)))
    where z = fresh (merge(merge(used y) (used n)) ([x]))
substitute x n (Apply m y) = Apply (substitute x n m) (substitute x n y)

--Beta reduction
beta :: Term -> [Term]
beta (Variable x) = []
beta (Lambda x y) =  map (Lambda x) (beta y)
beta (Apply (Lambda x m) n) = [(substitute x n m)] ++ [(Apply (Lambda x n) m) | m <- beta m] ++ [(Apply (Lambda x z) m) | z <- beta n]
beta (Apply x y) = [Apply x' y | x' <- beta x] ++ (map (Apply x) (beta y))

预期结果如下：

*Main> Apply example (numeral 1)
(\a. \x. (\y. a) x b) (\f. \x. \f. x)
*Main> beta it
[\c. (\b. \f. \x. \f. x) c b,(\a. \x. a b) (\f. \x. f x)]

但这是我的结果：

*Main> Apply example (numeral 1)
(\a. \x. (\y. a) x b) (\f. \x. \f. x)
*Main> beta it
[\c. (\b. \f. \x. \f. x) c b,(\a. \f. \x. \f. x) (\x. a b)]

任何帮助将不胜感激。

Answer 1

认为你的教堂数字编码错误，数字 1 应该返回

\f. \x. f x

而不是

\f. \x. \f. x.