在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)（10 x元素X意味着P（x ））。由於這個含義的左邊對於空集是假的（即，沒有元素x使得x∈Ø，其僅僅是空集的定義），所以暗示是真實的（即，false ⇒ whatever評估爲真;檢查truth tablehere）。

這正是您所看到的代碼中顯示的內容：Clojure正在根據謂詞邏輯將空列表'()上的通用謂詞(every? pred)評估爲true，根據謂詞邏輯，這是正確的和完美的邏輯。

最後，您可以期待在每個功能語言或功能庫上看到完全相同的行爲，其中包括同義詞all,forall或其他。如果您研究這些函數的實現，您會注意到一個常見模式：函數將返回true，除非它找到一個反例，即謂詞爲false的元素;如果它沒有找到這樣的元素（包括根本找不到任何元素 - 空集），那麼它不能證明謂詞是假的，並返回true。這可以通過循環或摺疊完成，具體取決於語言或框架，但這個想法總是相同的。

例如，檢查：

• 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維基百科的文章。

Answer 2

我們有3種可能的情況，每次只適用於一個集合。

• 館藏有項目，他們都PAS謂語 - 真
• 一位在科爾的項目失敗的斷言 - 假
• 的科爾是空的 - ??

現在，如果您考慮爲空列表返回false，它也會感到不可思議，因爲當coll中至少有一個項失敗謂詞但未發生空列表時返回false。

我認爲選擇真空作爲理性選擇是基於這樣一個事實，即在現實世界中適用的情況的數量多於無意義的情況。例如：有人給了我一個網址列表，我需要回到他們的下載內容，現在我的功能首先要驗證每個URL是正確的格式，然後用地圖或PMAP下載網址 -

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

這個和更多的這種例子將使序列更加無縫工作。

另一方面，我是一個靜態類型的語言傢伙（像Haskell），並傾向於使用類型來解決這個問題。而不是返回一個true或false我希望這個函數返回Maybe bool這樣的：

• 在科爾的每一項通過謂語 - Just True
• 一位在科爾的項目失敗的斷言 - Just False
• 的科爾是空的 - Nothing