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

问题描述

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

我知道我需要一个匹配的模式案例来查看 item 是否可简化，如果不是，则为变量、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)]

解决方法

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

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

变量不会减少 beta，所以这种情况应该很容易。

beta (Lambda var term) = ...

Lambda 只有在它们的 body 减少时才会减少。在 term 开始递归。

beta (Apply term1 term2) = ...

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

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

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

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