嵌套 “让” OCaml中表达

Question

所有：

我怎么能写在 “咖喱” 语法如下：

let y = 2 in 
let f x = x + y in 
let f x = let y = 3 in f y in 
f 5 

我在第一次尝试这样的事情：

(y -> (f -> ((f x -> f 5) (y -> f y) 3)) x + y) 2 

但是，这似乎并没有正确评估。

更好的是，Lambda表达式可以看到绑定。

谢谢！

Answer 1

let v = e1 in e2转换为lambda微积分为(\v.e2)(e1)（其中我使用反斜杠来表示lambda）。所以，你的例子是

(\y1.(\f1.(\f2.f2 5)(\x2.(\y2.f1(y2))(3)))(\x1.x1+y1))(2) 

我用alpha转换来区分变量，否则会有相同的名称。注意中间的f已变成f1，即f的f y在您的示例的第三行中使用了第二行中定义的f，而不是第三行中将要定义的那个。换句话说，你的定义不是递归的;您已使用let，而不是let rec。

Digression：将let rec转换为lambda演算需要一个固定点组合器Y（或一些类似技术）。 Y的特征是Y(f)简化为f(Y(f))。然后，let rec v = e1 in e2大致转换为(\v.e2)(Y(\v.e1))。