haskell - 如何在haskell中替换表达式中的变量？

Question

我正在使用在 haskell 中实现的 lambda 演算。表达式:

%x.e  -- lambda abstraction, like \x->e in Haskell
e e'  -- application
x,y,z -- variables
succ, pred, ifzero, 0, 1, 2....

语法:

type Id = String

-- The "builtin" functions.
data Op = Succ | Pred | IfZero
       deriving (Show, Ord, Eq)

-- Expressions of L
data Exp = Var Id
     | Nat Integer
     | Op Op
     | Lam Id Exp
     | App Exp Exp
       deriving (Ord, Eq, Show)

还有一个函数可以将通常的表示形式转换成Exp:

    parse "%f. f 1 2" = Lam "f" App (App (Var "f") (Nat 1)) (Nat 2)`

而且我必须编写函数 subst x e e' 将 e 替换为所有“免费”出现的 (Var x)在 e' 中。 “自由”意味着它不是由周围的 % 声明的变量。例如，在表达式中

x (%x. x (%y.xz)) (%y.x)

x 出现了 5 次。第一个是“免费”。第二个是 % 表达式的参数，永远不会被替换。第三次和第四次出现是指封闭的 % 表达式的参数。第五个是免费的。因此，如果我们将 0 替换为 x，我们将得到 0 (%x.x (%y.xz)) (%y.0)。

我需要使用的只是模式匹配和递归。我所能写的只是函数原型(prototype)

subst :: Id -> Exp -> Exp -> Exp
subst x (App z z') (App e e') =

如果有人能给我提示如何实现该功能，那就太好了。非常感谢任何帮助

Answer 1

我想首先指出模式匹配 (subst x (App z z') (App e e')) 是非穷尽的。 (大部分)其他模式都是微不足道的，所以很容易忘记它们。我建议不要对第三个参数进行模式匹配，因为如果你所做的只是将它代入第二个参数，你就不会关心它是 Application 还是 Natural.

大多数递归函数的第一步是考虑案例。什么是基本情况？在这种情况下，第二个参数等于 Var x:

-- Replace x with y in a Var. If the Var is equal to x, replace
-- otherwise, leave alone.
subst x (Var a) y
    | a == x    = y
    | otherwise = (Var a)

然后我们需要考虑步骤情况，如果是应用程序怎么办，如果是 lambda 抽象怎么办？

-- Replace x with y in an application. We just need to replace
-- x with y in z and in z', because an application doesn't
-- bind x (x stays free in z and z').
subst x (App z z') y = (App new_z new_z')
    where new_z  = -- Recursively call subst here.
          new_z' = -- And recursively call subst here, too.

-- Replace x with y in a lambda abstraction. We *do* need to
-- check to make sure that the lambda doesn't bind x. If the
-- lambda does bind x, then there's no possibility of x being
-- free in e, and we can leave the whole lambda as-is.
subst x (Lam z e) y
    | z == x    = (Lam z e)
    | otherwise = (Lam z new_e)
                  where new_e = -- Recursively call subst here.

最后，所有微不足道的情况都是相同的(我们不理会 Nat 和 Op，因为我们不可能替换它们):

subst :: Id -> Exp -> Exp -> Exp
subst _ nat_or_op _ = nat_or_op