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:

Post a Comment