Haskell 将递归步骤保存到列表中

Question

我正在研究 Haskell lambda 演算解释器。我有一种方法可以将表达式简化为正常形式。

type Var = String

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

normal :: Term -> Term
normal (Variable index)      = Variable index
normal (Lambda var body)       = Lambda var (normal body)
normal (Apply left right) = case normal left of
    Lambda var body  -> normal (substitute var (normal right) body)
    otherwise -> Apply (normal left) (normal right)

如何将采取的步骤保存到集合中？

我的正常功能输出如下： \a. \b. a (a (a (a b))) 我的目标是完成所有步骤：

(\f. \x. f (f x)) (\f. \x. f (f x)),
\a. (\f. \x. f (f x)) ((\f. \x. f (f x)) a),
\a. \b. (\f. \x. f (f x)) a ((\f. \x. f (f x)) a b),
\a. \b. (\b. a (a b)) ((\f. \x. f (f x)) a b),
\a. \b. a (a ((\f. \x. f (f x)) a b)),
\a. \b. a (a ((\b. a (a b)) b)),
\a. \b. a (a (a (a b)))]

我尝试将普通方法封装到列表中，如下所示：

normal :: Term -> [Term]
normal (Variable index)      = Variable index
normal (Lambda var body)       = term: [Lambda var (normal body)]
normal (Apply left right) = case normal left of
    Lambda var body  -> normal (substitute var (normal right) body)
    otherwise -> Apply (normal left) (normal right)

但这似乎不是正确的方法。

Answer 1

我认为你是本末倒置。 normal 反复减少一个术语，直到它不能再减少为止。那么，真正减少一个术语once的函数在哪里？

reduce :: Term -> Maybe Term -- returns Nothing if no reduction
reduce (Variable _) = Nothing -- variables don't reduce
reduce (Lambda v b) = Lambda v <$> reduce b -- an abstraction reduces as its body does
reduce (Apply (Lambda v b) x) = Just $ substitute v x b -- actual meaning of reduction
reduce (Apply f x) = flip Apply x <$> reduce f <|> Apply f <$> reduce x -- try to reduce f, else try x

然后

normal :: Term -> [Term]
normal x = x : maybe [] normal (reduce x)

或者，更准确一点

import Data.List.NonEmpty as NE
normal :: Term -> NonEmpty Term
normal = NE.unfoldr $ (,) <*> reduce

---

请注意，reduce 的此定义还纠正了您原来的 normal 中的一个错误。有些术语具有您的normal 无法评估的正常形式。考虑这个词

(\x y. y) ((\x. x x) (\x. x x)) -- (const id) omega

这标准化为\y. y。根据substitute 的实现方式，您的normal 可能会成功或无法规范化该术语。如果它成功了，它就会被懒惰所拯救。 normal 的假设“步进”版本，在替换之前规范化参数，肯定无法规范化。

避免在替换之前减少参数保证您将找到任何术语的范式，如果存在范式。您可以使用

恢复急切的行为

eagerReduce t@(Apply f@(Lambda v b) x) = Apply f <$> eagerReduce x <|> Just (substitute v x b)
-- other equations...
eagerNormal = NE.unfoldr $ (,) <*> eagerReduce

正如承诺的那样，eagerNormal 在我的示例术语上生成一个无限列表，并且永远找不到正常形式。

Answer 2

您在正确的轨道上，但您还需要做很多事情。请记住，如果您将函数的类型从Term -> Term 更改为Term -> [Term]，那么您需要确保对于任何输入Term，该函数都会产生一个输出[Term]。但是，在 normal 的新实现中，您只对一种情况进行了更改（这样做时，您创建了一些名为 term 的新值——不知道为什么要这样做）。

所以，让我们考虑一下整个问题。当输入为Variable index 时，normal 应生成的Term 列表是什么？好吧，没有工作要做，所以它应该是一个单例列表：

normal' (Variable index) = [Variable index]

Lambda var body 怎么样？你写了term: [Lambda var (normal' body)]，但这没有任何意义。请记住，normal' body 现在正在生成一个列表，但 Lambda 不能将术语列表作为其主体参数。你试图将这个term 值加入你的单例列表是什么？

致电normal' body 是个好主意。这会产生一个Terms 的列表，它代表身体的部分标准化。但是，我们想要生成 lambda 的部分归一化，而不仅仅是主体。因此，我们需要修改列表中的每个元素，将其从 body 转换为 lamdba：

normal' (Lambda var body) = Lambda var <$> normal' body

万岁！ （请注意，由于我们在此步骤中没有进行任何实际的归一化，因此我们不需要增加列表的长度。）

（为了编码方便，对于最后一种情况，我们将逆序构造部分项的列表，以后可以随时逆序。）

最后一种情况是最难的，但它遵循相同的原则。我们首先认识到递归调用 normal' left 和 normal' right 将返回结果的列表，而不仅仅是最后一项：

normal' (Apply left right) =
  let lefts  = normal' left
      rights = normal' right

这引发的一个问题是：我们首先采取哪些评估步骤？我们先选择评估left。这意味着left 的所有评估步骤必须与原始right 配对，right 的所有评估步骤必须与评估最多的left 配对。

normal' (Apply left right) =
  let lefts  = normal' left
      rights = normal' right
      lefts'  = flip Apply right <$> lefts
      rights' = Apply (head lefts) <$> init rights
      evalSoFar = rights' + lefts'

注意最后使用init rights——因为rights的最后一个元素应该等于right，并且我们已经有了一个值，其头部为lefts，最后一个元素为rights在lefts' 中，我们在构建rights' 时省略了rights 的最后一个元素。

从这里开始，我们需要做的就是实际执行我们的替换（假设head lefts 确实是一个Lambda 表达式）并将我们的evalSoFar 列表连接到它产生的内容：

normal' (Apply left right) =
  let lefts  = normal' left
      rights = normal' right
      lefts'  = flip Apply right <$> lefts
      rights' = Apply (head lefts) <$> init rights
      evalSoFar = rights' ++ lefts'
  in case (lefts, rights) of
    (Lambda var body : _, right' : _) -> normal' (substitute var right' body) ++ evalSoFar
    _ -> evalSoFar

请记住，这会向后生成列表，因此我们可以如下定义 normal：

normal :: Term -> [Term]
normal = reverse . normal'

---

考虑到您没有提供substitute 的定义，我很难对此进行准确测试，但我很确定它应该满足您的需求。

也就是说，我会注意到，我从评估您的示例术语中得到的评估步骤与问题中给出的评估步骤不相同。具体来说，您的第二个评估步骤，从

\a. (\f. \x. f (f x)) ((\f. \x. f (f x)) a),
\a. \b. (\f. \x. f (f x)) a ((\f. \x. f (f x)) a b),

根据您的实现似乎是错误的。请注意，在这里您在完全评估参数之前执行替换。如果您运行此答案中的代码，您会看到您得到的结果不执行此步骤，而是在替换之前完全评估函数参数（即((\f. \x. f (f x)) a)）。 p>

Answer 3

当我想“我希望计算在进行过程中产生额外的信息”时，我会说：“当 Writer 就在那儿时，我为什么要手动实现呢？”当您主要只对一对中的一半感兴趣时，Writer 是生成一对的方法，而另一半是您像日志一样附加到的一些结构。

你没有提供substitute，我也不想实现，所以我自己写了一个简单的语言来减少。这也让您可以练习将相同的技术应用于您的语言。

import Control.Monad.Trans.Writer.Lazy (Writer, runWriter, tell, censor)

data Sum = Number Int
         | Sum :+ Sum

instance Show Sum where
  show (Number n) = show n
  show (x :+ y) = "(" ++ show x ++ " + " ++ show y ++ ")"

除了通常的 Applicative/Monad 组合器之外，我们需要实现它的关键 Writer 函数是 tell 和 censor。 tell 很无聊：它只是说“将其附加到日志中”。 censor 很有趣：它运行另一个 Writer 并返回该 Writer 的输出，但它也修改了该 Writer 生成的日志。

我们的想法是每次我们进行约简时都使用tell 记录术语，并使用censor 确保记录的子术语正确放置在整体计算的上下文中。

normalize :: Sum -> Writer [Sum] Sum
normalize root = tell [root] *> go root
  where go n@(Number _) = pure n
        go ((Number left) :+ (Number right)) =
          let sum = (Number (left + right))
          in tell [sum] *> pure sum
        go (left :+ right) = do
          left' <- censor (map (:+ right)) (go left)
          right' <- censor (map (left' :+)) (go right)
          go $ left' :+ right'

为此，请注意我们唯一的tell（除了在根处，以显示原始表达式）是在两个操作数都已归约的情况下，因此我们可以进行一些简化。在非归约情况下，我们简单地将两个操作数标准化，将生成的任何日志放入更广泛的上下文中。当然，您的语言有不同的缩减步骤；只要您确保在直接简化某些内容时准确地记录某些内容，您就不会出现重复或丢失的步骤。我认为你做过的唯一减少就是替换，所以这应该很简单。

请注意，这会产生理想的结果：

main = print . runWriter . normalize $
  (Number 1 :+ Number 2) :+ (Number 3 :+ (Number 4 :+ Number 5))

$ runghc tmp.hs
(15,[((1 + 2) + (3 + (4 + 5))),(3 + (3 + (4 + 5))),(3 + (3 + 9)),(3 + 12),15])

这里返回的对在左侧包含预期结果 (Number 15)，在右侧包含应用的一组缩减，按照它们完成的顺序。