时间戳

首页 > 解决方案 > Lambda 演算 Haskell 的 Beta 转换

haskell - Lambda 演算 Haskell 的 Beta 转换

问题描述

我想实现一个函数，它对 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)

wheresubst是用于定义替换的函数。

但是，当我尝试使用 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))) 它工作正常 -> 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)，如果我添加最后一种情况，显然不会减少

任何人都可以帮我解决这个问题吗？:)

标签： haskelllambda-calculus

解决方案

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

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)

推荐阅读