修改这个简单的reducer，展示不同的评估策略，是否有可能？

Question

我更喜欢通过查看代码来学习，而不是阅读冗长的解释。这可能是我不喜欢长篇学术论文的原因之一。代码明确、简洁、无噪音，如果你不理解某些东西，你可以直接尝试操作它 - 不需要问作者。

这是Lambda演算的完整定义：

-- A Lambda Calculus term is a function, an application or a variable.
data Term = Lam Term | App Term Term | Var Int deriving (Show,Eq,Ord)

-- Reduces lambda term to its normal form.
reduce :: Term -> Term
reduce (Var index)      = Var index
reduce (Lam body)       = Lam (reduce body)
reduce (App left right) = case reduce left of
    Lam body  -> reduce (substitute (reduce right) body)
    otherwise -> App (reduce left) (reduce right)

-- Replaces bound variables of `target` by `term` and adjusts bruijn indices.
-- Don't mind those variables, they just keep track of the bruijn indices.
substitute :: Term -> Term -> Term
substitute term target = go term True 0 (-1) target where
    go t s d w (App a b)             = App (go t s d w a) (go t s d w b)
    go t s d w (Lam a)               = Lam (go t s (d+1) w a) 
    go t s d w (Var a) | s && a == d = go (Var 0) False (-1) d t 
    go t s d w (Var a) | otherwise   = Var (a + (if a > d then w else 0))

-- If the evaluator is correct, this test should print the church number #4.
main = do
    let two = (Lam (Lam (App (Var 1) (App (Var 1) (Var 0)))))
    print $ reduce (App two two)

我认为上面的“reduce”函数比几页的解释更能说明Lambda演算，当初学习时我希望能够直接看它。你还可以看到它实现了非常严格的计算策略，甚至在抽象中也是如此。在这种精神下，如何修改该代码以说明LC可能具有的许多不同评估策略（按名称调用、惰性评估、按值调用、按共享调用、部分评估等）？

- MaiaVictor

---

非常有趣的主题，不过我怀疑这个问题是否符合 StackOverflow 的指南要求。 - leftaroundabout

@leftaroundabout，实际上我也有一些疑问。但是，我认为这可以被视为一个编程问题，因为底部的问题询问如何调整代码以适应多种策略（可能以一种优雅的方式）。这不仅仅是关于λ演算。 - chi

Answer 1

"Call-by-name需要做出一些改变："

1. Not evaluating the body of a lambda abstraction: reduce (Lam body) = (Lam body).

2. Not evaluating the argument of the application. Instead, we should substitute it as is:

   reduce (App left right) = case reduce left of
       Lam body -> reduce (substitute right body)
   

Call-by-need（也称惰性求值）似乎更难（或者可能不可能）以完全声明性的方式实现，因为我们需要记忆化表达式的值。我没有看到通过小改变来实现它的方法。

在简单的λ演算中，共享调用不适用，因为这里没有对象和赋值。

我们还可以使用完整的β缩减，但是我们需要选择一些确定性的评估顺序（我们不能选择“任意”红式并使用我们现有的代码来减少它）。这个选择将产生某种评估策略（可能是上述描述的其中一个）。

- kraskevich

Answer 2

这个主题非常广泛，我只会写一些想法。

所提出的reduce执行并行重写。也就是说，它将App t1 t2映射到App t1' t2'（前提是t1'不是抽象）。某些策略，例如CBV和CBN更加顺序化，因为它们只有一个可减少表达式。

为了描述它们，我会修改reduce，使其返回是否实际进行了缩减，或者该项是否为正常形式。这可以通过返回Maybe Term来完成，其中Nothing表示正常形式。

以这种方式，CBN将是

reduce :: Term -> Maybe Term
reduce (Var index)            = Nothing   -- Vars are NF
reduce (Lam body)             = Nothing   -- no reduction under Lam
reduce (App (Lam body) right) = Just $ substitute right body
reduce (App left right) = 
      (flip App right <$> reduce left) <|>  -- try reducing left
      (App left       <$> reduce right)     -- o.w., try reducing right

虽然CBV就是

reduce :: Term -> Maybe Term
reduce (Var index)            = Nothing
reduce (Lam body)             = Nothing   -- no reduction under Lam
reduce (App (Lam body) right) 
     | reduce right == Nothing            -- right must be a NF
     = Just $ substitute right body
reduce (App left right) = 
      (flip App right <$> reduce left) <|>
      (App left       <$> reduce right)

懒惰求值（带共享）不能使用术语来表达，如果我没记错的话。它需要使用图形来表示子术语正在被共享。

- chi