In the comments to the OP it has been pointed out by the kind @PasqualCuoq that λ
in lambda calculus associates the same as fun
in OCaml. That is, the term t in λx.t
is evaluated greedily (see http://en.wikipedia.org/wiki/Lambda_calculus#Notation).
What this is means is that (λz.y z)
is actually (λz.(y z))
, and that the function above is correct, but the translation provided for the sample expression (λx.(x (λz.y z))) x
isn't, as it should've been
(App(Abs("x", App(Var "x", Abs("z", App(Var "y", Var "z")))), Var "x"))
in place of
(App(Abs ("x", App (Abs ("z", Var "y"), Var "z")), Var "x"))
Here's to this awesome place called Stack Overflow!