畳み込みの視点から見たforall(every)とexists(some): 空集合に対するforallは常にtrueになる - Lambdaカクテル

こういうツイートが話題になっていた。 「配列のすべての要素が条件を満たすならtrueを返す」関数を定義するとき、空の配列を渡したらfalseを返すかtrueを返すかが、良いプログラマかどうかの一つの境目だ— ふみ (DJ Monad) (@fumieval) 2023年5月29日 つまりScalaで言うと次のようなコードが何になるか、というものである。 val xs = Seq.empty[Int] xs.forall(_ == 42) 結論から言うと、このような関数は常にtrueを返す。 なぜだろう？その理由をこれから説明する。 ちなみに他に以下のような意見があった: 仕様による 例外を投げるべき いずれもまぁありえなくはないが、やめておいたほうが良いと思う。もし仮にfalseを返すような仕様があった場合、それは数学から乖離しているのでいずれ仕様内部で矛盾する可能性が高いし*1、最終的に

[Windymelt]

空集合に対するforallは自分も昔悩んだので書きました

[takumikabu]

all([a,b,c])が真なら、all([a]) && all([b,c])もall([a,b]) && all([c])も真になるべきだし、それならall([]) && all([a,b,c])も真であるべき。つまりall([])は真しかあり得ないと理解した。

[yojik]

「仕様による」っていうのは、その仕様を考えるときどうするか？っていう話なのでなんも意味ないよな、と思う。そしてその仕様を決めるとき、こういう足回りの部分が論理的に正しくないと全てがあやふやになる

[mollifier]

仕様によるというのは答えになってないよね。その仕様をどうするのが望ましいか、合理的なのかを決めようという話なのだから。でtrueにするのが妥当だと思う

[hase0510]

forall/existsよりもevery/someで書いた記事の方がPV増えそう／手続き的にforループで&=して行く処理を書く場合も結果変数の初期値はtrueにしておく必要があるし、配列が空なら初期値trueが結果になる

[deep_one]

記号論理学に従えば「常に真」と決まっている。集合Aは常に「集合Aと空集合の和」と書けるから、空集合がfalse返すとtrueを返せる集合はこの世に一つも存在しないことになる（笑）

[hom_functor]

「配列のすべての要素が条件を満たすならtrueを返す」が仕様ならtrueを返す以外の選択肢はない。空の場合にfalseを返す意図だったとしても、そういうビジネスロジックをこのレイヤーに混ぜ込むことはしない

[yuutetu]

ユーザが触るプロダクトの挙動に直結する部分は「仕様による」はそれはそうで、ライブラリの実装ならば集合論や論理学のallより「対象が空ならばtrue」の方がシンプルかつ共通認識が得られるのでそうすべきだとも思う

[aike]

and条件は単位元が1、orは0というのはわかりやすい。それはそうと、あるべき仕様を議論するときに必要以上に強い言葉を使わないのも良いプログラマーの条件だったり。

[slax]

空集合では要素をまともに判定できないんだからfalse返してくれ。

[masa8aurum]

・「空集合に対するforallはtrueを返す」としないと、数学的に矛盾する。単位元（加算なら0、乗算なら1、論理積なら真、論理和なら偽）を考えるとわかる

[daruyanagi]

“&&や||にも単位元がある”

[hylom]

数学的な話は別にして、仕様として「配列のすべての要素が条件を満たすならtrueを返す」が与えられた場合は別途空集合の場合の挙動を明確にするのが良い設計者（PythonもJSもそのケースはドキュメントに明記されている）

[asiamoth]

JavaScriptの`every`, `some`も同じ動作だった。「空配列か否か」の判定を別に用意して、必ずチェックするべきだな。

[aya_momo]

当たり前だけど説明するのは難しい。理屈はあるのだが、それで納得してもらえるかというと。

[zyzy]

あー、そうか。&&の単位元はtrueか。そらそうだな。

[codehex]

面白い！名前は知らなかったけど all 系はループ中に異常が見つかれば false を返して、ループが終われば true が返るから空配列だと必ず true の認識だった

[rgfx]

数学の話だけで済む部分のロジックならそれがよさそう

[koba789]

結論にパーマリンクが付いて便利（よい記事）

[hitode909]

わかりやすい

[takc923]

そうか、forallとexitsはそれぞれ (boolean, &&, true), (boolean, ||, false) のモノイドか。そういう目線で見たことなかった。面白い。

[nanakoso]

数学のルールも人が決めるといっても keepit simple が基本で、利点もないのに無意味に複雑になったり例外が増えるようなルールは作らない（作ってもほかの数学者に受け入れられない）

[uehaj]

「パーティのメンバ全員が死んでるとき全滅」パーティメンバがいないときは全滅扱い。「パーティのメンバ全員が生きているときザオラル不可」パーティメンバがいないときはザオラル不可

[ghostbass]

なるほど

[gfx]

めちゃくちゃ分かりやすくて感動した。

[cl-gaku]

直感的には？だけどそういう数学の決まりならそれでええわ

[tattyu]

最初の命題は例外を投げる、投げないならコメントやドキュメント、サジェストで判断出来る様にするが正解だろう。C++みたいに負のmodの挙動がある時から急に数学的に厳密になったりする方が困る。。

[teslur]

自然な拡張というのが大事な概念ですよね

[hitsujibane]

"Vacuous Truth"

[griefworker]

数学的に説明されて納得感ある。

[UhoNiceGuy]

数学のルール(どういう定義や公理を採用するか)って人間が決めるんでしょ。結局、仕様による、じゃないの