haskell - 在 lambda 演算中编写用于重命名术语的递归函数

Question

我尝试编写一个函数来重命名 Lambda 演算术语中的变量名。重命名操作是 M[y/x]（M 与 x 重命名为 y）。

问题在于，在这些代码行中 | z == x = y， where newN = rename(n)、where newZ1 = rename(newZ1)和newZ2 = rename(newZ2)。

| z == x = y出现类型错误Expected type: Term Actual type: Var。请你能帮我理解为什么我会收到这个错误吗？

其他三个错误来自我尝试递归调用重命名函数时。我得到错误• Probable cause: ‘rename’ is applied to too few arguments。当我写这篇文章时，我认为它会根据为变量设置的大小写将变量重命名为。我该如何正确地做到这一点，干杯。

type Var = String

data Term =
    Variable Var
  | Lambda   Var  Term
  | Apply    Term Term
--  deriving Show

instance Show Term where
  show = pretty

example :: Term
example = Lambda "a" (Lambda "x" (Apply (Apply (Lambda "y" (Variable "a")) (Variable "x")) (Variable "b")))


pretty :: Term -> String
pretty = f 0
    where
      f i (Variable x) = x
      f i (Lambda x m) = if i /= 0 then "(" ++ s ++ ")" else s where s = "\\" ++ x ++ ". " ++ f 0 m 
      f i (Apply  n m) = if i == 2 then "(" ++ s ++ ")" else s where s = f 1 n ++ " " ++ f 2 m

rename :: Var -> Var -> Term -> Term
rename x y (Variable z)     
    | z == x    = y
    | otherwise = (Variable z)

rename x y (Lambda z n)
    | z == x    = (Lambda z n)
    | otherwise = (Lambda z newN)
                  where newN = rename(n)

rename x y (Apply  n m) = (Apply newZ1 newZ2)
    where newZ1 = rename(newZ1)
          newZ2 = rename(newZ2)

标签： haskell

Answer 1

错误的原因与消息中所说的完全一样。在引用整个错误的定义之后，我将通过它们：

rename :: Var -> Var -> Term -> Term
rename x y (Variable z)     
    | z == x    = y
    | otherwise = (Variable z)

rename x y (Lambda z n)
    | z == x    = (Lambda z n)
    | otherwise = (Lambda z newN)
                  where newN = rename(n)

rename x y (Apply  n m) = (Apply newZ1 newZ2)
    where newZ1 = rename(newZ1)
          newZ2 = rename(newZ2)

正如您所报告的，第一个错误是type error Expected type: Term Actual type: Var, on the line | z == x = y。

这完全是由于这种情况下的返回值y，它的类型是Var。然而你的签名说返回值必须有 type Term。这可以通过替换来解决y，Variable y就像您z在下一行所做的那样。

至于其他的，GHC 的建议在我看来又是正确的：rename在进行递归调用时，您没有应用足够的参数。rename具有 type Var -> Var -> Term -> Term，这意味着当应用于单个参数（假定为 type Var）时，如在您的rename(n)（可以更简洁地写为rename n）中，您将获得 type 的值Var -> Term -> Term，而不是Term您显然想要的 type 之一。为此，您必须应用rename3 个参数（适当类型的），而不仅仅是 1 个。

以下将修复提到的错误 - 尽管我没有测试它是否有更多错误，我也不能完全确定我已经理解了你的函数的预期行为（尽管我对此有点信心）。

我还删除了一些不必要的括号，并重新定义newZ1并newZ2成为我相信你的意图，而不是根据它们本身来定义。

rename :: Var -> Var -> Term -> Term
rename x y (Variable z)     
    | z == x    = Variable y
    | otherwise = Variable z

rename x y (Lambda z n)
    | z == x    = Lambda z n
    | otherwise = Lambda z newN
                  where newN = rename x y n

rename x y (Apply  n m) = Apply newZ1 newZ2
    where newZ1 = rename x y n
          newZ2 = rename x y m