Lambda演算Haskell的Beta转换

Question

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表达式根本不会被缩减，这意味着函数的输入和输出是相同的。

1. 如果使用第一个函数而不添加最后一个大小写，则为非穷尽模式
2. 或完全相同的表达式App(ABS1(ABS2(VAR1)))(VAR3)，如果添加最后一个例子
，它显然不会减少

谁能帮我弄清楚这件事吗？：）

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)

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

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

如果替换的结果是一个应用术语，会发生什么？会对结果进行评估吗？

编辑

关于您的更改，给定Lamapp e1 e2，您之前遵循的是按值调用的评估策略（即在替换之前评估e2)。那就没了，

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

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

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