是否可以在 Ocaml 中实现罗素悖论？

Question

我最近在朴素集合论中了解了罗素悖论，在考虑所有不属于其自身的集合的集合时，该集合似乎是其自身的成员，当且仅当它不是其自身的成员，这就产生了悖论。我想知道一个询问集合是否是其自身成员的函数是否可以用 Ocaml 这样的函数式语言来实现，因为罗素悖论本身没有明确的答案，如果是这样，希望有任何关于如何解决这个问题的提示问题。此外，我有兴趣了解这些数学悖论是否可以普遍实现。

Answer 1

我既不是逻辑学家，也不是类型论或集合论学家。但是如果你打开，-rectypes你可以编写一个函数来测试列表是否是其自身的成员：

$ ocaml -rectypes
        OCaml version 4.10.0

let f x = List.mem x x;;
val f : ('a list as 'a) -> bool = <fun>

您可以创建一个列表，该列表是其自身的成员：

# let rec mylist = [mylist];;
val mylist : 'a list as 'a = [<cycle>]
# f mylist;;
- : bool = true

不幸的是，我怀疑这与罗素悖论只有微弱的关系。

更新

假设您将一个集合定义为一个函数，该函数对于集合中的元素返回 true，对于不在集合中的元素返回 false。然后你就可以在相当合理的程度上创造罗素悖论。

空集是一个总是返回 false 的集：

$ rlwrap ocaml -rectypes
        OCaml version 4.10.0

# let empty x = false;;
val empty : 'a -> bool = <fun>

这是一个包含自身的单例集：

# let rec just_self x = x == just_self;;
val just_self : 'a -> bool as 'a = <fun>

您可以尝试对这些值进行各种测试并获得合理的答案：

# empty empty;;
- : bool = false

空集不包含任何东西，包括它本身。

# just_self empty;;
- : bool = false

该集合just_self仅包含其自身，而不包含空集合。

# just_self just_self;;
- : bool = true

那么罗素集就是包含不包含自身的集合的集合：

# let russell s = not (s s);;
val russell : ('a -> bool as 'a) -> bool = <fun>

罗素集包含空集（因为它不包含自身）：

# russell empty;;
- : bool = true

罗素集不包含just_self，因为该集包含其自身：

# russell just_self;;
- : bool = false

现在是巨大的回报。罗素集包含自身吗？

# russell russell;;
Stack overflow during evaluation (looping recursion?).

这是你应该期待的。即，计算发散。（对于这个网站来说也是一个非常合适的结果。）