lambda 演算的按值调用解释器和按名称调用解释器之间的区别

Question

在另一个问题中，Bob 提出了以下 interpreter for the untyped lambda calculus。

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 remarked 由于 F f -> f (interpret env e2)，该解释器是按值调用的。 按名称调用解释器的实现与上面介绍的解释器有何不同？

Plotkin 在 1970 年代研究 call-by-name and call-by-value strategies 以评估 lambda 演算。

Answer 1

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

我们可以修改数据定义：

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

还有解释器 return 明确的 thunks:

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，而是存储一个 partial application object，然后在不同的调用站点分别对其进行评估。

需要

force 和 delay 来防止 GHC 浮出函数体，thereby recovering sharing. 或者，可以使用 {-# OPTIONS -fno-full-laziness #-} 编译并使用简单的 lambda 和应用程序代替代替上面的机器。

Answer 2

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 时才会填充环境，这将在环境中插入上面的值 v、g。因此，不会在此处插入 thunk。

lambda 演算的按值调用解释器和按名称调用解释器之间的区别

Difference between call-by-value and call-by-name interpreter for the lambda calculus

haskell

lambda-calculus

callbyname

call-by-value