How would you implement a beta-reduction function in F#?

Question

I am writing a lambda calculus in F#, but I am stuck on implementing the beta-reduction (substituting formal parameters with the actual parameters).

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

example of usage:

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

So I'd love to hear some suggestions in regards to how others might go about this. Any ideas would be greatly appreciated.

Thanks!

Answer 1

Assuming your representation of an expression looks like

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

, you have a function subst (x:ident) (e1:expression) (e2:expression) : expression which replaces all free occurrences of x with e1 in e2, and you want 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 subst function should work as follows:

For a function application it should call itself recursively on both subexpressions.

For lambdas it should call itself on the lambda's body expression unless the lambda's argument name is equal to the identifier you want to replace (in which case you can just leave the lambda be because the identifier can't appear freely anywhere inside it).

For a variable it should either return the variable unchanged or the replacement-expression depending on whether the variable's name is equal to the identifier.