限量子を含むような数式が正しいかどうかを判定する話
そういえば一月以上前に授業で聞いて、面白かったので書こうと思ったんだった。なお、この話にウソが含まれていた場合は、私がいかにまじめに授業を聞いていないかを証明する材料になります。もう成績出てるから関係ない。(開き直った。)
Presburger formula
- 定数: 0, 1, 2, ...
- 関数: +
- 述語: <,≦,=,≧,>
上の三つと変数からなる式をPresburger formulaという。日本語だとプレスバーガ式?
Presburger formulaの例は次みたいな感じ。
二つ目の例に含まれるは、のことでいきなり定義に含まれない関数を使ってるように見えたりする。これは、よく見るとと一緒だからOKという理屈。みたいのは、Presburger formulaじゃない。
さて、こいつにとかとかの限量子(quantifier)をつけた式を考える。
こんな感じ。
驚くべきことは、この限量子付きのPresburger formulaが正しいか正しくないかが決定可能、つまり正しいか正しくないかを判定するアルゴリズムが存在すること。すげぇ。
Quantifier elimination
嫌らしいのはとかとかで、こいつらを消去できれば、かなり話は簡単になる。この限量子の消去について、変数のドメインが実数の場合には、次のことが言える。
見ての通り、限量子を含む式をを含まない式に変換できてることがわかる。変数も消えてるので、定数a,b,c,dの値がわかっていることから、右側の式の真理値を求めるのは実に簡単。
あ、aとbはゼロ以上じゃないとダメです。
一応、証明というか簡単な説明をすると、
はなので、になって、つまりとなる。
最後の式には変数が含まれていないので、限量子は取っちゃってもOK
という感じだと思う。中学とかでやる二次方程式の解の公式みたいな感じ。
ちょっと面白くないですかね?
Normalization
上で説明したQuantifier eliminationは良いんだけど、でもとかとか使った式も考えたいのが人情ってもんだと思う。当然、普通の限量子付きPresburger formulaを、上の書き換えが可能な形に変形することが可能で、これを正規化(Normalization)とか言うような気がする。
これは通常の一階述語論理(First-order predicate logic)の話なので、細かくは説明しない*1けど、次のようにして変形していける。
- >、≧、=について
- はと等しい。
- について
- はと等しい。(ドモルガンの法則)
- とか[tex
- \vee]とか:はと等しい。(ドモルガンの法則)
- はと等しい
- を内側へ移動
- はと等しい。さらにはと、Rが変数xを含まない場合に、等しい。
こんな感じで、上のQuantifier eliminationが適用できる形の式に変形してから考える。
あ、他には普通の数学の知識は使っても良い。例えばはそれぞれxを引いてになる。(上の方で出した例がいきなり解けてしまったorz)
実際にやってみる
を考える。
内側の式は、という形をしているが、これはと等しいので、次のようになる。
これを整理して次になる。
[tex:\forall y . *2 \vee (\exists x . (-6 \lt 13x \wedge 10x \lt y)))]
はと、はと、それぞれ等しいので、次の式が得られる。
整理して、こうなる。
ここでドモルガン。
は、明らかに偽なので、全体としては真。
と思ったんだけど、これはウソだorz。
からの変形が、yの係数が-8を含んでいるので、正しくない。えーと…これは…になるので、まあ結局はの内側が偽になって全体は真ですね。
※追記
ウソだウソ。
は偽。
から。これはy = 0とかで真なので、が真。
なにに使えるの?
Quantifier eliminationの説明を簡単にするため、変数のドメインとして実数を考えたが、整数についてもこれは成り立つ。整数で、大小比較が意味を持つようななにかというと……配列の添え字とかですね。プログラムを解析して範囲外の配列をアクセスしないことを保障したい場合なんかに利用されるそうです。詳しくはよく知りません。
参考文献
参考文献的なものは http://axiom.anu.edu.au/~michaeln/pubs/arithmetic-dps.pdf なんかがあるそうです。恐ろしいことに、私はこれを読まずに話をしてます(!)。