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

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)

在我看来,上面的"减少"功能更多地讲述了Lambda微积分而不是解释的页面,我希望在我开始学习时能够看到它.您还可以看到它实现了一种非常严格的评估策略,即使在抽象内部也是如此.在这种精神上,如何修改代码以说明LC可以具有的许多不同的评估策略(按名称,懒惰评估,按值调用,按分享调用,部分评估等等)上)？

Answer 1

Call-by-name 只需要进行一些更改：

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

2. 不评估应用程序的论点。相反，我们应该按原样替换它：

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

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

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

我们还可以使用完整的 beta 缩减，但是我们需要选择一些确定性的评估顺序（我们不能选择“任意”的 redex 并使用我们现在拥有的代码来缩减它）。这种选择将产生一些评估策略（可能是上述策略之一）。