ansaurus

Question

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

Answer 1

+3 A:

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.

sepp2k 2010-10-28 09:35:37

Thanks for the response sepp2K. You have pretty much gotten the gist of what I am trying to do. But the part that I was having trouble fully implementing is the beta_reduce. Here you have injected a function called subst that does the same thing that beta_reduce would do without explaining how subst would be implemented. Which leaves me in the same position as before.

klactose 2010-10-28 18:40:31

Other than that though, your code is pretty representative of how mine looks.

klactose 2010-10-28 18:42:35

Oh and one more thing... shouldn't you your App case end with eval(beta_reduce(x,e) arg)? Otherwise wouldn't we simply be returning the function without actually applying it?

klactose 2010-10-28 18:54:57

@klactose: I updated my answer to explain how to implement `subst`. And yes, of course it should call eval on the result of the substitution. Silly mistake.

sepp2k 2010-10-28 18:59:04

Thanks for your input sepp2k. I'm not certain that I understand what you mean when you suggest that subst should call itself recursively on both subexpressions of a function application. My function application looks like this: App(expr1, expr2). While expr1 should be a Lambda epression, expr2 is the value that should be replacing the variable in the lambda. So if subst takes 3 parameters, what parameters would be used for the recursive calls for non-lambda expressions??? Sorry for the long response!

klactose 2010-10-29 04:08:19

I hope that question made sense to you

klactose 2010-10-29 04:09:21

@klactose: You're saying "expr1 should be a lambda expression". That's not necessarily correct though. `((lambda x. x) y) z` is a valid expression, which should be parsed as something like `App ( App (Lambda ("x", Var "x"), Var "y") Var "z"`. Here the outer `App` has as its first argument an `App`, not a `Lambda` and that's perfectly valid.

sepp2k 2010-10-29 14:28:48

Then you're saying "expr2 is the value that should be replacing the variable in the lambda". That's correct in a sense, but technically expr2 is an *expression* which, when evaluated, will return the value that you want to substitute (and that value might very well be a lambda itself - in the pure lambda calculus that would be the only possible kind of value).

sepp2k 2010-10-29 14:31:01

So what I'm trying to say is: Both `expr1` and `expr2` should have type `expression` (and if your definition of `expression` looks like the one in my answer, they will), so you can use them as the third argument for `subst` without a problem.

sepp2k 2010-10-29 14:32:20

ansaurus

tags:

views:

answers:

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

related questions