Lambda 演算 Haskell 的 Beta 转换

Question

我想实现一个函数，它对 lambda 表达式进行 beta 缩减，其中我的 lambda 表达式属于以下类型：

data Expr = App Expr Expr | Abs Int Expr | Var Int deriving (Show,Eq)

到目前为止我的评价函数是：

eval1cbv :: Expr -> Expr
eval1cbv (Var x) = (Var x)
eval1cbv (Abs x e) = (Abs x e)
eval1cbv (App (Abs x e1) e@(Abs y e2)) = eval1cbv (subst e1 x e)
eval1cbv (App e@(Abs x e1) e2) =  eval1cbv (subst e2 x e)  
eval1cbv (App e1 e2) = (App (eval1cbv e1) e2)

其中subst 是一个用于定义替换的函数。

但是，当我尝试使用 beta 缩减来缩减表达式时，我得到了一个非详尽的模式错误，我不明白为什么。我可以做的是在底部添加一个额外的案例，如下所示：

eval :: Expr -> Expr
eval (Abs x e) = (Abs x e)
eval (App (Abs x e1) e@(Abs y e2)) = subst e1 x e
eval (App e@(Abs x e1) e2) = App e (eval e2)
eval (App e1 e2) = App (eval e1) e2
eval (Var x) = Var x

但是，如果我这样做，则 lambda 表达式根本不会被减少，这意味着输入与函数的输出相同。

所以，如果我尝试评估一个简单的案例，例如：

eval (App (Abs 2 (Var 2)) (Abs 3 (Var 3))) 它工作正常 -> 绝对值 3（变量 3）

但是当我为更大的测试用例运行它时：

eval (App (Abs 1 (Abs 2 (Var 1))) (Var 3)) 我得到：

1. 如果我使用第一个函数而不添加最后一个案例，则不是详尽的模式
2. 或完全相同的表达式 App (Abs 1 (Abs 2 (Var 1))) (Var 3)，如果我添加最后一种情况，显然不会减少

谁能帮我解决这个问题？ :)

Answer 1

但是当我为更大的测试用例运行它时：

eval (App (Abs 1 (Abs 2 (Var 1))) (Var 3)) 

当您尝试将Abs x e 形式的内容应用到Var y 时，您就在这个分支中，

eval (App e@(Abs x e1) e2) = App e (eval e2)

原来如此，

  App (Abs x e) (Var y)
= App (Abs x e) (eval (Var y))
= App (Abs x e) (Var y)

这不是你想做的。 (Abs x e) 和 (Var y) 都是正常形式（即已评估），因此您应该替换。您似乎只将 lambdas 视为已评估，而不是变量。

---

您的代码存在更多问题。考虑这个分支，

eval (App e1 e2) = App (eval e1) e2

结果始终是App。例如。如果eval e1 = Abs x e 则结果为App (Abs x e) e2。它停在那里，不进行进一步的评估。

考虑一下这个分支，

eval (App (Abs x e1) e@(Abs y e2)) = subst e1 x e

如果替换的结果是一个应用项会发生什么？是否会评估结果？

---

编辑

关于您的更改，鉴于 LamApp e1 e2 您之前遵循的是按值调用的评估策略（即，您在替换之前正在评估 e2）。没了，

这里e2 是一个 lambda，所以它不需要评估，

eval1cbv (LamApp (LamAbs x e1) e@(LamAbs y e2)) = eval1cbv (subst e1 x e)

不管e2 是什么，你都可以在这里替换，所以你做的和以前一样。那时您不需要前面的案例，现在正在遵循按名称调用的评估策略。我不知道这是否是你想要的。此外，您在这里使用错误的参数调用subst。我想你的意思是subst e1 x e2 而你不需要那个@e。

eval1cbv (LamApp e@(LamAbs x e1) e2) =  eval1cbv (subst e2 x e)  

在这里，您只是评估与按名称调用策略一致的第一个参数。但我不知道这是否是你的意图。

eval1cbv (LamApp e1 e2) = (LamApp (eval1cbv e1) e2)