Beta reduction in lambda calculus using Haskell

Question

I have defined the following functions for beta reduction but i'm not sure how to consider the case where free variables get bounded.

data Term = Variable Char | Lambda Char Term | Pair Term Term deriving (Show,Eq)
--substition
s[M:x]= if (s=x) then M else s
AB[M:x]= (A[M:x] B [x:M])
Lambda x B[M:x] = Lambda x B 
Lambda y P[M:x]= if x=y then Lambda y P else Lambda y P (M:x) 



--beta reduction
Reduce [s]= s
Reduce[Lambda x B]M = B[M:x]
Reduce[L1 L2] = (Reduce [L1] Reduce [L2])

Answer 1

The link hammar gave in the comment describes the solution in detail.

I'd just like to offer a different solution. Nicolaas Govert de Bruijn, a Dutch mathematician, invented an alternative notation for lambda terms. The idea is that instead of using symbols for variables, we use numbers. We replace each variable by the number representing how many lambdas we need to cross until we find the abstraction that binds the variable. Abstraction then don't need to have any information at all. For example:

λx. λy. x

is converted to

λ λ 2

or

λx. λy. λz. (x z) (y z)

is converted to

λ λ λ 3 1 (2 1)

This notation has several considerable advantages. Notably, since there are no variables, there is no renaming of variables, no α-conversion. Although we have to renumber the indices accordingly when substituting, we don't have to check for names conflicts and do any renaming. The above Wikipedia article gives an example of how a β-reduction works with this notation.