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

如何解决是否可以在 Ocaml 中实现罗素悖论？

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

解决方法

我既不是逻辑学家，也不是类型论或集合论者。但是，如果您打开 -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

Russell 集合不包含 just_self，因为该集合包含自身：

# russell just_self;;
- : bool = false

现在是大回报。罗素集是否包含自身？

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

这是您应该期待的。即，计算发散。 （也是这个网站非常合适的结果。）