如何在没有“let rec”的情况下定义y-combinator？
在几乎所有的例子中，ML型语言中的一个y-combinator是这样写的：
let rec yfx = f (yf) x let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1)) 这可以像预期的那样工作，但是使用let rec ...来定义y-combinator感觉就像是在作弊。
我想定义这个组合子，而不使用recursion，使用标准的定义：
Y = λf·(λx·f (xx)) (λx·f (xx))
直接翻译如下：
let y = fun f -> (fun x -> f (xx)) (fun x -> f (xx));;
但是，F＃抱怨说，它无法弄清楚types：
let y = fun f -> (fun x -> f (xx)) (fun x -> f (xx));; --------------------------------^ C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a 'a but given a 'a -> 'b The resulting type would be infinite when unifying ''a' and ''a -> 'b'
如何在F＃中编写y-combinator而不使用let rec ... ？
正如编译器所指出的那样，没有可以赋值给xtypes，所以expression式(xx)是很好的types（这不是严格意义上的;你可以显式地将x为obj->_ – 参见我的最后一段）。 你可以通过声明一个recursiontypes来解决这个问题，这样一个非常相似的expression式就可以工作：
type 'a Rec = Rec of ('a Rec -> 'a)
现在Y-combinator可以写成：
let yf = let f' (Rec x as rx) = f (x rx) f' (Rec f')
不幸的是，你会发现这不是很有用，因为F＃是一个严格的语言，所以你试图用这个组合器定义的任何函数都会导致堆栈溢出。 相反，您需要使用Y-combinator的适用版本（ \f.(\xf(\y.(xx)y))(\xf(\y.(xx)y)) ）：
let yf = let f' (Rec x as rx) = f (fun y -> x rx y) f' (Rec f')
另一个select是使用明确的懒惰来定义正序Y-组合器：
type 'a Rec = Rec of ('a Rec -> 'a Lazy) let yf = let f' (Rec x as rx) = lazy f (x rx) (f' (Rec f')).Value
这有一个缺点，recursion函数定义现在需要一个显式的延迟值的强制（使用Value属性）：
let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))
但是，它的优点是可以像使用惰性语言一样定义非函数recursion值：
let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))
作为最后的select，您可以尝试使用装箱和向下转换来更好地逼近无types的lambda演算。 这会给你（再次使用Y-combinator的应用程序版本）：
let yf = let f' (x:obj -> _) = f (fun y -> xxy) f' (fun x -> f' (x :?> _))
这有一个明显的缺点，它会导致不必要的装箱和拆箱，但至less这是完全内部的实现，并不会真正导致在运行时失败。
我会说这是不可能的，并问为什么，我会交手和调用简单types的lambda微积分具有归一化属性的事实。 简而言之，简单types的lambda微积分的所有项都终止（因此Y不能在简单types的lambda微积分中定义）。
F＃的types系统并不完全是简单types的lambda演算的types系统，但它足够接近。 没有let rec F＃真的接近简单types的lambda微积分 – 重申一下，用这种语言，你不能定义一个不终止的术语，也不能定义Y.
换句话说，在F＃中，“let rec”至less应该是一个语言原语，因为即使你能够从其他原语中定义它，也不能input这个定义。 把它作为一个原始的元素可以让你在这个原始元素中给予一种特殊的types。
编辑：kvb在他的答案中显示，types定义（从简单的typeslambda微积分缺席的function之一，但是在let-rec-less F＃中）允许获得某种recursion。 非常聪明。
案例，让ML衍生物的声明是什么使它图灵完成，我相信他们是基于系统F，而不是简单的input，但重点是相同的。
系统F找不到任何定点组合器的types，如果可能的话，它不是强烈的标准化。
强正规化意味着任何expression式都只有一个正规forms，其中正规forms是不能再减less的expression式，这与每个expression式具有最大一个正常forms的无types化不同，它也可以不具有正常forms所有。
如果types化的lambda结石能以某种方式构造一个定点算子，那么expression式就很可能没有任何正规的forms。
另一个着名的定理，即停顿问题，意味着强烈正常化的语言不是图灵完全的，它说，不可能决定 （不同于certificate）一个图灵完全语言，其程序的哪个子集将停止什么input。 如果一种语言强烈正常化，那么它是可判定的，即它停止。 我们的algorithm来决定这是程序： true; 。
为了解决这个问题，ML-derivative扩展了System-F，并且让（rec）来克服这个问题。 因此函数可以再次引用它们自己的定义，使它们实际上不再是lambda结构，所以不可能仅仅依靠匿名函数来实现所有可计算函数。 他们因此可以再次进入无限循环，重新获得完整性。
简短的回答：你不能。
长答案：简单types的lambda演算强烈规范化。 这意味着它不等于图灵。 这样做的原因基本上归结为Y组合器必须是原始的或recursion定义的（如你所发现的）。 它不能在系统F（或更简单的types的结石）中expression。 这是没有办法的（事实certificate，毕竟）。 不过，您可以实现的Y组合器完全按照您所需的方式工作。
如果你想要一个真正的教会式的Y combinator，我会build议你尝试一下scheme。 使用上面给出的应用版本，因为其他版本将不起作用，除非您明确地添加懒惰，或使用懒惰的Scheme解释器。 （从技术上来说，Scheme不是完全无types的，但是它是dynamictypes的，这对于这个来说已经足够了。）
看到这个强标准化的certificate： http : //citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794
再想一想，我很确定添加一个原始的Y组合器，其行为与letrec定义的完全一样，使得系统F Turing完成。 所有你需要做的模拟一个图灵机，然后是实现磁带作为一个整数（二进制解释）和转变（定位头）。
