CODEWITHSUNDEEP
haskelllambda-calculus
user3133295
user3133295

Reputation: 313

Why doesn't this lambda calculus reducer reduce succ 0 to 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

I tried:

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)

In GHCi, but it didn't seem to give me the expression for one (Lambda (Lambda (Apply (Var 1) (Var 0)) that I'm looking for. Instead it gives me:

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

The variables are encoded not by name, but by how many lambdas you need to walk outwards to get the parameter.

Upvotes: 4

Views: 582

Answers (1)

Ganesh Sittampalam
Ganesh Sittampalam

Reputation: 29100

Your reducer, in common with the way lambda calculus is normally evaluated, doesn't reduce inside Lambda terms - it only removes top-level redexes. The result it produces should be equivalent to one, in that if you apply both to the same arguments you will get the same result, but not syntactically identical.

Upvotes: 3

Related Questions