是否可以通过修改这个简单的 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 可以具有的许多不同的评估策略（按名称调用、惰性评估、按值调用、按共享调用, 部分求值等等)?

Answer 1

直呼名字只需稍作改动：

不评估 lambda 抽象的主体：reduce (Lam body) = (Lam body)。

不评估应用程序的参数。相反，我们应该按原样替换它：

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

按需调用（又名惰性求值）似乎更难（或者可能不可能）以完全声明的方式实现，因为我们需要记住表达式的值。我没有看到通过微小的改变来实现它的方法。

共享调用不适用于简单的lambda演算，因为我们这里没有对象和赋值。

我们也可以使用完整的 beta 缩减，但我们需要选择一些确定的评估顺序（我们不能选择 "arbitrary" redex 并使用我们现在的代码对其进行缩减）。这种选择将产生一些评估策略（可能是上述之一）。

Answer 2

话题很广泛。我就写几个想法吧。

提议的reduce执行并行重写。也就是说，它将 App t1 t2 映射到 App t1' t2'（前提是 t1' 不是抽象）。 CBV 和 CBN 等一些策略更具顺序性，因为它们只有一个 redex。

为了描述它们，我会修改 reduce 以便 returns 是否确实进行了归约，或者该术语是否为范式。这可以通过返回 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)

懒人评价（附分享）不能用术语表达，没记错的话。它需要图表来表示正在共享子项。

是否可以通过修改这个简单的 reducer 来展示不同的评估策略？

Is it possible to showcase the different strategies of evaluation by modifying this simple reducer?

haskell

lambda

functional-programming

lazy-evaluation

lambda-calculus