証明を型にはめると ● 証明チェッカ コンピュータ・サイエンスの究極の目標が、人間と同等もしくは人間よりも高度 な思考を計算機に行わせることだとすると、その第一歩は、人間の思考過程を忠 実に計算機に入力して、計算機の上で人間の思考過程をトレースすることだろう。 少し古くなるけれども、人工知能の分野において、ジョン・マッカーシーとパト リック・ヘイズは、その古典的論文(題名は忘れてしまった)で、思考過程を記述 することをepistemology(認識論)と呼び、その重要性を説いた。しかし、人工知 能に限らず、人間の思考過程を計算機に入力することは、コンピュータ・サイエ ンスの色々な分野で行われてきたことである。例えば、ソフトウェア工学の目標 は、ソフトウェアの生産性を向上させることであるが、そのための重要な方法は、 いままでのソフトウェアの蓄積をいかにして再利用し、空間軸と時間軸における ソフトウェア開発の重複を避けるかということである。このようなソフトウェア 再利用のターゲットは、プログラムのコードに限られるものではない。いわゆる、 プログラムの「スペック」である仕様記述、そして、究極的には、ソフトウェア の「開発過程」そのものの再利用も考慮されている。例えば、最近騒がれている (いた?)「プロセス・プログラミング」は、ソフトウェアの開発過程をプログラ ミング言語によって記述し、開発過程( プロセス)を記述したプログラム(プロセ ス・プログラム)を再利用しようとする試みである。すなわち、思考過程を記述 しようとする試みの裏には、何とかして「思考」という捉えどころのないものを 計算機にも理解できるような形式的な枠組で表現したいという純粋な動機だけで なく、あわよくば、その成果を用いて、思考の再利用、ひいては、思考の「売買」 をしようというもくろみが、もちろん、あるわけであるが、それはそれですばら しい。 ともかく、思考というものを形式的な枠組で記述し、計算機に入力しようという 試みは、計算機が発明されたときから行われてきたことである。さて、人間の思 考過程の中で、「形式化」悪くいえば「非融通化」に最も適したものは何であろ うか。いうまでもなく、論理学や数学における「証明」と呼ばれるものが、最も 形式化しやすいと考えられる。 それは、本当であるともいえるし、嘘であるともいえる。例えば、数学の本とい うのは形式的に書かれているだろうか、と考えてみる。問いを少し変えて、数学 というのは形式的な学問なのだろうか、と考えてみると、それは全く嘘である。 数学というのは、もちろん、集合論というハードウェアの中で行われているのだ ろうけれども、はっきりいって「数学的直感」なくしてはできないものであり、 従って、数学の本も「数学的直感」であふれており、むしろ、数学の本とは「数 学的直感」を養うためのものであるといえる。逆に、馬鹿ていねいで余りにも形 式的な数学の本は、数学の本としてはよくないものである。 余談だけれども、「彼は最近いい数学をしているなあ」とか「彼の数学は面白く ない」とか、数学の先生がおっしゃる。ここで、「数学」を「コンピュータ・サ イエンス」に置き換えて、「彼は最近いいコンピュータ・サイエンスをしている なあ」とか「彼のコンピュータ・サイエンスは面白くない」とかいってみても、 全然さまにならないのは、まあ、し方がないのだろう。 ということで、要するに、形式化しやすい証明とは、余り面白そうなものではな いが、それでも、実際の数学の証明を計算機上で表現するのは、非常に難しいこ とである。 計算機に定理の証明を行わせることを、「定理の自動証明」と呼ぶ。定理の自動 証明は人工知能の古典的な研究分野であり、レゾリューションを始めとする多く の技法が考案されてきた。これに対して、人間が証明を適当な形式言語で記述し、 証明が正しいかどうかを計算機にチェックさせることを、証明チェック (proof check)といい、証明のチェックを行うプログラム(処理系)のことを、証明チェッ カ(proof checker)と呼ぶ。つまり、証明チェッカを作って、実際の数学の証明 を計算機にチェックさせる、ということが、人間の思考過程を計算機上に表現し ようという試みにおける、出発点の一つなのである。 実際に、多くの人々が、証明チェッカの研究をしてきた。古くは、リチャード・ ウェイラックのFOL (これはPrologでおなじみの一階の述語論理の証明チェッカ である)、そして、新しくはICOTのCAPプロジェクトがある。 さて、証明チェッカを作る場合の最大の問題は、どのような論理体系を用いるか ということである。なるべくシンプルで、それでいてパワフルで、しかもフレキ シブル、余りしつこくなく、そして、なじみやすく使いやすい。ということで、 大変難しい。 世界で最初の大がかりな証明チェッカ・プロジェクトは、オランダのド・ブラウ ンのオートマス・プロジェクトであった。オートマスの採用した論理体系につい てはさておき、このプロジェクトは偉大な成果をあげた。ランダウのo(無限小) で有名なランダウという数学者が書いた「グルンド・ラーゲン」という解析学の 教科書がある。この本は(余り中身は知らないが)、数の定義から始まって、極限 の定義、そして微分積分へと進む、大学教養過程の解析学の教科書である。それ で、オートマス・プロジェクトの成果の一つは何かというと、この本一冊まるご と、オートマスの形式言語に翻訳し、その結果をオートマスの証明チェッカに通 して、実際にチェックを行ったということなのである。この偉大さは、例えば、 一階述語論理の枠組で、非常に簡単な算術の定理、例えば、「任意のd>0、n≧0 に対して、n=d*q+rとなるqとrがある」という「割り算の定理」を完全に形式的 に証明しようとすればわかる。また、プログラム検証のホーアの論理を知ってい る人が、非常に簡単なプログラムの正当性、例えば、「クイック・ソート」のプ ログラムが正しいことを完全に形式的に証明しようとすればわかる。要するに、 人間の「証明チェック」能力はおそるべきものなのであり、計算機には100行必 要なことが、人間には1行で足りてしまうということは、よくあることである。 実は、オートマス・プロジェクトが重要であるのは、グルンド・ラーゲンの成果 だけによるのではなく、オートマスの形式言語の重要性にもよっている。簡単に いうと、オートマスの形式言語では、証明をλ式で記述したのである。λ式とは、 LISPの基礎となった、関数を記述するための記法である。例えば、 x + x という式はxの2倍を表す式である。従って、 x |--> x + x という対応(xにその2倍を対応させる)は、一つの関数になっている。この関数を λ式で表すと、 λx(x + x) となる。いうまでもなくLISPでは (と、暗黙のうちに読者はLISPを知っていると 仮定してしまっているが)、 (lambda (x) (+ x x)) と書かれる。しかし、オートマスの形式言語は、純粋なλ算法(λ式の計算体系) やLISPとは異なり、型(type)を持った言語である。例えば、C言語やPascalでは、 整数とか文字とかが型であり、変数や式に対してはコンパイル時にその型が定ま る。例えば、 int fact(x) int x; { if (x == 0) return(1); else return(x*fact(x-1)); } というCのプログラムで、 xという変数の型はint(整数)、 x*fact(x-1)という式 の型もintである。このような言語では、型はデータの集合を表す。例えば、int という型は(32bit)整数データの集合を表し、 charという型は(8bit)文字データ の集合を表すのである。そして、xの型がintであるとは、 xがintの表す集合の 上を走る変数ということであり、 x*fact(x-1)の型がintであるとは、 x*fact(x-1)の値が必ずintの表す集合に入っているということである。 λ算法に型を導入したものを、「型付きλ算法」という。オートマスの形式言語 も、この型付きλ算法の一種なのであるが、型の用い方が大きく異なっている。 それは、「命題=型」の概念と呼ばれているものである。命題=型の概念について は後で詳しい説明を試みるが、簡単にいうならば、 型 = 集合 元 = 要素 という図式ではなく、 型 = 命題 元 = 証明 という図式が用いられるのである。つまり、オートマスの形式言語では、λ式が 集合の要素を表しλ式の型が集合を表すのではなく、λ式が証明を表し、λ式の 型は、そのλ式が証明している命題なのである。 実は、そのような考え方は、多くの人々が同時に発見し発展させたものであった。 その中で最も有名なものは、マルチン・レフの構成的型理論の体系であろう。そ れはともかく、多くの人々が同時に発見したということは、「命題=型」という 考え方が非常に普遍的であったという証拠である。 さて、オートマスの形式言語は、「命題=型」の考え方に従っているが、単なる 一つの論理体系というよりも、色々な論理体系(例えば、直観論理、様相論理、 時制論理、自省論理...)を定義する万能言語というべきものである。時と場合に よって必要とする論理体系は様々であるから、一つの論理体系に固定した形式言 語よりも、そのような万能言語の方が望ましいことは明らかだろう。ということ で、構成的型理論のマルチン・レフも、「ロジカル・フレームワーク」と呼ばれ る体系を提唱している。この体系は、エジンバラ大学等で洗練され、実際に証明 チェッカが作成されるに至っている。 ということで、以下、命題=型の考え方、そして、ロジカル・フレームワークに ついて簡単に解説してみたい。命題=型の考え方は、コンピュータ・サイエンス において非常に重要な概念であり、しかも、決して難解なものではない。にもか かわらず、日本語で平易に解説したものがいまだかつでないので、こうして、 7bitsの機会を借りて解説しようと思うのである。 その前に、準備として、「ディペンデントな型」について説明する。これは、命 題=型とは別にしても、非常に重要な概念であり、(筆者を含めたCプログラマに とっても)知っていて損にはならない話である。この概念も、残念ながら、平易 に解説したものがいまだかつてない。 ● ディペンデントな型 「ディペンデントな型」とは何か。平凡であるが最も身近な例を上げよう。 zeroarrayという関数を考える。 zeroarrayは、(非負)整数を一つもらって、そ の大きさの整数配列で要素が全部0のものを返すとものする。例えば、zeroarray が8 をもらったとすると、 zeroarrayは要素が全部0の大きさ8の整数配列を返す。 いま、いつものように、 Aという型の元をもらってBという型の元を返す関数の 型を A → B と書くことにする。また、整数の型をint、要素の型がEである大きさnの配列の 型を、 array(E, n) と書くことにする。すると、例えば、階乗を計算する関数factの型は、int→int となる。 aという式の型がAであることを、 a ε A というように、εという記号を使って書こう。すると、factの型がint→intであ ることは、 fact ε int → int と書くことができる。さて問題である。zeroarrayの型は何か。 factに8を入力 すると、 fact(8) = 40320 であり、すなわち、 fact(8) ε int である。また、 fact(10) = 3628800 であり、すなわち、 fact(10) ε int である。これは当り前である。 なぜなら、 f ε A → B で、 a ε A ならば、 f(a) ε B だからである。ここで、いうまでもなく、f(a)は、 fという関数をaという引数 に適用した結果を表す式である。 zeroarray(8)の値は大きさ8の整数配列だから、 zeroarray(8) ε array(int, 8) である。同様に、 zeroarray(10) ε array(int, 10) である。さて、zeroarrayの型が、 A → B と書けるならば、zeroarrayは、整数をもらうのであるから、 A = int である。そして、 zeroarray(8) ε array(int, 8) であるから、 B = array(int, 8) でなければならない。ところが、 array ε int → array(int, 8) とすると、 array(10) ε array(int, 8) となってしまい、 array(10) ε array(int, 10) と矛盾する。ということで、 zeroarrayの型は、A→Bという形では書けないので ある。こまった。ではどうするか。 まず、定義域がint(もしくはその部分集合)である関数は数列であるということ を思い出して欲しい(数列は関数であるといった方がいいかしらん)。いま、 [0..3] = {0,1,2,3} というように、[n..m]で、n以上m以下の整数の集合を表すとする。すると、 [0..3] → int とは、[0..3]からintへの関数の型であるが、 [0..3]→intの関数は、0に対する 値、1に対する値、2に対する値、3に対する値の四つの値(四つ組)を定めれば定 まる。つまり、[0..3]→intの関数は、整数の四つ組(四つの整数の列)と一対一 に対応するのである。 A × B で、AとBの直積(ウーン、直積ぐらいは知っているものとしますよ)を表すとする と、 [0..3] → int 〜 int × int × int × int ＝ となる。ここで、〜は集合の間の同型を意味している。要するに、左の集合の要 ＝ 素を何らかの方法で右の集合の要素と見ることができ、逆に、右の集合の要素を 何らかの方法で左の集合の要素と見ることができる、ということである。このよ うに、 A → B という関数の集合は、 B × B × B × B × B × B × B × B × ... ... A個 ... というように、BがA個(正確にはAの元の数だけ)、×で結ばれたものということ ができる。 さて、ここで、数列の和の記法を思い出そう。 3 2 Σ n n=0 2 とは、n を、nを0から3まで変化させたものについて全部足せ、ということを表 している。つまり、 3 2 2 2 2 2 Σ n = 0 + 1 + 2 + 3 n=1 ということである。これを、 [0..3]という記法を用いて、 2 Σ n nε[0..3] と書くこともある。つまり、 Σ f(n) nεA は、Aという集合の各元nについてf(n)を求め、それをすべて足し合わせたものを 表す。 +は結合的(かつ可換的)であるので、和の値はAの元をとる順番には依存 しない。 +(足し算)でなくて×(掛け算)を繰り返すこともできる。それには、Σでなくて Πを用いる。例えば、 (0-π)×(1-π)×(2-π)×(3-π) は、 3 Π (n-π) n=0 もしくは、 Π (n-π) nε[0..3] と書かれる。 ×という記号は、掛け算を表すこともあるが、上のように、集合や型の直積を表 すこともある。それに従って、Πも集合や型の積を表すことになる。いま、 [0..3] の元nに対して、 F(n) = int と定義する。つまり、Fは、いつも必ずintという型(集合)を返す関数である。す ると、 F(0) × F(1) × F(2) × F(3) = int × int × int × int であり、 Π F(n) = F(0) × F(1) × F(2) × F(3) nε[0..3] であるから、 Π F(n) = int × int × int × int nε[0..3] ということになる。 F(n) = int を上の左辺に代入すると、 Π int = int × int × int × int nε[0..3] となる(当り前だ)。ところで、 [0..3] → int 〜 int × int × int × int ＝ であったことを思い出すと、 [0..3] → int 〜 Π int ＝ nε[0..3] ということになる。これを一般化すると、 A → B 〜 Π B ＝ nεA となる。ただし、Bはnには依存しない型である。 上のFという関数の値である型(int)は、 nに依存していない。従って、 Π int nε[0..3] という積は、intが[0..3]の要素の数(4)だけ×で結ばれたものに過ぎない。では、 F(n) = array(int,n) だと、どうだろうか。 Fの値は次のようになる。 F(0) = array(int,0) F(1) = array(int,1) F(2) = array(int,2) F(3) = array(int,3) つまり、F(n)は大きさnのintの配列を表している。このFに対して、 Π F(n) = F(0) × F(1) × F(2) × F(3) nε[0..3] という式をあてはめると、 Π array(int,n) nε[0..3] = array(int,0) × array(int,1) × array(int,2) × array(int,3) となる。この型の元は何か。いうまでもなく、 array(int,0)の元 array(int,1)の元 array(int,2)の元 array(int,3)の元 の四つ組がこの型の元であるが、 [0..3]→intの関数がintの四つ組と対応して いたのと同様、上の四つ組も、 [0..3]の元をもらう関数とみなすこともできる。 ただし、関数の値の型が、関数の入力に従ってまちまちなのである。つまり、上 の四つ組を関数とみなしたとき、 0に対してはarray(int,0)の元 1に対してはarray(int,1)の元 2に対してはarray(int,2)の元 3に対してはarray(int,3)の元 を返す関数となる。つまり、 f ε Π array(int,n) nε[0..3] とすると、[0..3]の元nに対して、 f(n) ε array(int,n) となる。おお、これこそ、我々が求めていたものではなかっただろうか。つまり、 [0..3]の代わりにintを用いると、 Π array(int,n) nεint という型を考えることができる。 f ε Π array(int,n) nεint とすると、nεintならば、 f(n) ε array(int,n) となる。これは、まさしく、zeroarrayが満足すべき条件である。つまり、 zeroarray ε Π array(int,n) nεint である。 いくつかの注意が必要である。まず、 Π array(int,n) nεint において、Πの下はintだから、 array(int,-1) のような型も定義されていなくてはならない。ここでは、例えば、n<0ならば、 array(int,n) = array(int,0) とでも定義しておくことにする(大きさ0の配列は考えられる)。また、 Π array(int,n) nεint の中のnは、いわゆる束縛変数である。つまり、 int fact(n) int n; { if (n == 0) return(1); else return(n*fact(n-1)); } というＣプログラムと、 int fact(m) int m; { if (m == 0) return(1); else return(m*fact(m-1)); } というＣプログラムとが全く同じであるように、また、 λn(n + n) というλ式と、 λm(m + m) というλ式が、同じ関数を表現しているように、 Π array(int,n) nεint のnは、この式の中でのみ意味がある変数で、別の変数に置き換えてもよい。す なわち、 Π array(int,n) = Π array(int,m) nεint mεint である。 さて、一般的に、 B(x)が型を表す式で、xを含むとき、 Π B(x) xεA も型を表す式となる。また、fが上の型の元(fの型が上の式)で、 aがAの元(aの 型がA)ならば、 fをaに適用した結果、すなわちf(a)は、 f(a) ε B(a) となる。このことは、 f ε Π B(x) a ε A xεA ------------------------ f(a) ε B(a) というように推論規則の形で(かっこよく)書かれる。ここで、---の上側が規則 の前提、下側が規則の結論である。 値の型が入力によらずに一定している関数の型はA→Bと書かれるが、これは、Π を用いて、 Π B xεA と書くことができる。ただし、Bにはxが現れない、つまり、Bはxに依存しない。 Πの方が一般的だから、Πの方を主として、→はΠの略記と考えた方がよい。つ まり、 A → B = Π B xεA と定義してしまう。 さて、 Π B(x) xεA という型を、値の型が入力に依存するという意味で、「ディペンデント」な関数 型ということがある。ディペンデントな関数型は、ディペンデントな型の一つで ある。ディペンデントな型には、関数型の他に、ディペンデントな直積というも のがある。これは、組(ペア)の第二の要素の型が第一の要素に依存するというも のである。 型の直積は、実際のプログラミング言語では、レコードとかストラクチャという 形で提供されている。例えば、Pascalでは、レコード型が型の直積に相当する。 複素数はrealの組(ペア)であるから、 real × real の元と定義することができ、 x + yi という複素数は、 (x, y) ε real × real という組で表現される。Pascalでは、real×realは、 type complex = record re: real; im: real; end; というようなレコード型となる。reとimはこのレコードのフィールドである。 z: complex; と宣言すると、zの型はcomplexになり、その実部と虚部は、それぞれ、 z.re z.im で参照される。 なぜ、Ｃプログラマである筆者がＣのストラクチャを例としてあげなかったのか は、 Pascalのレコードにはバリアント・フィールドと呼ばれるフィールドがあ るからである。例えば、学生に関するstudentというデータ型を定義したいとす る。 studentには、sexという性別を表すフィールドと、 clubという所属クラブ を表すフィ-ルド、 gradeという学年を表すフィールド、そして、 sentaku_kamokuという選択科目を表すフィールドがあったとする。ただし、 sentaku_kamokuは各学年について異なるとする。すると、Pascalでは、バリアン ト・フィールドを用いて、 studentは次のように定義することができる。 type student = record sex: (male, female); club: (baseball, sumou, sadou, ... ); case grade: 1..3 of 1: (sekaishi, nihonshi); 2: (rinri_shakai, seiji_keizai); 3: (suugaku_3, koten_otsu); end; さて、このstudentという型を直積を用いて表そうとすると、 Sex = {male, female} Club = {baseball, sumou, sadou, ...} とおいて、 Sex × Club × [1..3] × ... となりそうなのであるが、 ... のところが困ってしまう。 ... のところは、三 番目の要素が[1..3]のどれをとるかによって異なるからである。これを解決する のが、デペンデントな直積と呼ばれるものである。 デペンデントな直積では、デペンデントな関数型におけるΠの代わりにΣを用い る。すなわち、 Σ B(x) xεA は、Aの元xとB(x)の元yの組(x,y)の集合を表す。ここで、B(x)のxは、B(x)がxに 依存することを表している。簡単な例をあげよう。 Σ (if x=1 then [1..2] else if x=2 then [3..4] else [5..6]) xε[1..3] 余りよい例ではないが、 (1, 2) は上のディペンデントな直積の元である。なぜなら、組の第二要素である2は、 (if x=1 then [1..2] else if x=2 then [3..4] else [5..6]) のxのところに第一要素である1を代入したもの、すなわち、 (if 1=1 then [1..2] else if 1=2 then [3..4] else [5..6]) = [1..2] の元だからである。同様に、 (2, 3) (3, 6) も上のディペンデントな直積の元である。 さて、このΣを用いれば、先のstudentは、 Sex × Club × Σ (if x=1 then {sekaishi, nihonshi} ) xε[1..3] (else if x=2 then {rinri_shakai, seiji_keizai}) ( else {suugaku_3, koten_otsu} ) となる。 プログラムを書いていると、 zeroarrayやstudentに限らず、ディペンデントな 型が必要な場面が多々あるわけで、ディペンデントな型というものは、そのよう に身近なものなのである。 ● 命題=型 命題=型の概念は、構成的な証明と呼ばれるものを考えたときに最も理解しやす い。構成的な証明とは、簡単にいうと、具体的なものを提示して行う証明のこと である。例えば、方程式に解があることを証明する場合、実際に解を構成してみ せる証明が、構成的な証明である(しつこい)。 任意の整数(自然数)に対して、それよりも大きな素数があることはよく知られて いる。その証明を復習してみよう。自然数nが与えられたとき、 q = ( Π i) + 1 iε[1..n] とおく。そして、qを素因数分解する。その素因数の中の一つ(例えば最小のもの) をpとする。すると、p>nのはずである。なぜなら、p≦nならば、qをpで割った とき、1余ってしまうからである。以上の証明は構成的である。なぜなら、自然 数nが与えられたとき、上の証明に従えば、 nよりも大きい素数pを実際に得るこ とができるからである。従って、証明が関数となっているといってもよい。 --------------------- ここでfのグラフ。 f(1) = 2 f(2) = 3 f(3) = 7 f(4) = 5 f(6) = 721 f(7) = 71 --------------------- nより大きい素数の集合をprime(n)で表すと、上の証明(fとおく)を関数とみなし たとき、 f ε Π prime(n) nεint となる。ここで、 Π prime(n) nεint は、先に説明したディペンデントな関数型で、 nを入力とし、prime(n)の元を返 す関数の型を表している。ここでよく考えて見よう。上の関数型を持つ関数が存 在することを示せば、「任意のnに対してnよりも大きい素数がある」ということ が示されたことになる。逆に、「任意のnに対してnよりも大きい素数がある」と いうことを、構成的に証明するとは、上の関数型を持つ関数を実際に定義するこ との他ならない。ということは、 Π prime(n) nεint という関数型は、「任意のnに対してnよりも大きい素数がある」という命題を示 しているのではないか。ここで、次のような対応が考えられるのである。 命題 = 関数型 証明 = 関数 もう少し説明しよう。 prime(n)は、nより大きい素数の集合であると述べたが、集合は一般に、その集 合が空でないという命題と対応させられる。 prime(n)に対しては、「nより大き い素数の集合が空でない」ということは、「nより大きい素数が存在する」とい うことである。そして、 Π prime(n) nεint という関数型が空でない、つまり、この型を持つ関数があるということは、「任 意のintの元nについて、nより大きい素数が存在する」という命題を意味すると 考えられる。つまり、型を命題とみなした場合、 Π ... nεint という型は、「任意のintの元nに対して、... 」という意味になる。ここで、一 階述語論理というものをご存じの読者に対するコメントである。一階述語論理で は、「任意のnに対して、... 」ということを、 ∀n ... という記号で表す。∀は「全称記号」と呼ばれる記号である。上の記法では、x が動く集合(変域)が明示されていないが、例えば、 ∀nεint ... と書くことにすれば、 Π ... <--> ∀nεint ... nεint という対応が得られるのである。 また、AとBの直積A×Bに対しては次のことが成り立つ。 A×Bが空でないための 必要十分条件は、 Aが空でなく、かつ、Bが空でない。実際、A×Bが空でなけれ ば、 (a,b) ε A × B という組があるから(aεA、bεB)、AもBも空ではない。また、 a ε A b ε B ならば、 (a,b) ε A × B である。ということで、 A × B <--> A ∧ B という対応が得られる。ここで、∧は一階述語論理で「かつ」を表す記号である。 ところで、[0..3]に対して、 ∀nε[0..3] F(n) = F(0) ∧ F(1) ∧ F(2) ∧ F(3) Π F(n) = F(0) × F(1) × F(2) × F(3) nε[0..3] であるから、実にみごとに対応しているのである。 次に、Prologでおなじみの「ソクラテスは死すべきものである」の証明を考えて みよう。例によって、 ソクラテス <--> Socrates xは死すべきものである <--> Mortal(x) xは人間である <--> Human(x) と表すとする。 Human(x)ならばMortal(x)であるが、これは、 ∀x(Human(x) → Mortal(x)) と表される。ここで、xの変域は何だろう。知能を持つものの全体、特に、人間 や神やロボットを意味するものと思われる。すなわち、神やロボットは知能を持 つが死なない。知能を持つものの全体をIntelligentと書くことにすると、 ∀xεIntelligent(Human(x) → Mortal(x)) となる。また、 ∀xεIntelligent(God(x) → Mortal(x)) ∀xεIntelligent(Robot(x) → Mortal(x)) は成り立たない。 さて、上の命題の中のHuman(x)もMortal(x)も集合を表しているとは思われない。 しかし、それではうまくないので、これらを何とか集合(型)と思いたい。そこで、 Human(Socrates) を、「Socratesが人間であるということの証拠」の集合と考えるのである。つま り、Human(Socrates)が成り立つとは、 Socratesが人間であるということの証拠 がある、ということと考える。例えば、 Socratesが屁をした Socratesがカラオケを歌った という事実は(神やロボットはそのようなことをしないだろうから)、 Human(Socrates)の元であるといえる。また、 Mortal(Socrates) は、「Socratesは死すべきものであることの証拠」の集合である。すると、 Human(Socrates) → Mortal(Socrates) は、→が関数型を表すとすれば、「Socratesが人間であるということの証拠」が 与えられたとき、「Socratesは死すべきものであることの証拠」を返す関数の型 である。もし、この型が空でなければ、すなわち、このような関数があるとすれ ば、 Human(Socrates)が空でないとき、すなわち、「Socratesが人間であるとい うことの証拠」があったとき、その証拠を関数に入力すれば、「Socratesは死す べきものであることの証拠」が返される、ということは、Mortal(Socrates)が空 でないということである。以上をまとめると、 Human(Socrates) → Mortal(Socrates) が空でないとは、 Human(Socrates) ならば Mortal(Socrates) という命題が成立していることを意味する。つまり、関数型を表す→は、論理記 号として「ならば」と読むことができるのである。これを「ならば」の構成的な 解釈という。 ------------------------------------- ここで、ソクラテスがカラオケを歌う絵。 ------------------------------------- 一階述語論理では、「ならば」は正式には⊃と書くので、 → <--> ⊃ という対応になる。 さて、Mortal(Socrates)を証明するとき、 Human(Socrates) と Π (Human(x) → Mortal(x)) xεIntelligent を仮定する。「仮定する」とはどういうことかというと、これらの集合(型)が空 でないことを仮定することである。空でないことを仮定するには、これらの集合 の中にあるものを仮定すればよい、ということで、これらの集合上の変数を宣言 すればよい。例えば、 p ε Human(Socrates) と宣言することは、Human(Socrates)と仮定していることになる。ここで、pは変 数である。同様に、 q ε Π (Human(x) → Mortal(x)) xεIntelligent とする。すると、qの型から、 q(Socrates) ε Human(Socrates) → Mortal(Socrates) となる。 q(Socrates)も関数である。その型とpの型から、 q(Socrates)(p) ε Mortal(Socrates) となる。 q(Socrates)(p)は、q(Socrates)という関数をpに適用したものである。 q(Socrates)(p)の型がMortal(Socrates)ということは、 Mortal(Socrates)が空 でないということを意味している、従って、Mortal(Socrates)が証明された。 q(Socrates)(p)はその証明である。 以上で、次のような対応がおわかりいただけたと信じたい。 型 = 集合 = 命題 元 = 要素 = 証明 要素や証明を表現するものとして、「式」がある。式としては、 LISPのもとに なったλ式を用いるのが最も一般的である。また、集合や命題のどちらも、式の 型となるわけだが、こちらもΠやΣ等のオペレータはあるにしろ、同じようなλ 式で表現することができる。 さて、「証明」という「ちみもうりょう(漢字で)」としたものが、我々にとって 馴染みの深い、λ式として表現できるということは、非常に嬉しいことである。 関数型言語では、λ式はプログラムとなるから、プログラムを書くような気分で 証明を書ける可能性が出てくる。 さて、もう少し我慢して欲しい。 f ε A → B a ε A --------------------- f(a) ε B という規則を、命題=型の考えによって解釈すると、 AとA→Bが成り立てば、Bが 成り立つ、と読むことができる。おお、これは、三段論法(モーダス・ポネンス) に他ならないではないか。なんと、論理法則は、型チェックの規則でもあったの である。 また、 xεA のもとで bεB(x) ------------------------ (λxεA b) ε Π B(x) xεA という規則がある。例えば、xεintという仮定のもとでx+xεintだから、 λxεint(x + x) ε Π int = int → int xεint となる。じつは、この規則は、⊃の導入、∀の導入という論理法則に対応するの である。ふっふっふっ。 ● ロジカル・フレームワーク さて、以上のような「命題=型」の概念から、もう一段だけ、階段を登ったとこ ろに、ロジカル・フレームワークの世界がある。ここでは、簡単な例をあげて説 明しようと思う。 ロジカル・フレームワークでは、型の型を考え、これを、種(kind)と呼んでいる。 つまり、 種 ｜ 型 ｜ 元 という三段の構造になる。代表的な種は、 Type と書かれるものである。これは、型の型(type of type)を意味している。Type の元が型である。すなわち、Aが型であるということは、 A ε Type が成立することに他ならない。また、Typeの元を動く変数を宣言することもでき る。つまり、 P ε Type と宣言すると、これは、Pを型であると仮定したことに相当する。すると、型に 対しては、その元を動く変数を宣言できるので、 p ε P と宣言できることになる。 また、Aが型のとき、すなわち、AεTypeのとき、 A → Type も種であると定義される。これは、もちろん、AからTypeへの集合を表している。 A→Typeという形の種に対しても、その元を宣言することができる。すなわち、 P ε A → Type のような宣言を行うことができる。同様に、 A → (B → Type) のようなものも種である。 一般的に、Kが種で、Aが型ならば、 A → K も種である。 Kが種ならば、Kの元を動く変数を宣言できる。 P ε K また、Aが型(AεType)ならば、Aの元を動く変数を宣言できる。 x ε A さて、次のような宣言を(順に)して行こう。 Minna ε Type Minnaは型である Minnaとは「皆」のことである。 Prop ε Type Propは型である Propは、命題(proposition)の型を意味する。いままでは命題=型(Prop=Type)で あったのに、ここではPropεTypeと定義している。その代わり、後で、命題を型 に変換するTrueという関数を宣言する。 Hanako ε Minna HanakoはMinnaの一人である Taro ε Minna TaroはMinnaの一人である Hanako(花子)とTaro(太郎)は「皆」の一人である。 MinnaεTypeなので、Minna の元を宣言することができる。 Loves ε Minna → (Minna → Prop) Lovesは、Minna上の二項関係と考えることができる。つまり、aεMinna、bε Minnaならば、 Loves(a)(b) ε Prop である。なお、Loves(a)(b)等は見にくいので、 Loves(a, b) のように書いてしまうことにする。 Implies ε Prop → (Prop → Prop) Impliesは「ならば」を意味するProp上の二項関数である。すなわち、PεProp、 QεPropならば、 Implies(P, Q) ε Prop である。 Impliesと→の関係については、すぐ後で述べる。 Knows ε Minna → (Prop → Prop) Knowsは、「知っている」という命題を表す。すなわち、aεMinna、PεPropのと き、 Knows(a, P) ε Prop で、Knows(a,P)は、aがPを知っているという意味である。 命題を型にするために、次のTrueという変数を宣言する。 True ε Prop → Type PεPropならば、 True(P) ε Type である。つまり、Propの元Pに対して、True(P)は「Pは真である」という命題 を表す。 Pは型ではないのに対して、True(P)は型になっているので、True(P) の元を考えることができる。True(P)の元とは、もちろん、「Pは真である」と いうことの証明である。 なお、Prop→Typeは種であるので、その元であるTrueを宣言することが できるのである。 Impliesと→を結びつけるためには、次のax0を宣言すればよい。 ax0 ε Π Π True(Implies(P, Q))→(True(P)→True(Q)) Pεprop Qεprop 例えば、 a ε True(Implies(P, Q)) b ε True(P) であったとしよう。すると、 ax0(P, Q, a, b) ε True(Q) となる。つまり、ax0は、 Implies(P, Q) P ------------------ Q というモーダス・ポネンスを表している。 Impliesの他に、AndやOrやAll等を導入し、一階の述語論理を完全に展開するこ ともできるが、それは、読者への演習問題としよう。ここでは、「知っている」 ということに関する議論を進めたい。 「花子は太郎を愛している」と仮定しよう。このために、 Hanako_Loves_Taroと いう変数を宣言する。 Hanako_Loves_Taro ε True(Loves(Hanako,Taro)) また、「誰でも、自分が誰かを愛していれば、そのことを本人は知っている」と いうことは、次のように表される。 ax1 ε Π Π True(Loves(x,y))→True(Knows(x,Loves(x,y))) xεMinna yεMinna 「花子は、自分が愛している人は自分を愛してくれていると思っている」 ax2 ε Π True(Knows(Hanako,Implies(Loves(Hanako,x), xεMinna Loves(x,Hanako)))) また、誰でも、自分の頭の中で三段論法を行える。 ax3 ε Π Π Π True(Knows(x Implies(P,Q))→ xεMinna Pεprop Qεprop (True(Knows(x,P))→True(Knows(x,Q))) すると、次のような証明が行える。 ax3(Hanako,Loves(Hanako,Taro),Loves(Taro,Hanako), ax2(Taro),ax1(Hanako,Taro,Hanako_Loves_Taro)) ε True(Knows(Hanako,Loves(Taro, Hanako))) つまり、「花子は太郎が自分のことを愛していると思っている」 以上、簡単なknowledge logic(知識に関する論理)を、ロジカル・フレームワー の中で表してみた。書いている本人は、非常に楽しい (ただし、読んでいる人は どうかな)。ともかく、非常にフレクシブルでパワフル、しかもシンプルな形式 体系であり、様々な論理体系を簡単に定義することができる。 将来、色々な分野で応用されるようになるかもしれない。つづく。