Wednesday, February 21, 2007

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.

No comments: