Hambell Beta Reduction in Lambda Calculus

Question

I have defined the following functions for beta reduction, but I'm not sure how to consider the case where free variables become 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 hammar link provided in the comment details the solution.

I just would like to propose another solution. Nicholas Govert de Broin , a Dutch mathematician, invented an alternative notation for lambda terms. The idea is that instead of using characters for variables, we use numbers. We replace each variable with a number representing how many lambdas we need to traverse until we find the abstraction that binds the variable. Abstractions then do not need to have any information at all. For instance:

 λx. λy. x 

converted to

 λ λ 2 

or

 λx. λy. λz. (xz) (yz) 

converted to

 λ λ λ 3 1 (2 1) 

This notation has several significant advantages. It is noteworthy that, since there are no variables, there is no renaming of variables, and there is no α-transformation. Although we must renumber indexes accordingly when replacing, we do not need to check for name conflicts and perform any renaming. The Wikipedia article above provides an example of how β-reduction works with these notations.