【関数型言語,論理学】推論して関数を自動生成する

こんにちは。
関数型言語(haskell)や論理学を独学している者です。
勉強中ふと思ったことがあるので質問します。（以降、表記はhaskell文法に倣います）

例えば今、我々に与えられた関数は
（x -> Int）型の関数fと、（Int -> y） 型の関数gと（(b -> c) -> (a -> b) -> a -> c）型の関数(.)だけだとします（a,b,c,x,yは全て型変数）。それ以外の関数は存在しません。
この時、(x -> y) 型の関数hは例えば(g . f)と表せると思います。
Int=b, x=a, y=cとみなせば、hは簡単に作れます。
しかし、それはあくまで人間にとって簡単だということです。
これを「計算機が作る」ことは可能でしょうか。
つまり、与えられた関数（と型の情報）だけで特定の型の関数を自動生成できるプログラムは存在し得るか、ということです。

カリー＝ハワード同型対応という性質がありますね。これは簡単に言うと「ある型を持つプログラム（関数）が一つでも書ければその型に対応した命題は真」ということだと思いますが、僕が聞きたいのは「その命題（型）が真かどうか分からないけど、前提は用意するので証明（プログラム）は計算機に任せてもいいのか」ということです。
CoqやPrologという、計算機で証明を行うプログラミング言語があるというのは知っていますが勉強したことが無いのでよくわかりません。

よろしくお願いします。

No.3 回答者： stomachman 回答日時： 2013/09/16 11:02

ANo.2へのコメントについてです。

> 早速prologを使ってみましたが、果たしてprologに反例を出す能力はあるのでしょうか。

　わー、早いですね。もう使いこなせていると？　ですが、肝心のパターンマッチングは理解できましたか？

> 変数を持つ述語を真にするその変数の中身

　最も単純なのは変数がない場合で、答はtrueかfalse。次が単に変数を1個書いただけの式の場合で、答はxにマッチする具体例。でもこんな使い方ではパターンマッチングの有り難みが分かりません。
　式同士のマッチングができるのが値打ちなんです。たとえば(x,y,a,b,c,dを変数として) (x -> y)と ((a -> b) -> (c->d))はマッチする（実際、xと(a ->b), yと(c->d)をそれぞれ対応させれば良い）。これをprologが判定できるってことを、確認してみて下さい。
　ご質問にある例題の場合は、aとx, bとInt, cとyをそれぞれ対応させればマッチする。で、この対応を見つけるまで、あらゆる組み合わせ (たとえば、aと(x -> Int), bとy, cとyをそれぞれ対応させる、など）を機械的に探索するだけです。


> これでは存在量化子を用いた証明がやりにくくなります。

　自動証明では、まず∃で束縛された変数をスコーレム関数で置き換え、限量記号を全部取り除いてから扱う。これは導出原理でも同じことです。ただし、命題を黙って放り込めば済む導出原理とは違って、プログラミングによって問題に応じた探索順序を指定してやる必要があるのが線形導出です。ヒトの知恵が必要なので、真の意味での「自動証明」とは言えない。
　だから、prologを証明システムと思うな、探索システムだと思え、と申し上げたんですけどね。ご質問の課題の場合には、上記の通り、単純な探索をやるだけですから、これで充分。

No.2 回答者： stomachman 回答日時： 2013/09/15 07:15

　（(b -> c) -> (a -> b) -> a -> c）, （x -> Int）, （Int -> y）から (x -> y) を作るという話は、要するに「変数や定数やそれらを組み合わせた式同士が互いに矛盾なく対応するような対応付けをすべて求む」ということであり、まさにこれをやる再帰的アルゴリズム「パターンマッチング」が、（お書きの通り）prologの核心にほかなりません。

　一階述語論理の証明の完全な（どんな命題XでもXかその否定を証明できる）アルゴリズムは「導出原理」という名で知られています(1960年だと思う）。しかしこれはひどく計算量が大きいしメモリも喰うんです。そこで、相手にできる命題の形に制限を付ける代わりに効率を高くしたのが「線形導出」と呼ばれる一群のアルゴリズムであり、その一種を実装したのがprologです。（1970年代後半だと思う。）
　そういう出自があるから、prologがやることを「計算機で証明を行う」と要約して分かった気になる人が多い。ですが、その証明ってのは（導出原理と同じく）「『（(b -> c) -> (a -> b) -> a -> c）, （x -> Int）, （Int -> y）から (x -> y) を作ることはできない』という主張に対する反例（つまり実際に作ってみせた例）をすべて探す」というやりかたで行われる。要するに、総当たりでパターンマッチングをやってみて反例を探索(search)するんです。この「総当たり探索」を再帰的に行うことが、prologのもう一つの核心です。（核心とは言っても木の探索をやるだけですから、実に簡単な話。）なので、prologは「デキアイの汎用総当たり探索プログラム」として利用されることが多い。「反例が見つからなければ証明、見つかれば反証」と解釈すれば、なるほどこれは証明をやってることになるけれど、そうではなしに（あるはずだと分かってる）反例を具体的に得ることを目的として使う訳です。

　ですから、prologを「既成のプログラミング言語」だと思わないで、単なるひとつの探索プログラムだと思えば、「よくわかりません」で切り捨てる必要はない。たいして複雑じゃないんです。実際、prologのインタープリタをLispで書けば、パターンマッチングと探索を実装するだけなので半ページぐらいで書ける。BASICで書けば数ページぐらいになるけれども、それは主にパージング（入力された文字列から内部表現への変換）とメモリ管理（アロケーションとガベージコレクション）を書く必要があるからで、パターンマッチングと探索についてだけなら半ページ程度。prologで書けば、パターンマッチングと探索が既に組み込まれているんで3行ぐらいで済む。その程度の規模のプログラムです。
　prologから（実用性のために追加された）「カット演算( ! )」や「副作用」を除けばごくシンプルなシステムで、haskellが分かる人なら1時間もあれば理解できるでしょ。ポイントはパターンマッチングを理解することですが、下手な入門書だときちんと書いてないかも知れない。むしろインタープリタのソースを読む方が確実じゃないかな。Lispによる実装なら簡単にみつかるはず。

　prologのインタープリタをhaskellで書くのは雑作もないでしょう。haskellでもパージングやメモリ管理は必要ないから、たいした規模になるはずがない。もちろん、prologを使ってこのご質問を解決するプログラムを書くことも。

この回答への補足

回答ありがとうございます。
早速prologを使ってみましたが、果たしてprologに反例を出す能力はあるのでしょうか。
出力はtrueかfalse、もしくは変数を持つ述語を真にするその変数の中身、ぐらいだと思いました。
また調べたところ、prolog内の変数は全て全称量化されてるらしいです。
これでは存在量化子を用いた証明がやりにくくなります。
prologが僕がやろうとしていることの手助けになるとは思えません。
よろしくお願いします。

補足日時：2013/09/16 01:59

No.1 回答者： Tacosan 回答日時： 2013/09/15 02:24

関数に対してどのような操作ができるのかをはっきりさせた方がいいとは思うが, とりあえず「ある関数の値を別の (あるいは同じ) 関数の引数とする」こと (その特殊な場合が関数合成) ができないとどうにもならないのでそれはあるとする.

それを仮定してしまえば, 関数の引数・返り値の型に対して Horn節のような形で記号化できるから, Prolog的なにかで処理できる... かな?