【関数型言語,論理学】推論して関数を自動生成する
こんにちは。
関数型言語(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という、計算機で証明を行うプログラミング言語があるというのは知っていますが勉強したことが無いのでよくわかりません。
よろしくお願いします。
お礼
ありがとうございます。 自分としてはhaskellをやってみようと思います。