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反复减少一个项，直到它不能再减少为止。那么，实际上将项减少一次的函数在哪里？

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在我的示例术语上生成一个无限列表，并且永远找不到正常形式。