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

Question

我正在尝试提出一种算法，可以打印给定表达式的所有可用 Beta 缩减。
我知道我需要一个匹配的模式案例来查看 item 是否可简化，如果不是，则为变量、lambda 和应用程序的三个案例。我为这些定义了自定义类型，如下所示:

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

以前我已经实现了以下方法:
给定方法的功能如下:

合并

重命名重命名以避免变量捕获

替换减少表达式

新鲜给出了一个以前没有使用过的新变量

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，所以这种情况应该很容易。

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