haskell - 为什么这个 lambda 演算 reducer 不能将 succ 0 减少到 1？

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 (Lambda (Apply (Var 1) (Var 0))) 我正在寻找的表达式。相反，它给了我:

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

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

最佳答案

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

关于haskell - 为什么这个 lambda 演算 reducer 不能将 succ 0 减少到 1？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/20937353/