haskell - 为什么这个 lambda 演算缩减器不将 succ 0 缩减为 1？

Question

data Term = Var Integer
          | Apply Term Term
          | Lambda Term
          deriving (Eq, Show)

sub :: Term -> Integer -> Term -> Term
sub e v r = case e of
    Var x -> if x == v then r else e
    Apply m1 m2 -> Apply (sub m1 v r) (sub m2 v r)
    Lambda t -> Lambda (sub t (v + 1) r)

beta :: Term -> Term
beta t = case t of
    Apply (Lambda e) e' -> sub e 0 e'
    otherwise -> t

eta :: Term -> Term
eta t = case t of
    Lambda (Apply f (Var 0)) -> f
    otherwise -> t

reduce :: Term -> Term
reduce t = if t == t'
    then t
    else reduce t'
  where t' = beta . eta $ t

我尝试过:

let zero = Lambda $ Lambda $ Var 0
let succ = Lambda $ Lambda $ Lambda $ Apply (Var 1) $ (Apply (Apply (Var 2) (Var 1)) (Var 0))
reduce (Apply succ zero)

在 GHCi 中，但它似乎没有给我我正在寻找的表达式(Lambda (Lambda (Apply (Var 1) (Var 0)))。相反，它给了我:

Lambda (Lambda (Apply (Var 1) (Apply (Apply (Lambda (Lambda (Var 0))) (Var 1)) (Var 0))))

变量不是按名称编码，而是按需要向外走多少个 lambda 来获取参数。

Answer 1

您的 reducer 与 lambda 演算的通常评估方式相同，不会减少Lambda 项内的内容 - 它只会删除顶级 redexes。它产生的结果应该等价于一个，因为如果您将两者应用于相同的参数，您将得到相同的结果，但语法上不相同。