在 Ocaml 中编写 Z 组合器

Posted 2023-02-19

【中文标题】在 Ocaml 中编写 Z 组合器

【英文标题】：Writing the Z combinator in Ocaml

【发布时间】：2022-01-13 05:44:18

【问题描述】：

我是 lambda 演算的新手，我发现语法有时对我来说模棱两可。 具体来说，我想知道如何理解 Z 组合器：

Z = λ f. (λ x. f (λ v. xxv)) (λ x. f (λ v. xxv))

如何在 OCaml 中编写它？ 更新： 像这样写时出现错误：

 fun f-> let g = fun x -> f(fun v-> x x v)in g g;;

错误：此表达式的类型为 'a -> 'b -> 'c 但是需要一个类型为 'a 的表达式 类型变量 'a 出现在 'a -> 'b -> 'c

【问题讨论】：

您觉得有什么歧义？语法直接转换为 OCaml（但在这种情况下它不会进行类型检查，除非您将选项 -rectypes 传递给 OCaml）。您唯一需要了解的是构造 λ x, … 的含义。你肯定知道如何用 OCaml 语法表达同样的概念。

我想知道在哪里加括号，例如：does λ x. f (λ v. xxv) 均值 (λ x. f) (λ v. xxv) 或 λ x。 (f (λ v. xxv))？ λ v. xxv 是指 λ v. (xxv) 还是 (λ v. x)xv ?

您不需要对括号进行任何更改。

当我写 fun f -> let g = fun x -> f fun v -> x x v in g g;;在 ocaml 中存在语法错误。

确实，与 lambda 演算表达式相比，您已经删除了括号：写 f (fun v -> ...) 而不是 f fun v -> ...。所以你的问题真的是 OCaml 的语法，而不是 lambda 演算的语法。

【参考方案1】：

键入 Z-combinator 需要允许递归类型（使用 -rectypes 选项）或将类型递归装箱在类型构造函数中：

type 'a fix = Fix of ('a fix -> 'a)
let z f = 
  (fun (Fix x as fx) -> f (fun v -> x fx v)) 
  (Fix (fun (Fix x as fx) -> f (fun v -> x fx v)))

本质上，我们正在替换

x x v

要求x 接受自身有一个参数导致递归类型'a -> 'b -> 'c as 'a by

x fx v

将递归类型装箱为('a -> 'b) fix -> 'a -> 'b