47

在几乎所有示例中，ML 类型语言中的 y-combinator 都是这样编写的：

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

这可以按预期工作，但是使用let rec ....

我想在不使用递归的情况下定义这个组合器，使用标准定义：

Y = λf·(λx·f (x x)) (λx·f (x x))

直接翻译如下：

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

但是，F# 抱怨它无法确定类型：

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

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 组合器let rec ...？

4

5 回答 5

52

正如编译器指出的那样，没有可以分配给表达式的类型以x使表达式(x x)具有良好的类型（严格来说这不是真的；您可以显式键入xas obj->_- 请参阅我的最后一段）。您可以通过声明递归类型来解决此问题，以便使用非常相似的表达式：

type 'a Rec = Rec of ('a Rec -> 'a)

现在 Y-combinator 可以写成：

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

不幸的是，您会发现这不是很有用，因为 F# 是一种严格的语言，因此您尝试使用此组合器定义的任何函数都会导致堆栈溢出。相反，您需要使用 Y-combinator ( \f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))) 的应用顺序版本：

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

另一种选择是使用显式惰性来定义正常顺序 Y 组合器：

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

这样做的缺点是递归函数定义现在需要惰性值的显式强制（使用Value属性）：

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

但是，它的优点是您可以定义非函数递归值，就像在惰性语言中一样：

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

作为最后的选择，您可以尝试通过使用装箱和向下转换来更好地逼近无类型的 lambda 演算。这会给你（再次使用 Y 组合器的应用顺序版本）：

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

这有一个明显的缺点，它会导致不必要的装箱和拆箱，但至少这完全是实现内部的，并且永远不会真正导致运行时失败。

于 2010-01-04T14:54:10.640 回答
9

我会说这是不可能的，并问为什么，我会挥手并援引简单类型的 lambda 演算具有规范化属性的事实。简而言之，简单类型的 lambda 演算的所有项都终止（因此 Y 不能在简单类型的 lambda 演算中定义）。

F# 的类型系统并不完全是简单类型 lambda 演算的类型系统，但它已经足够接近了。F# withoutlet rec非常接近于简单类型的 lambda 演算——而且，重申一下，在那种语言中，你不能定义一个不终止的术语，也不能定义 Y。

换句话说，在 F# 中，“let rec”至少需要是一种语言原语，因为即使您能够从其他原语中定义它，您也无法键入此定义。将其作为原语允许您为该原语赋予特殊类型。

编辑：kvb 在他的回答中表明类型定义（简单类型的 lambda-calculus 中缺少的功能之一，但存在于 let-rec-less F# 中）允许获得某种递归。非常聪明。

于 2010-01-04T09:35:52.347 回答
4

ML 衍生品中的 Case 和 let 语句是图灵完备的原因，我相信它们是基于 System F 而不是简单的类型，但要点是相同的。

系统 F 找不到任何定点组合器的类型，如果可以，它不是强标准化。

强归一化意味着任何表达式都只有一个范式，其中范式是不能进一步简化的表达式，这与每个表达式最多只有一个范式的无类型不同，它也可以没有范式全部。

如果类型化的 lambda 演算可以以任何方式构造定点运算符，那么表达式很可能没有范式。

另一个著名的定理，停止问题，意味着强规范化语言不是图灵完备的，它表示不可能决定（不同于证明）图灵完备语言的程序的哪个子集将在什么输入上停止。如果一种语言正在强烈规范化，则可以确定它是否停止，即它总是停止。我们的算法来决定这是程序：true;.

为了解决这个问题，ML-derivatives 用 case 和 let (rec) 扩展 System-F 来克服这个问题。因此，函数可以在其定义中再次引用自己，使它们实际上不再有 lambda 演算，不再可能仅依赖匿名函数来处理所有可计算函数。因此，它们可以再次进入无限循环并重新获得它们的图灵完备性。

于 2010-05-18T20:31:13.767 回答
2

简短的回答：你不能。

长答案：简单类型的 lambda 演算是强归一化的。这意味着它不是图灵等效的。其原因基本上归结为 Y 组合子必须是原始的或递归定义的（如您所见）。它根本无法用 System F（或更简单的类型计算）来表达。没有办法解决这个问题（毕竟它已经被证明了）。不过，您可以实现的 Y 组合器完全按照您想要的方式工作。

如果你想要一个真正的 Church 式 Y 组合器，我建议你试试 scheme。使用上面给出的 applicative 版本，因为其他版本不起作用，除非你明确添加惰性，或者使用惰性 Scheme 解释器。（从技术上讲，方案不是完全无类型的，但它是动态类型的，这已经足够了。）

有关强标准化的证明，请参见： http ://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

在考虑了更多之后，我很确定添加一个与 letrec 定义的完全一样的原始 Y 组合子可以使 System F Turing 完整。模拟图灵机所需要做的就是将磁带实现为整数（以二进制解释）和移位（定位磁头）。

于 2011-04-09T07:32:41.873 回答
0

只需定义一个将自己的类型作为记录的函数，就像在 Swift 中一样（它是一个结构）:)

在这里，Y（大写）在语义上被定义为一个可以用自己的类型调用的函数。在 F# 术语中，它被定义为包含名为 call 的函数的记录，因此要调用定义为这种类型的 ay，您必须实际调用 y.call :)

type Y = { call: Y -> (int -> int) }

let fibonacci n =
    let makeF f: int -> int =
        fun x ->
            if x = 0 then 0 else if x = 1 then 1 else f(x - 1) + f(x - 2)
    let y = { call = fun y -> fun x -> (makeF (y.call y)) x }
    (y.call y) n

阅读起来并不是非常优雅，但它不会诉诸递归来定义应该自行提供递归的组合子^^

于 2021-02-11T21:55:48.713 回答