Beta Conversion for Lambda Calculus Haskell

Question

I want to implement a function which does beta reduction to a lambda expression where my lambda expression is of the type:

data Expr = App Expr Expr | Abs Int Expr | Var Int deriving (Show,Eq)

My evaluation function so far is:

eval1cbv :: Expr -> Expr
eval1cbv (Var x) = (Var x)
eval1cbv (Abs x e) = (Abs x e)
eval1cbv (App (Abs x e1) e@(Abs y e2)) = eval1cbv (subst e1 x e)
eval1cbv (App e@(Abs x e1) e2) =  eval1cbv (subst e2 x e)  
eval1cbv (App e1 e2) = (App (eval1cbv e1) e2)

where subst is a function used to define substitution.

However, when I try to reduce an expression using beta reduction I get a non-exhaustive patterns error and I cannot understand why. What I can do to fix it is adding an extra case at the bottom like this:

eval :: Expr -> Expr
eval (Abs x e) = (Abs x e)
eval (App (Abs x e1) e@(Abs y e2)) = subst e1 x e
eval (App e@(Abs x e1) e2) = App e (eval e2)
eval (App e1 e2) = App (eval e1) e2
eval (Var x) = Var x

However, if I do that then the lambda expression is not being reduced at all, meaning that the input is the same as the output of the function.

So, if I try to evaluate a simple case like:

eval (App (Abs 2 (Var 2)) (Abs 3 (Var 3))) it works fine giving -> Abs 3 (Var 3)

but when I run it for a bigger test case like:

eval (App (Abs 1 (Abs 2 (Var 1))) (Var 3)) i get:

1. non-exhaustive patterns if I use the first function without adding the last case
2. or the exact same expression App (Abs 1 (Abs 2 (Var 1))) (Var 3), which obviously does not get reduced, if I add the last case

Can anyone help me figure this out please? :)

Answer 1

but when I run it for a bigger test case like:

eval (App (Abs 1 (Abs 2 (Var 1))) (Var 3)) 

When you try to apply something of the form Abs x e to Var y, you're in this branch,

eval (App e@(Abs x e1) e2) = App e (eval e2)

so you have,

  App (Abs x e) (Var y)
= App (Abs x e) (eval (Var y))
= App (Abs x e) (Var y)

This is not what you want to do. Both (Abs x e) and (Var y) are in normal form (i.e. evaluated), so you should have substituted. You appear to only treat lambdas, and not variables, as evaluated.

---

There are more problems with your code. Consider this branch,

eval (App e1 e2) = App (eval e1) e2

The result is always an App. E.g. if eval e1 = Abs x e then the result is App (Abs x e) e2. It stops there, not further evaluation is performed.

And consider this branch,

eval (App (Abs x e1) e@(Abs y e2)) = subst e1 x e

What happens if the result of substitution is an application term? Will the result be evaluated?

---

EDIT

Regarding your changes, given LamApp e1 e2 you were following a call-by-value evaluation strategy before (i.e. you were evaluating e2 before substituting). That is gone,

Here it e2 is a lambda so it needs no evaluation,

eval1cbv (LamApp (LamAbs x e1) e@(LamAbs y e2)) = eval1cbv (subst e1 x e)

Here you substitute anyway regardless of what e2 is, so you do the exact same as before. You don't need the previous case then and are now following a call-by-name evaluation strategy. I don't know if that's what you want. Also you are calling subst with the wrong arguments here. I suppose you mean subst e1 x e2 and you don't need that @e.

eval1cbv (LamApp e@(LamAbs x e1) e2) =  eval1cbv (subst e2 x e)  

Here you are just evaluating the first argument which is consistent with a call-by-name strategy. But again I don't know if that's your intention.

eval1cbv (LamApp e1 e2) = (LamApp (eval1cbv e1) e2)