All:
How can I write the following in the "Curry" syntax:
let y = 2 in
let f x = x + y in
let f x = let y = 3 in f y in
f 5
I at first tried something like this:
(y -> (f -> ((f x -> f 5) (y -> f y) 3)) x + y) 2
However this does not seem evaluate properly.
Even better yet would be a Lambda-expression to see binding.
Thanks!
let v = e1 in e2 translates to lambda calculus as (\v.e2)(e1) (where I use the backslash to denote a lambda). So, your example would be
(\y1.(\f1.(\f2.f2 5)(\x2.(\y2.f1(y2))(3)))(\x1.x1+y1))(2)
I used alpha conversion to differentiate between variables that otherwise would have the same name. Observe that the f in the middle has become f1, that is the f in f y in the third line of your example uses the f defined in the second line, not the one which is about to be defined in the third line. In other words, your definition is not recursive; you have used let, not let rec.
Digression: Translating let rec into the lambda calculus requires a fixed point combinator Y (or some like technique). Y is characterized by the property that Y(f) reduces to f(Y(f)). Then, let rec v = e1 in e2 roughly translates to (\v.e2)(Y(\v.e1)).