ケネディと天使の問題を Isabelle で証明 その２ 気まぐれ天使問題

■

概要

ケネディと天使の問題、または、うそつき天使問題、気まぐれ天使問題、三人の天使問題…と言われているものを、定理証明システム Isabelle でその答えが正しいかチェック(証明)した。

これは「その２」で、気まぐれ天使問題を扱う。

■

スターリン登場

野崎昭弘『詭弁論理学』(中公新書)の p.14-16, 148-154 に、「ケネディの問題」があり、それを「その１」で説明したが、それには続きがある。

>	ケネディの問題を、次のように変更してみよう。まず登場人物をチャーチル、ヒトラー、スターリンの三人にふやす。そしてチャーチルはいつでも正しいことをいい、ヒトラーはいつでもウソをつくが、スターリンはウソをつくか本当のことをいうか、きまっていないとする。ケネディはこれらのうちの (誰ともわからない) 二人に、一回ずつ、「はい」か「いいえ」で答えられる質問をする。三回以上質問をしても、誰も答えてくれない。ケネディは正しい道をみつけられるのだろうか？

答えはケネディは正しい道を見つけることができて、その質問は、わからないなりに三人を A B C とラベル付けした上で、

>	天使 A (誰でもよい) をつかまえて、次のようにきく。 「あなたは、『この方(と天使 B を指さしながら) がスターリンですか』ときかれたら、『はい』と答えますか？」 (…) 前の答が「はい」なら C に、「いいえ」なら B にきく。 「あなたは『この (右の) 道が天国に行く道であうか』ときかれたら『はい』と答えますか？」

…と質問すればよい。これがネットで「気まぐれ天使」問題・三人の天使問題と言われているものの解答である。

■

記号論理的解答

問題は、スターリンをどう定式化するかである。つまり乱数を返してくるのがスターリンということになる。これを記号論理という「関数型プログラミング」の世界でどう表すか？

一つよくやる手が、環境の導入である、今回はそのテでいく。つまり、「何時何分何秒 経度緯度何分で言った」という子供のあおりがあるが、それを地で行き、環境(時間・場所)を指定すれば、スターリンと言えど言ったことは一つだったはずであるとするのである。

そして、基本、質問はみずに環境だけ見てると考える。スターリン関数 s は、環境 e について s(e) を返すが、その値はわからないとする。(質問 q について s(q, e) とすることもできるが、本質的な差はない。)

そして、s(e) がどんな値になるかわからないが成り立つ、というのは、すべての e について成り立つことと定式化する。

最初の質問 Q1 は Q1(f) = f(f = s) ということになる。p1 = f(Q1(f)) とすると、何らかの選択関数 ch について y = ch(p1) とし y(Q2(y)) = p となるようにしたいということ。

ch は p1 が真ならば C を 偽ならば B を返す関数で、Q2 は、「その１」の q に等しく Q1(f) = f(p) とすればいいというのが解答になる。

■	Isabelle でのチェック

ここまで難しくなるとチェックしがいがあるというものである。ソース KennedyProblem2.thy は次のようになる。

theory KennedyProblem2
  imports Main
begin

typedecl env 

consts Paradise :: "bool"

datatype angel = Churchill | Hitler | Stalin

definition churchill :: "bool => bool" where
"churchill x == x"

definition hitler :: "bool => bool" where
"hitler x == ~x"

consts stalin :: "env => bool"

fun apply_angel :: "angel => env => bool => bool" where
"apply_angel Churchill e x = churchill x" |
"apply_angel Hitler e x = hitler x" |
"apply_angel Stalin e x = stalin e"

definition kennedy_problem ::
  "((bool => bool) => angel => angel => angel => bool) => 
   (bool => nat) => 
   ((bool => bool) => angel => angel => angel => bool) => 
   bool"
  where
"kennedy_problem Q1 C Q2 == 
ALL a::angel. ALL b::angel. ALL c::angel.
  a ~= b & b ~= c & c ~= a
-->
(ALL p1::bool. ALL y::angel.
  ALL e1::env. ALL e2::env. ALL e3::env. ALL e4::env.
  apply_angel a e1 (Q1 (apply_angel a e2) a b c) = p1
  & y = nth [a, b, c] (C p1)
  -->
  apply_angel y e3 (Q2 (apply_angel y e4) a b c) = Paradise)"

lemma kennedy_answer:
  shows "kennedy_problem (%f a b c. f (b = Stalin))
           (%p. if p then 2 else 1) (% f a b c. f Paradise)"
  apply (unfold kennedy_problem_def)
  apply (intro allI)
  apply (case_tac [!] a)
  apply (case_tac [!] b)
  apply (case_tac [!] c)
  apply (simp_all add: churchill_def hitler_def)
  done

end

apply_angel は「その１」と違い、環境 e::env を取るものとなっている。そして A B C は a b c とローカルに表されることになる。その a b c が使えるように Q1 や Q2 は a b c も引数として取るように変更されている。

しかし、ch は C になっているが、この C は質問を介さないので、a b c のことは知らないというのを表現するために、C の結果を何番目かという数値として出し、その番号で a b c のうちの一つが選ばれるようになっている。

解答である Q1 f a b c は、f (b = Stalin) に、C p1 は、 if p1 then 2 else 1 に、Q2 f a b c は、f Paradise になっている。

証明はとても簡単で、a b c をそれぞれ Churchill Hitler Stalin に総当り的に割り当ててから simplify すればよい。

■

結論

Isabelle で「気まぐれ天使」問題の解答をチェックした。

a b c が誰かを「知らない」ということを a b c を「区別できない」まますべての a b c について成り立つと表現しているのがおもしろい。さらに、「知らない」というのは C が a b c を直接使わないことで表現されているのもおもしろい。

また stalin 関数の詳しい内容が定義されていなくても、それが使われないように消えるので問題ないというのもおもしろい。

「その３」では気まぐれ天使問題について、悪戦苦闘した経緯を話したい。ただ、そこは「失敗」が語られるだけなので、普通の人は、この「その２」までで十分かもしれない。

(配布物・参考文献・ライセンス・更新の情報は「その１」にあります。)

更新：	2020-06-22
初公開：	2020年06月22日 08:07:44
最新版：	2020年06月23日 00:14:58