Lambdaカクテル

京都在住Webエンジニアの日記です

Invite link for Scalaわいわいランド

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

こういうツイートが話題になっていた。

つまりScalaで言うと次のようなコードが何になるか、というものである。

val xs = Seq.empty[Int]
xs.forall(_ == 42)

結論から言うと、このような関数は常にtrueを返す。 なぜだろう?その理由をこれから説明する。

ちなみに他に以下のような意見があった:

  • 仕様による
  • 例外を投げるべき

いずれもまぁありえなくはないが、やめておいたほうが良いと思う。もし仮にfalseを返すような仕様があった場合、それは数学から乖離しているのでいずれ仕様内部で矛盾する可能性が高いし*1、最終的に数学的に正しい方向に修正されることが多い(経験的に)。例外を投げるべき理由も見当らない。絶対にどうしても空集合にならないと保証できるのであれば良いが、NonEmptyListのような型のサポートを受けられるのでない限り、そういう保証ができることのほうが少ないだろう。引数として空集合を受け付ける以上は、絶対に値を返さなければならないはずだと思う。

Vacuous Truth

この概念は、Vacuous Truth という数学の概念で説明される(定訳はなさそう)。

en.wikipedia.org

空集合に対してforall演算をすると、常にtrueになるというものだ。とはいえこれだけだと味気ないので、もう少し直感的に分かりやすい説明に挑んでみよう。

空和

空和という概念がある。

ja.wikipedia.org

これは、空集合の要素の和を取るといくつになるか?という概念である。これなら多くの人が直感的に0と考えるのではないだろうか。というのも、加算の単位元は0だから、何もしないという操作に対応させると空和は0になるのが自然だからである。何も買わなかった日の支出は0円に決まっている。

ちなみに、Scalaでもそのように振る舞う。

scala> Seq[Int]().sum
val res0: Int = 0

同様の概念として空積という概念もある:

ja.wikipedia.org

空集合の要素の積を取ると1である。こうなる理由も空和同様、乗算の単位元は1だから、そのように定義したほうが自然だからである。

一般に、集合に対する操作は、空集合に対して何らかの自然な拡張が与えられていることが多い。

畳み込み演算として見た場合のforall、exists

さて、発端のツイートで話題となっているのは「全ての要素がpを満たすときtrue」というような演算である。ちなみにこれはforallとかeveryという名前で呼ばれる一般的な演算である。仮にforallを自前で演算するなら、以下のように実装するのではないだろうか?(コードは疑似コード)

// pseudocode
forall p xs = p(x1) && p(x2) && p(x3) && p(x4) && ... && p(xn)

また、「要素が1つでもpを満たすときtrue」を返すような演算であるexists(someという名前で呼ばれる言語もある)は以下のように実装することだろう:

// pseudocode
exists p xs = p(x1) || p(x2) || p(x3) || p(x4) || ... || p(xn)

&&|| の単位元を導入する

さて、問題となっているのはxsが空集合の場合である。先程の定義ではこのような場合は要素が無いので定義できなくなってしまう。

ここで便利なのが単位元である。&&||にも単位元があるのだ*2。先程の定義を変形して、それぞれの演算に単位元の要素を導入してみよう:

// pseudocode
forall p xs = p(x1) && p(x2) && p(x3) && p(x4) && ... && p(xn) && eAnd
exists p xs = p(x1) || p(x2) || p(x3) || p(x4) || ... || p(xn) || eOr

それぞれ、&&の単位元をeAnd||の単位元をeOrとしている(単位元は通例eと表現される)。単位元はその定義上「二項演算しても結果を変えない」ので、eAndeOrはそれぞれ以下の通りになる:

  • eAnd: true (p && eAnd == pにより定まる)
  • eOr: false (p || eOr == pにより定まる)

したがって、さきほどの定義中の単位元を具体的な値に置換すると以下の通りになる(単位元の性質上、挙動は変わらない):

// pseudocode
forall p xs = p(x1) && p(x2) && p(x3) && p(x4) && ... && p(xn) && true
exists p xs = p(x1) || p(x2) || p(x3) || p(x4) || ... || p(xn) || false

空集合の場合

もうお分かりかと思うが、先程の定義によれば、空集合の場合の定義は要素部分が消えて以下の通りになる:

// pseudocode
forall p [] = true
exists p [] = false

とくにforallの場合はやや直感に反するかもしれないが、数学的にはこちらのほうが矛盾が無い良い定義である。対偶を取ると直感的になるかもしれないので試してみてほしい。

したがって、以下のことが言える:

  • 「配列のすべての要素が条件を満たすならtrueを返す」関数を空集合に対して適用すると、常にtrueになる
  • 「配列の要素が1つでも条件を満たすならtrueを返す」関数を空集合に対して適用すると、常にfalseになる
  • このように実装しなければ数学的矛盾を抱えることになる

ちなみに同様のメソッドが定義されている言語では、ほぼ全ての言語でこの仕様になっている。例えばScalaでもそうなっている:

val xs = Seq.empty[Int]
xs.forall(_ == 42) // => true
xs.exists(_ == 42) // => false

集合が空かどうかと、全ての要素についてpであるという判定とは、分けたほうがコードや仕様がシンプルになる。仕様が前述のものに反しそうなときは、この二者を分離できないか考えてみよう。

ウェイソン選択課題

ウェイソン選択課題という古典的な論理学のパズルがある。

ja.wikipedia.org

この課題に見られた面白い現象として、以下のようなものがある。

1992年に、進化心理学者のレダ・コスミデスとジョン・トゥービーは、社会関係という文脈で課題が提示された時に、被験者は「正しい」反応を返す傾向があることを突き止めた[9]。例えば、「アルコール飲料を飲んでいるならば18歳以上である」という仮説と「『資格が認められる年齢』と『飲み物』が書かれたカード」(例えば、16・25・ビール・コーラ)に対しては、ほとんどの参加者は容易に正しい解答である「16」と「ビール」を選択した。

どうやら、人間は社会的規範を判定するルールが関与するとこの手の問題を理解しやすくなるらしい。

そこで、問題を書き換えて以下のような形にしてみよう:

Q. ある映画館では、防犯や視聴体験の観点から、入場要件を満たした荷物しか持ち込むことができません。例えば銃や携帯電話は預けなければなりません。ある人が手ぶらで入場しようとしているとき、入場要件を満たしているといえますか?

この設問は冒頭の問題と論理的に全く等価だ。

モノイド

ところで、このforallexistsのような演算は、モノイドのリストに対する畳み込み演算という形で一般化される。そして、モノイドリストに対する畳み込みは、リストが空のとき、モノイドの単位元を返さなければならない。

モノイドとは、以下の各要素で構成される3兄弟のことを指す:

  • ある集合 $M$
  • その集合の上に定義された何らかの二項演算$\times$
    • ここでは $\times$ としているが、実際の記号は何でもよい
    • 演算の結果も $M$ のどれかの要素になる($M$に閉じている)必要がある
  • 任意の $x \in M$ について $x \times e = x$となるような単位元 $e$

また、モノイドは以下の制約を満たさなければならない:

  • $(x \times y) \times z = x \times (y \times z) = x \times y \times z$
  • $x \times e = e \times x$

ja.wikipedia.org

この定義だとちょっと抽象的だ。具体例をいくつか挙げてみよう。例えば、以下のようなモノイドを考えることができる:

  • 整数とその加算
    • $(\mathbb{Z}, +, 0)$ は前述の制約を満たす
  • 文字列とその結合
    • 全ての文字列の集合 $\mathbb{S}$に対して、二項演算として文字列結合を、単位元として""を採用すれば前述の制約を満たす
  • 真偽値とその論理積
    • $( \{ true, false \}, \wedge, true)$ は前述の制約を満たす
  • 真偽値とその論理和
    • $( \{ true, false \}, \vee, false)$ は前述の制約を満たす

このように、モノイドは普遍的な構造であり、どこにでも出現する。普遍的な構造であることの利点は、モノイド一般に対して適用できる操作を考えると、どのモノイドでもそれが可能になる点だ。つまり実装を大幅に省略できるということ。覚えておくと便利だぜ!

例えば、Scalaのリストを畳み込むメソッドであるfoldLeftはモノイドのリストを畳み込む演算に使うことができる((foldLeft自体はリストの内容がモノイドかどうかは気にしていないので、そこは区別する必要がある)):

val xs = Seq(true, false, true)
def forall[A](p: A => Boolean): Seq[A] => Boolean = (lis: Seq[A]) => lis.foldLeft(true)((x, y) => x && p(y))

forall((n: Int) => n % 2 == 0)(Seq(1,2,3)) // => false

これを応用すると、整数の加算による畳み込み(sum)や、文字列とその結合による畳み込み(mkString)も同じ形で実装できる:

def sum(ns: Seq[Int]): Int = ns.foldLeft(0)(_ + _)
sum(Seq(1,2,3,4,5)) // => 15
def mkString(ss: Seq[String]): String = ss.foldLeft("")(_ concat _)
mkString(Seq("foo", "bar", "buzz")) // => "foobarbuzz"

すごい!形が似ている演算が畳み込みという形式で一般化されてしまった。ループを手で書く必要がなくなった。「畳み込め」と命じたら終わりだ。

モノイドを意識して実装する利点は、各種演算の頑健さ(互いに矛盾しないこと)が数学的に保証されていることだ。前述の制約さえ守れば、どう合成してもちゃんと矛盾なく振る舞いますよ、というのが数学によって保証されている。 加えて、モノイドは畳み込みと特に相性が良い構造だ(なんせ単位元があり、結合の順位も無視していいから)。なので畳み込みになりそうな構造があったら、モノイドになるか確かめたほうがいい。

モノイドになりそうな集合と演算を見付けたら、このモノイド則を満たせるか確認してみて、それに従うように実装してみると将来にわたってその恩恵を受けられるだろう。仕様は変化するかもしれないが、数学は不変だ。

別解 (2023-06-10追記)

val lis: Seq[Int] = Seq()

これが成り立つのは自然ですよね(空のSeqSeq[Int]に代入できるべきですよね)、と考えるとより素直かもしれない。Seq[Int]は当然全ての要素がIntであることを要求するが、空であってもSeq[Int]の型を付けることが許されている。

あわせて読みたい

qiita.com

summertree.hatenablog.com

nowokay.hatenablog.com

*1:この結果をさらに論理演算するのであればその可能性はより高まる

*2:なぜなら、ブール代数はその2つの演算についてモノイドを成すからである

★記事をRTしてもらえると喜びます
Webアプリケーション開発関連の記事を投稿しています.読者になってみませんか?