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

Question

从示例和对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计算为真;检查这里的真相表 ).

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

最后,您可以期望在每个函数语言或函数库中看到完全相同的行为,包括同义词all,forall也可能是其他函数.如果你探索这些函数的实现,你会发现一个共同的模式:函数将返回true,除非它找到一个反例,即谓词为false的元素; 如果它没有找到这样的元素(包括根本没有找到任何元素 - 空集)那么它就不能证明谓词是假的,并返回true.这可以通过循环或折叠来完成,具体取决于语言或框架,但这个想法总是相同的.

例如,检查:

• 谷歌番石榴Iterables.all(更具体地说,Iterators.all) ; 要么
• 功能JavaList.forall ; 要么
• Scala的forall ; 要么
• Haskell的数据/列表all ; 要么
• ECMAScript 5的Array.every ; 要么
• Underscore.js的every ; 要么
• F#的Seq.forall ; 要么
• C#的Enumerable.All ; 要么
• C++的all_of ; 要么
• Python的all ; 要么
• Ruby的 all?

(它们都与(every? pred coll)Clojure 完全相同;可以随意编辑和添加您喜欢的语言或库!).

有关更多信息,请务必阅读Wikipedia关于Universal Quantification和Vacuous truth的文章.

Answer 2

我们有3种可能的情况,一次只有一种情况适用于集合.

• 集合中有项目,它们都是谓词 - True
• coll中的一个项目使谓词失败 - False
• 柯是空的 - ??

现在,如果你考虑为空列表返回false,它也会感觉很奇怪,因为当coll中的至少一个项目使谓词失败但是没有发生的空列表时返回false.

我认为选择真空的合理理由是基于这样一个事实,即在现实世界中这种情况适用的情况与没有意义的情况相比更多.例如:有人给了我一个URL列表,我需要返回他们下载的内容,现在我的函数首先要验证每个URL是否格式正确,然后使用map或pmap下载URL -

(if (every? url? urls) (map download urls) (throw "Invalid url found"))

这种以及更多此类示例将使序列的处理更加无缝.

另一方面,我是一个静态类型的语言家伙(如Haskell),并且更喜欢使用类型来解决这个问题.我不希望返回true或false,而是希望此函数返回Maybe bool:

• coll中的每个项目都传递谓词 - Just True
• coll中的一个项目使谓词失败 - Just False
• 柯是空的 - Nothing