How would you implement the beta recovery feature in F #?

Question

I write lambda calculus in F #, but I'm stuck on implementing beta reduction (replacing formal parameters with actual parameters).

(lambda x.e)f
--> e[f/x]

usage example:

(lambda n. n*2+3) 7
--> (n*2+3)[7/n]
--> 7*2+3

Therefore, I would like to hear some suggestions as to how others can do this. Any ideas would be greatly appreciated.

Thank!

Answer 1

Assuming your expression expression looks like

type expression = App of expression * expression
                | Lambda of ident * expression
                (* ... *)

you have a function subst (x:ident) (e1:expression) (e2:expression) : expressionthat replaces all free entries xwith e1in e2, and you want a normal order evaluation, your code should look something like this:

let rec eval exp =
  match exp with
  (* ... *)
  | App (f, arg) -> match eval f with Lambda (x,e) -> eval (subst x arg e)

The function substshould work as follows:

.

lambdas , , ( , ).

, , .