如何在没有“let rec”的情况下定义 y-combinator？

StackOverflow https://stackoverflow.com/questions/1998407

  •  22-09-2019
  •  | 
  •  

题

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

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

这按预期工作，但使用定义 y 组合器感觉像是作弊 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 ...?

有帮助吗？

解决方案

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

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

现在 Y 组合器可以写成：

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

不幸的是，您会发现这不是很有用，因为f＃是一种严格的语言，因此您尝试使用此组合器定义的任何功能都会导致堆栈溢出。相反，您需要使用 Y 组合器的应用顺序版本（\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 :?> _))

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

其他提示

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

F# 的类型系统并不完全是简单类型 lambda 演算的类型系统，但也足够接近。F# 不带 let rec 非常接近简单类型的 lambda 演算——并且重申一下，在该语言中，您不能定义一个不终止的术语，并且也排除定义 Y。

换句话说，在 F# 中，“let rec”至少需要是一个语言原语，因为即使您能够从其他原语定义它，您也无法键入该定义。将其作为原语可以让您除其他外，为该原语提供特殊类型。

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

ML 导数中的 Case 和 let 语句使其成为图灵完备，我相信它们基于 System F，而不是简单地键入，但要点是相同的。

系统 F 无法找到任何定点组合器的类型，如果可以的话，它不是强归一化。

强标准化意味着任何表达式都具有精确的 一 范式，其中范式是一个不能进一步简化的表达式，这与无类型的不同，无类型的每个表达式都有 最大时 一种范式，它也可以根本没有范式。

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

另一个著名的定理，停止问题，暗示强规范化语言不是图灵完备的，它说这是不可能的 决定 （与证明不同）图灵完备语言的程序的哪个子集将在什么输入上停止。如果一种语言是强规范化的，那么它是否停止是可判定的，即它 总是 停止。我们决定这个的算法是程序： true;.

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

简短回答：你不能。

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

如果你想要一个真正的教会风格的 Y 组合器，我建议你尝试一下方案。使用上面给出的应用版本，因为其他版本将不起作用，除非您显式添加惰性，或使用惰性方案解释器。（从技术上讲，方案并不是完全无类型的，但它是动态类型的，这对此已经足够好了。）

请参阅以下内容以获取强标准化的证明：http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.127.1794

经过更多思考后，我非常确定添加一个原始 Y 组合器（其行为方式与 letrec 定义的组合器的行为方式完全相同）可以使系统 F 图灵完整。模拟图灵机所需要做的就是将磁带实现为整数（以二进制解释）和移位（以定位磁头）。

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top