我最近在朴素集合论中了解了罗素悖论，当考虑所有不是自身成员的集合的集合时，如果它不是自身的成员，则该集合似乎是自身的成员，这就产生了悖论。 我想知道一个询问一个集合是否是其自身成员的函数是否可以用 Ocaml 等功能语言实现，因为罗素悖论本身没有明确的答案，如果是这样，想知道如何解决这个问题的任何提示问题。此外，我有兴趣了解这些数学悖论中的任何一个是否可以普遍实现。
【问题讨论】：
标签： functional-programming ocaml set-theory
我既不是逻辑学家，也不是类型论或集合论者。但是如果你打开-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。然后你可以在相当合理的程度上创造罗素悖论。
空集是一个总是返回假的集合：
$ 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?).
这是您应该期待的。即，计算发散。 （对于这个网站也是一个非常合适的结果。）
【讨论】：