Think Stitch
  最近の更新


MUパズル

ゲーデル、エッシャー、バッハ―(ダグラス・R. ホフスタッター著)という本に「MUパズル」というものが出てきます.このパズルを定理証明支援系 Isabelle で扱ってみます.

MUパズルとはこんなパズルです.M, I, U 3つの文字からなる文字列を考えます.はじめに MI という文字列を1つだけ持っています.それから規則があって,これを使って持ちものである文字列を増やしてくことができます.規則は4つあります.

  1. 最後の文字が I である文字列を持っているなら,そのあとに U を付け加えてよい.
    • 例: MI → MIU
  2. 文字列 M$x$ を持っているときは,文字列 M$xx$ を持ちものに加えてよい.
    • $x$ というのは M, I, U からなる任意の文字列を表します.$xx$ というのはそれを2回繰り返して並べるという意味です.たとえば MIU を持っているとすると M$x = $ MIU から $x = $IU なので,これを2回繰り返して M をつけた MIUIU を得られます.
      • MIU → MIUIU
      • MUM → MUMUM
  3. もし所有しているある文字列の中にIIIが現れるなら,そのIIIをUで置き換えてよい.
      • MIIII → MIU
      • MIIII → MUI
  4. もし所有する文字列のあるものがUUを含むなら,そのUUを省略してよい.
      • UUU → U
      • MUUUIII → MUIII

これらの規則をうまくつかって,MI からはじめて MU を作ることができるか?というのが問題です.

不可能の証明と不変条件

しばらくやってみると,これはできないんじゃないかという疑いが強くなってきますね.事実,これは「できない」というのが答えです.でも本当の問題はそこからです.できないということを証明することはできるでしょうか.

これはいわゆる「不可能の証明」というもので,難しい傾向があるようです.不可能の証明を行うひとつの方法は「不変条件」に着目することです.不変条件とは何かというと,ある操作の前後で変わらない条件のことです.いま考えているMUパズルでいうと,「規則を適用して新しい文字列を作る」という操作がありますね.ある性質を持つ文字列があるとして,それに規則を適用して新しい文字列を作ったとき,できた文字列も同じ性質を持っていれば,その性質を持っているという条件が不変条件になります.

なぜ不変条件が不可能の証明で役に立つかというと,目指しているゴール,いまの場合 MU という文字列,が不変条件を満たしていなければ,それは規則では作れないといえるからです.

MUパズルの不変条件

ではMUパズルで着目すべき不変条件は何でしょうか.偶然なのですが Wikipedia の不変条件に関する項目は例としてMUパズルを使っています.詳細な解説はそちらをみてもらうとして,端的に答えだけをいうと

文字列に含まれる I の個数は3の倍数ではない.

というのが不変条件です.

はじめに持っている文字列 MI は I が1個ですから3の倍数ではありません.すると各規則で生成される文字列はこの条件を満たします.性質を「保存する」ともいいます.つまり不変条件です.しかし文字列 MU には I が入っていませんから条件を満たしません.したがって MU を生成することはできないわけです.

集合の帰納的定義

以上の証明を形式化してみます.MUパズルを数学的にみると,文字列のある集合を帰納的に定義しているものとみることができます.帰納的な集合の定義というのは数学やコンピュータサイエンスでよく出てきます.たとえば偶数の集合 $E$ を定義するにはこんなふうにします.

  1. 0 は偶数である: $0 \in E$
  2. $n$ が偶数ならば $n+2$ も偶数である: $n \in E \Rightarrow n+2 \in E$

さらに,以上の2つの規則だけを使って $E$ に入るものだけが偶数で,それ以外のものは含まれていないとする,という条件が付きます.いい換えれば,上の2つの規則で定まる $E$ の中で,もっとも小さいものを選ぶという意味です.小さいというのは集合の包含関係での意味です.もし上の条件を満たす別の集合 $X$ があったとしたら $E \subseteq X$ だということです.

MUパズルの規則で生成できる文字列の集合を $S$ とすると,偶数の集合と同じように帰納的に定義できます.

  1. 最後の文字が I である文字列を持っているなら,そのあとに U を付け加えてよい.
    • $x\mathsf{I} \in S \Rightarrow x\mathsf{IU} \in S$
  2. 文字列 M$x$ を持っているときは,文字列 M$xx$ を持ちものに加えてよい.
    • $\mathsf{M}x \in S \Rightarrow \mathsf{M}xx \in S$
  3. もし所有しているある文字列の中にIIIが現れるなら,そのIIIをUで置き換えてよい.
    • $x\mathsf{III}y \in S \Rightarrow x\mathsf{U}y \in S$
  4. もし所有する文字列のあるものがUUを含むなら,そのUUを省略してよい.
    • $x\mathsf{UU}y \in S \Rightarrow xy \in S$

そして偶数のときと同じく,これらの規則で生成できないものは入っていないとします.

定理証明支援系 Isabelle による形式化

集合 $S$ の定義を定理証明支援系 Isabelle にのせていくことにします.

まずおまじないです.

theory MU_Puzzle imports Main begin

次に文字 M, I, U からなる型 miu を定義しておきます.

datatype miu = M | I | U

集合の帰納的定義は inductive_set というコマンドでできます.コマンド名につづいて定義する集合の名前,その型,そして where のあとに縦棒で区切って規則を書きます.

inductive_set S :: "miu list set" where
  "[M, I] : S" |
  "x @ [I] : S ==> x @ [I, U] : S" |
  "[M] @ x : S ==> [M] @ x @ x : S" |
  "x @ [I, I, I] @ y : S ==> x @ [U] @ y : S" |
  "x @ [U, U] @ y : S ==> x @ y : S"

[...] はリスト,@ はリストの連結を表します.細かいところは省略しますが,雰囲気はわかると思います.

最終的に証明したい定理は次のものです.

theorem "[M, U] ~: S"

これを証明するために,不変条件についての補題を証明します.文字列 $x$ の中に含まれる I の数を関数 ci $x$ で表すことにすると補題は次のようになります.mod は剰余,~= は「等しくない」です.集合 $S$ に含まれるすべての文字列について,I の数は3の倍数ではない,ということです.

lemma miu_inv: "x : S ==> (ci x) mod 3 ~= 0"

関数 ci は次のように再帰的に定義できます.

fun ci :: "miu list => nat" where
  "ci [] = 0" |
  "ci (x#xs) = (if x = I then 1 + (ci xs) else ci xs)"

では証明をはじめます.ここでも細かいことは抜きにして,定理証明支援系でどんなふうに証明をするのか,という雰囲気をつかむことを目的にします.

この補題は「帰納的に定義された集合 $S$ の任意の要素 $x$ について~である」という形をしています.この形の定理を証明するときは定石として帰納法を使います.Isabelle では inductive_set を使って帰納的定義を書くと,それに合わせた帰納法の規則を自動的に作ってくれます.この規則の名前は S.induct です.規則の中身はこんなふうになっています.はじめは目がチカチカするかもしれませんが,よく見ると規則に対応した節があることがわかります.

[| ?x : S;
   ?P [M, I];
   !!x. [| x @ [I] : S; ?P (x @ [I]) |] ==> ?P (x @ [I, U]);
   !!x. [| [M] @ x : S; ?P ([M] @ x) |] ==> ?P ([M] @ x @ x);
   !!x y. [| x @ [I, I, I] @ y : S; ?P (x @ [I, I, I] @ y) |] ==> ?P (x @ [U] @ y);
   !!x y. [| x @ [U, U] @ y : S; ?P (x @ [U, U] @ y) |] ==> ?P (x @ y) |]
==> ?P ?x

おおざっぱにこれは何をいっているかというと,「~である」という性質を満たす集合がすべての規則を満たすなら,それは $S$ を含んでいるということです.なぜかというと $S$ は規則を満たす最小の集合だからです.数学的帰納法がいっていることって,そういうことなんですね.

さて,ではこの規則を適用して,さらにできるだけ自動で証明してくれとお願いします.

lemma miu_inv: "x : S ==> (ci x) mod 3 ~= 0"
apply(erule S.induct)
apply(auto)

するとこんなゴールが残ります.

proof (prove): depth 0

goal (4 subgoals):
 1. !!x. [| x @ [I] : S; 0 < ci (x @ [I]) mod 3 |] ==> 0 < ci (x @ [I, U]) mod 3
 2. !!x. [| M # x : S; 0 < ci x mod 3 |] ==> 0 < ci (x @ x) mod 3
 3. !!x y. [| x @ I # I # I # y : S; 0 < ci (x @ I # I # I # y) mod 3 |] ==> 0 < ci (x @ U # y) mod 3
 4. !!x y. [| x @ U # U # y : S; 0 < ci (x @ U # U # y) mod 3 |] ==> 0 < ci (x @ y) mod 3

よく見ると ci (x [I]) とか ci (x I # I # I # y) とかありますけど,これは ci x + 1 とか ci x + ci y + 3 とかに簡約できますね.そこで証明を一時中断して,こんな補題を作ります.いわゆる分配則ですね.

lemma [rule_format,simp]: "ALL y. ci (x @ y) = ci x + ci y"
apply(induct_tac x)
apply(auto)
done

改めて不変条件の証明に戻ると,今度はゴールが1個だけ残ります.

proof (prove): depth 0

goal (1 subgoal):
 1. !!x. [| M # x : S; 0 < ci x mod 3 |] ==> 0 < (ci x + ci x) mod 3

これは算術的に証明できるので arith というコマンドで片付けられます.これで補題ができました.

lemma miu_inv: "x : S ==> (ci x) mod 3 ~= 0"
apply(erule S.induct)
apply(auto)
apply(arith)
done

補題を使って MU が作れないことを証明します.まず背理法を適用したあとで補題を使うとかんたんに証明できます.

theorem "[M, U] ~: S"
apply(rule classical)
apply(simp)
apply(drule miu_inv)
apply(simp)
done

こんなふうにして不可能の証明ができました.

ポイントをまとめておきます.

複雑でたくさんの規則をもつ帰納的定義などでは,証明の管理がとてもたいへんになりますけど,定理証明支援系を使うともれなく間違いなく証明が書けます.証明を手伝ってくれるというのは,推論を手伝ってくれるというだけでなく,証明の進捗を管理してくれるという部分も大きいのでした.

最後にスクリプト全体を示しておきます.

theory MU_Puzzle imports Main begin

datatype miu = M | I | U

inductive_set S :: "miu list set" where
  "[M, I] : S" |
  "x @ [I] : S ==> x @ [I, U] : S" |
  "[M] @ x : S ==> [M] @ x @ x : S" |
  "x @ [I, I, I] @ y : S ==> x @ [U] @ y : S" |
  "x @ [U, U] @ y : S ==> x @ y : S"

fun ci :: "miu list => nat" where
  "ci [] = 0" |
  "ci (x#xs) = (if x = I then 1 + (ci xs) else ci xs)"

lemma [rule_format,simp]: "ALL y. ci (x @ y) = ci x + ci y"
apply(induct_tac x)
apply(auto)
done

lemma miu_inv: "x : S ==> (ci x) mod 3 ~= 0"
apply(erule S.induct)
apply(auto)
apply(arith)
done

theorem "[M, U] ~: S"
apply(rule classical)
apply(simp)
apply(drule miu_inv)
apply(simp)
done

end

2016/07/23

© 2013-2016 PRINCIPIA Limited