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。是。根据 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

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