clojure - 在 clojure 中，如果 coll 为空，(每个？pred coll)返回 true，这可能是设计缺陷吗？

Question

来自函数 every? 的示例和对 Clojuredoc 的评论

user> (every? true? '())    ;empty is true? 
true

user> (every? false? '())    ;empty is false? 
true

这确实很奇怪，而且可能不合逻辑，因为我预计上述两者都是错误的。有人可以解释一下这背后的基本原理吗？

Answer 1

在数学中，特别是在谓词逻辑领域，公认关于空集的每个全称谓词都是真的。例如，以下陈述是正确的:

Every integer in the empty set is even.

同样，以下陈述也是正确的:

Every integer in the empty set is odd.

因此，下面这个离奇的说法也是正确的:

Every integer in the empty set is simultaneously even and odd.

想一想:你能举出以上任何一个的反例吗？

更正式的解释如下。当你有一个全称谓词时，可以正式写成 ∀x∈XP(x) (对于 X 的所有 x 元素，P(x))，它等价于形式 x∈X ⇒ P(x) 的蕴涵(X 的 x 元素意味着 P(x))。由于这个蕴涵的左边对于空集是假的(即没有元素 x 使得 x∈Ø ，这只是空集的定义)，蕴涵是真的(即， false ⇒ whatever评估为真；检查 truth table here )。

这正是您在显示的代码中看到的:Clojure 正在评估通用谓词 (every? pred)在空列表中 '()为真，根据谓词逻辑，这是正确且完全合乎逻辑的。

最后，您可以期望在每种​​函数式语言或函数式库上看到完全相同的行为，同义词是 all。 , forall也许还有其他人。如果你探索这些函数的实现，你会注意到一个常见的模式:函数将返回真，除非它找到一个反例，即谓词为假的元素；如果它没有找到这样的元素(包括根本没有找到任何元素——空集)，那么它不能证明谓词为假，并返回真。这是通过循环或折叠完成的，具体取决于语言或框架，但想法始终相同。

例如，检查:

Google Guava's Iterables.all (and, more specifically, Iterators.all ) ;或

Functional Java's List.forall ;或

Scala's forall ;或

Haskell's Data/List all ;或

ECMAScript 5's Array.every ;或

Underscore.js's every ;或

F#'s Seq.forall ;或

C#'s Enumerable.All ;或

C++'s all_of ;或

Python's all ;或

Ruby's all?

(它们的作用与 Clojure 中的 (every? pred coll) 完全相同；并且可以随意编辑和添加您喜欢的语言或库!)。

如需更多信息，请务必阅读维基百科关于 的文章。 Universal Quantification 和 Vacuous truth .