4

在另一个问题中，Bob为无类型 lambda 演算提供了以下解释器。

data Expr = Var String | Lam String Expr | App Expr Expr

data Value a = V a | F (Value a -> Value a)

interpret :: [(String, Value a)] -> Expr -> Value a
interpret env (Var x) = case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> v
interpret env (Lam x e) = F (\v -> interpret ((x, v):env) e)
interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> f (interpret env e2)

Ivan Zakharyaschev 说这个解释器是按值调用的，因为F f -> f (interpret env e2). 名称调用解释器的实现与上面介绍的解释器有何不同？

Plotkin在 1970 年代研究了用于评估 lambda 演算的名称调用和值调用策略。

4

2 回答 2

5

我认为原始数据定义不可能进行正确的按名称调用。F (Value a -> Value a)hasValue a作为参数，所以我们别无选择，只能传入一些已经解释过的值，它会在 Haskell 缩减行为下按需调用。

我们可以修改数据定义：

data Value a = V a | F ((() -> Value a) -> Value a)

并且还让解释器返回显式的 thunk：

interpret :: [(String, () -> Value a)] -> Expr -> () -> Value a
interpret env (Var x) = delay (case lookup x env of
  Nothing -> error "undefined variable"
  Just v -> force v)
interpret env (Lam x e) = delay (F (\v -> force (interpret ((x, v):env) e)))
interpret env (App e1 e2) = delay (case force (interpret env e1) of
  V _ -> error "not a function"
  F f -> f (interpret env e2))

force :: (() -> a) -> a
force f = f ()
{-# NOINLINE force #-}

delay :: a -> () -> a
delay a () = a
{-# NOINLINE delay #-}

现在，我们不是在环境中存储一个 thunk，而是存储一个部分应用程序对象，然后在不同的调用站点分别评估它。

force并delay要求防止 GHC 浮出函数体，从而恢复共享。或者，可以{-# OPTIONS -fno-full-laziness #-}使用简单的 lambda 表达式和应用程序来代替上述机器进行编译和使用。

于 2015-03-01T08:07:32.337 回答
3

CBV/CBN 是与 lambda 演算的评估策略相关的概念，即与 lambda 项约简中 redex 的选择有关。在减少术语表示的操作式解释器中，您可以正确地说 CBV/CBN。

在像发布的那样的指称式解释器中，我会说急切与懒惰的语义，而不是 CBV/CBN。当然，eager 对应 CBV，lazy 对应 CBN。

由于 Haskell 是懒惰的，代码

interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> f (interpret env e2)

实现了惰性语义（CBN）。（正如 luqui 所说，在操作上，GHC 会以按需调用的方式减少这种情况）。

为了获得一个急切的（CBV）语义，我们可以在调用之前强制参数：

interpret env (App e1 e2) = case interpret env e1 of
  V _ -> error "not a function"
  F f -> case interpret env e2 of
         V v -> f v
         F g -> f g

这确保了不会将未评估的 thunk 馈送到函数，除非它们已经在环境中。但是，只有在评估 lambda 时才会填充环境，这将在环境中插入上面的vvalues g。因此，不会在那里插入任何 thunk。

于 2015-03-01T08:44:18.540 回答