Lambda Calculus Haskell的β转换

Question

我想要实现一个函数，它可以在我的lambda表达式的类型为这样的情况下，对lambda表达式进行beta缩减：

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)

但是当我运行一个更大的测试用例时，比如：

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 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)