EOPL - 2.2.2 - Exercise 2.12

This one asks you to implement alpha, beta and eta conversion on lambda-calculus expressions based on the substitution function of the previous exercise. For this we need a function to see if an identifier occurs free in an expression, similar to the one presented on section 1.3 and easy enough. The conversion functions can then be implemented quite simply:

let rec occurs_free v exp =
   match exp with
     Identifier i when v = i -> true
   | Lambda (x, e) when v <> x -> occurs_free v e
   | App (e1, e2) -> (occurs_free v e1) || (occurs_free v e2)
   | Prim (p, e1, e2) -> (occurs_free v e1) || (occurs_free v e2)
   | _ -> false

let alpha_conversion exp new_id =
   match exp with
     Lambda (id, body) when not (occurs_free new_id body) ->
         Lambda (new_id, lambda_calculus_subst body (Identifier new_id) id)
   | _ -> exp
  
let beta_conversion exp =
   match exp with
     App (Lambda (id, body), e) -> lambda_calculus_subst body e id
   | _ -> exp
  
let eta_conversion exp =
   match exp with
     Lambda (id, App (e, Identifier id'))
     when (id=id') && (not (occurs_free id e)) -> e
   | _ -> exp

These conversion functions simply return the same expression if they aren't of the right form. They could signal an error, depending on the application.