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

您走在正确的轨道上，但您需要做的还有很多。请记住，如果您将函数的类型从 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 是个好主意。这会生成一个 Term 的列表，它表示正文的部分规范化。但是，我们想要生成 lambda 的部分规范化，而不仅仅是主体。因此，我们需要修改列表中的每个元素，将其从 body 转换为 lamdba:

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

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

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

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

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 并且我们已经有了一个头部为 [=43 的值=]和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)) 替换之前。

Answer 2

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

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

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 and censor。 tell 非常无聊：它只是说“将此附加到日志”。 censor 很有趣：它运行另一个 Writer 和 returns 该 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) 和右侧应用的一组缩减，按它们完成的顺序排列。

Answer 3

我认为您是本末倒置。 normal 重复减少一个术语，直到不能再减少为止。那么，实际减少一项一次的函数在哪里？

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 在我的示例术语中生成了一个无限列表，并且从未找到范式。

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

Haskell save recursive steps into a list

haskell

lambda-calculus