Lambda calculus expression

Question

Hi All,

For a lambda expression (x (λx y. x y) z h), I did not understand how free variables x (outer x), z and h can be converted in C code?

Regards, darkie

Answer 1

Converting lambda calculus to C code is non-trivial. Usually you'll write an interpreter, which evaluates step-by-step. That is, turn the expression into a tree, and find the node closest to the root that's an application with the left-hand-side being a lambda. Now substitute in the right hand side. Repeat until you can't apply any more, and you have the result.

Note that there's no direct equivalent to the free variables here; we're just using them to know where to substitute things.

Keep in mind that turing equivalence does not require exact equivalence between any concepts in two turing-complete languages. It simply requires that you be able to emulate one with the other, and vice versa.

Answer 2

Free variables are a special case in the Lambda Calculus -- they cannot be "converted" to anything, so usually they're taken as just symbols. In your example, and given some fictitious constructors for lambda expressions, you'd translate it to the following (which includes dealing with the implicit currying) C-like expression:

mk_app(mk_app(mk_app(mk_sym("x"),
                     mk_lam("x",
                            mk_lam("y",
                                   mk_app(mk_var("x"),
                                          mk_var("y"))))),
              mk_sym("z")),
       mk_sym("h"));

Obviously, you can use mk_var() for those symbols too, but that would be misleading since they're not really variables, since they're not bound. In other words, if you do any alpha conversion on the expression, they will have to stay the same.

(BTW, the relevant part here is Barendregt's free variable assumption.)