Haskell 算法找到所有可能的 Beta 减少

Question

我正在尝试提出一种算法，可以打印给定表达式的所有可用的 beta 缩减。

我知道我需要一个匹配的模式案例来查看项目是否可约化，如果不是，则需要变量、lambda 和应用程序的三种案例案例。我为这些定义了自定义类型，如下所示：

data Term =
    Variable Var
  | Lambda   Var  Term
  | Apply    Term Term
  deriving Show

之前我已经实现了以下方法：

给定方法的功能如下：

• 合并
• 重命名重命名以避免变量捕获
• 替换减少表达式
• fresh 提供了一个以前未使用过的新变量
• used 返回给定表达式的所有使用变量

到目前为止，一切正常，但是，返回所有可能的 beta 减少的功能是我迷失的地方。我试图定义如下所示的四种大小写匹配模式，但是我正在努力定义 redex 案例（特别是查看其他 redex 的 redex）以及需要在 beta 方法中进行的操作。：

beta :: Term -> [Term]
beta (Variable var) = 
beta (Lambda var term) = 
beta (Apply term1 term2)

我现在不知道如何在此处进行以获得所有可用的折扣。结果应该是：

*Main> Apply (x y)
(\a. \x. (\y. a) x b) (\f. \x. f x)
*Main> beta it
[\c. (\b. \f. \x. f x) c b,(\a. \x. a b) (\f. \x. f x)]

Answer 1

这是一个非正式的描述，作为提示。

beta :: Term -> [Term]
beta (Variable var) = ...

变量不会进行 beta-reduce，所以这种情况应该很简单。

beta (Lambda var term) = ...

Lambdas 只有在他们的身体减少时才会减少。从term 的递归开始。

beta (Apply term1 term2) = ...

这是复杂的部分：我们这里有三个子案例。

• 如果term1 减少，则整个应用程序会相应减少。
• 如果term2 减少，则整个应用程序会相应减少。
• 如果term1 恰好是一个 lambda，那么您已经找到了一个 redex。您可以将 lambda 正文中的抽象变量替换为 term2。

整个代码可以遵循这个形状：

beta :: Term -> [Term]
beta (Variable var) = ...
beta (Lambda var term) = ...
beta (Apply term1 term2) = term1Moves ++ term2Moves ++ redexMoves
   where
   term1Moves = ...
   term2Moves = ...
   redexMoves = case term1 of
      Lambda var term -> ...
      _               -> []        -- no further moves

列表推导式使用起来很方便。

---

获取 OP 发布的部分代码，并添加更多提示，我们得到：

beta :: Term -> [Term]
beta (Variable var) = ...
beta (Lambda var term) = ...
beta (Apply term1 term2) = term1Moves ++ term2Moves ++ redexMoves
   where
   term1Moves = [ Apply term1' term2 | term1' <- beta term1 ]
   term2Moves = ...
   redexMoves = case term1 of
      Lambda var body -> [substitute var term2 body]  -- don't recurse here
      _               -> []        -- no further moves