限量子を含むような数式が正しいかどうかを判定する話

そういえば一月以上前に授業で聞いて、面白かったので書こうと思ったんだった。なお、この話にウソが含まれていた場合は、私がいかにまじめに授業を聞いていないかを証明する材料になります。もう成績出てるから関係ない。(開き直った。)

Presburger formula

  • 定数: 0, 1, 2, ...
  • 関数: +
  • 述語: <,≦,=,≧,>

上の三つと変数からなる式をPresburger formulaという。日本語だとプレスバーガ式?

Presburger formulaの例は次みたいな感じ。

  • x + 4 \gt x
  • 3x + 5y \le 0

二つ目の例に含まれる3xは、3 \times xのことでいきなり定義に含まれない関数を使ってるように見えたりする。これは、よく見るとx+x+xと一緒だからOKという理屈。xy \le 9みたいのは、Presburger formulaじゃない。

さて、こいつに\existとか\forallとかの限量子(quantifier)をつけた式を考える。

  • \forall x . (x +1 \gt x)
  • \forall y . (\exist x .(2x \ge y \vee 10x + 6 \gt -3x) \wedge (10x \lt y))

こんな感じ。

驚くべきことは、この限量子付きのPresburger formulaが正しいか正しくないかが決定可能、つまり正しいか正しくないかを判定するアルゴリズムが存在すること。すげぇ。

ちなみに変数のドメインは整数か実数で考える。虚数だとどうなるかは知らん。

Quantifier elimination

嫌らしいのは\forallとか\existとかで、こいつらを消去できれば、かなり話は簡単になる。この限量子の消去について、変数のドメインが実数の場合には、次のことが言える。

  • (\exists x . c \le ax \wedge bx \le d) \Leftrightarrow bc \le ad
  • (\exists x . c \lt ax \wedge bx \le d) \Leftrightarrow bc \lt ad
  • (\exists x . c \le ax \wedge bx \lt d) \Leftrightarrow bc \lt ad
  • (\exists x . c \lt ax \wedge bx \lt d) \Leftrightarrow bc \lt ad

見ての通り、限量子\existsを含む式を\existsを含まない式に変換できてることがわかる。変数も消えてるので、定数a,b,c,dの値がわかっていることから、右側の式の真理値を求めるのは実に簡単。

あ、aとbはゼロ以上じゃないとダメです。

一応、証明というか簡単な説明をすると、

c \le ax \wedge bx \le d\frac{c}{a} \le x \wedge x \le \frac{d}{b}なので、\frac{c}{a} \le \frac{d}{b}になって、つまりcb \le adとなる。
最後の式には変数が含まれていないので、限量子は取っちゃってもOK

という感じだと思う。中学とかでやる二次方程式の解の公式みたいな感じ。

ちょっと面白くないですかね?

整数だともうちょっと難しくなる

変数のドメインが実数の場合は上の簡単な関係が導けてかなり幸せになれるんだけど、整数だと考えるともうちょっとややこしくなる。えーと、\exists x . 3x = 2みたいな式は、変数のドメインが実数だとx = 1.5でOKだけど、整数だとダメになる。

相当複雑になるので、ここでは説明しない。ボロが出そうだし。

Normalization

上で説明したQuantifier eliminationは良いんだけど、でも\forallとか\veeとか使った式も考えたいのが人情ってもんだと思う。当然、普通の限量子付きPresburger formulaを、上の書き換えが可能な形に変形することが可能で、これを正規化(Normalization)とか言うような気がする。

これは通常の一階述語論理(First-order predicate logic)の話なので、細かくは説明しない*1けど、次のようにして変形していける。

>、≧、=について
\phi = \psi(\phi \le \psi) \wedge (\psi \le \phi)と等しい。
\forallについて
\forall x . P(x)\neg \exists x . \neg P(x)と等しい。(ドモルガンの法則)
\wedgeとか[tex
\vee]とか:P \wedge Q\neg (\neg P \vee \neg Q)と等しい。(ドモルガンの法則)
\Rightarrow
P \Rightarrow Q\neg P \vee Qと等しい
\existsを内側へ移動
\exists x . (P \vee Q)(\exists x . P) \vee (\exists x . Q)と等しい。さらに\exists x . (P(x) \wedge R)(\exists x . P(x)) \wedge Rと、Rが変数xを含まない場合に、等しい。

こんな感じで、上のQuantifier eliminationが適用できる形の式に変形してから考える。

あ、他には普通の数学の知識は使っても良い。例えば\forall x . x+1 > xはそれぞれxを引いて\forall x . 1 > 0になる。(上の方で出した例がいきなり解けてしまったorz)

実際にやってみる

\forall y . (\exist x .(2x \ge y \vee 10x + 6 \gt -3x) \wedge (10x \lt y))を考える。

内側の式は、(P \vee Q) \wedge Rという形をしているが、これは(P \wedge R) \vee (Q \wedge R)と等しいので、次のようになる。

\forall y . (\exist x . (2x \ge y \wedge 10x \lt y) \vee (10x + 6 \gt -3x) \wedge (10x \lt y))

これを整理して次になる。

\forall y . (\exists x . (y \le 2x \wedge 10x \lt y) \vee (-6 \lt 13x \wedge 10x \lt y ))

[tex:\forall y . *2 \vee (\exists x . (-6 \lt 13x \wedge 10x \lt y)))]

\exists x . (y \le 2x \wedge 10x \lt y)10y \lt 2yと、\exists x . (-6 \lt 13x \wedge 10x \lt y)-60 \lt 13yと、それぞれ等しいので、次の式が得られる。

\forall y . (10y \lt 2y \vee -60 \lt 13y)

整理して、こうなる。

\forall y . (0 \lt -8y \vee  13y \lt -60)

ここでドモルガン。

\neg ( \exists y . (0 \ge -8y \wedge 13y \ge -60))

\neg (\exists y . (-60 \le 13y \wedge -8y \le 0)

\neg (480 \le 0)

 480 \le 0は、明らかに偽なので、全体としては真。


と思ったんだけど、これはウソだorz。
\neg (\exists y . (-60 \le 13y \wedge -8y \le 0)から\neg (480 \le 0)の変形が、yの係数が-8を含んでいるので、正しくない。えーと…これは…\neg (\exists y . (0 \le y \wedge -60 \le 13y))になるので、まあ結局は\negの内側が偽になって全体は真ですね。

※追記

ウソだウソ。

\neg (\exists y . (0 \le y \wedge -60 \le 13y))は偽。

0 \le y \wedge -60 \le 13yから0 \le y \wedge \frac{-60}{13} \le y。これはy = 0とかで真なので、\exists y . (0 \le y \wedge -60 \le 13y)が真。

なにに使えるの?

Quantifier eliminationの説明を簡単にするため、変数のドメインとして実数を考えたが、整数についてもこれは成り立つ。整数で、大小比較が意味を持つようななにかというと……配列の添え字とかですね。プログラムを解析して範囲外の配列をアクセスしないことを保障したい場合なんかに利用されるそうです。詳しくはよく知りません。

参考文献

参考文献的なものは http://axiom.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf なんかがあるそうです。恐ろしいことに、私はこれを読まずに話をしてます(!)。

*1:って、上の話も細かく説明してないけど

*2:\exists x . (y \le 2x \wedge 10x \lt y