- 締切済み
【関数型言語,論理学】推論して関数を自動生成する
こんにちは。 関数型言語(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という、計算機で証明を行うプログラミング言語があるというのは知っていますが勉強したことが無いのでよくわかりません。 よろしくお願いします。
- 数学・算数
- 回答数3
- ありがとう数0
- みんなの回答 （3）
- 専門家の回答
みんなの回答
- stomachman
- ベストアンサー率57% (1014/1775)
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を証明システムと思うな、探索システムだと思え、と申し上げたんですけどね。ご質問の課題の場合には、上記の通り、単純な探索をやるだけですから、これで充分。
- stomachman
- ベストアンサー率57% (1014/1775)
（(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を使ってこのご質問を解決するプログラムを書くことも。
- Tacosan
- ベストアンサー率23% (3656/15482)
関数に対してどのような操作ができるのかをはっきりさせた方がいいとは思うが, とりあえず「ある関数の値を別の (あるいは同じ) 関数の引数とする」こと (その特殊な場合が関数合成) ができないとどうにもならないのでそれはあるとする. それを仮定してしまえば, 関数の引数・返り値の型に対して Horn節のような形で記号化できるから, Prolog的なにかで処理できる... かな?
関連するQ&A
- Ｃ言語のポインタの考え方について
ポインタについて理解ができていないのでお聞きしたいのですが 値を交換する関数のプログラミングでこの場合ポインタ で以下にしないといけないと思います。 #include<stdio.h> void swap(int *a int *b){ int c; c=*a; *a=*b; *b=c; } main(){ int x,y; x=123; y=456; swap(&x,&y); printf("x = %d, y = %d＼n", x, y); } またポインタを使用せず以下のプログラムではなぜダメのでしょうか。 よろしくお願い致します。 #include<stdio.h> void swap(int a int b){ int c; c=a; a=b; b=c; } main(){ int x,y; x=123; y=456; swap(x,y); printf("x = %d, y = %d＼n", x, y); }
- ベストアンサー
- C・C++・C#
- C言語の関数に関する質問ですが
C言語の初心者です。よろしくお願いいたします。 授業でこのような演習が出ました。 演習：実数x を入力したときの最大値を求めるプログラムを作れ． 実数x を入力すると，x; -x; x2; xの絶対値の平方根 の中で一番大きい値を答える プログラムを作れ（ファイル名はmax.c とする）． 表示は以下のようにする． Input x: -0.5 【Enter】 Answer is 0.707107. #include<stdio.h> #include<math.h> double max(double a, double b){ if( a > b) return a; else return b; } int main(void) { double x,y; printf(\"Input x: \"); scanf(\"%lf\",&x); y = max (x,-x); y = max (y,x*x); y = max (y,sqrt(fabs(x))); printf(\"Answer is %f.\\n\",y); } このように書けばうまく実行できますが、関数の中に関数を使えないでしょうか。うまく言えないですが、たとえば、以下のように書いてみましたが、うまく実行できません。どう直したらいいでしょうか、お忙しい中教えていただけたらうれしいです。 #include <stdio.h> #include <math.h> int max(double a,double b) { if (a<b) return b; else return a;} int main(void) { double x,result; printf(\"Input x:\"); scanf(\"%lf\",&x); result=max(max(x,-x),max(pow(x,２),sqrt(fabs(x)))); printf(\"%.2f\",result); return 0; } よろしくお願いいたします！！
- ベストアンサー
- C・C++・C#
- main関数以外での結果の表示？
C言語で関数を用いたプログラムを作成しています。内容はA君、B君のボーリングの成績を入力し、その点数をランク付けするというものです。（２５０以上はS、200以上はA、150以上はB、100以上はC、50以上はD、５０未満はFになります。） それから、このプログラムの条件は １、main関数は値の入力と関数を呼び出すだけ。 ２、関数の引数は入力した２つの値。 ３、関数の中で結果を表示。 ４、関数の戻り値はなし。 というもので、3番の結果のmain関数以外での結果の表示の仕方がわからず、どうやって結果を表示させていくのかよくわからず、行き詰っています。そのあたりの解説をしていただくとありがたいです。 なお、私が途中まで書いたので、問題点の指摘をおねがいいたします。 #include<stdio.h> int ia(int x); int ib(int y); int main(){ int a,b; printf("A君のスコア"); scanf("%d",&a); printf("B君のスコア"); scanf("%d",&b); } int ia(int x); char ix; if(x>=250){ ix = 'S'; }else if(x>=200 && x<250){ ix = 'A'; }else if(x>=150 && x<200){ ix = 'B'; }else if(x>=100 && x<150){ ix = 'C'; }else if(x>=50 && x<100){ ix = 'D'; else{ ix='F'; } int ib(int y); char iy; if(y>=250){ iy = 'S'; }else if(y>=200 && y<250){ iy = 'A'; }else if(y>=150 && y<200){ ix = 'B'; }else if(y>=100 && y<150){ iy = 'C'; }else if(y>=50 && y<100){ iy = 'D'; }else{ iy ='F'; }
- 締切済み
- C・C++・C#
- C言語 関数の問題
C言語（関数の問題）で読み込んだ４つの整数の最大値を求めプログラムで 整数を２つペア比較し、関数の入れ子を用いて最大値を見つけて、表示する。 というプログラムを作成したいのですが #include<stdio.h> int maxof(int a, int b) { if(a > b) return (a); else return (b); } int max4(int a, int b, int c, int d) { max(max(a, b), max(c, d)); } int main(void) { int num1,num2, num3, num4; ------ 整数の読み込み printf("最大値は%dです。", max4(num1, num2, num3, num4)); return(0); } と記述すると、上手くいったのですが これを max関数だけを用いて作成できますでしょうか？ 整数の比較は全てmax関数で行いたいです。
- 締切済み
- 情報工学
- 関数原型宣言について
関数原型宣言について 下記のプログラムのfunc関数は、関数原型宣言 <func(int a, long b, char *c);>が述されていないのにfunc関数の仮引数の型longは、関数原型宣言が与えられるといると本に書かれていたのですが、何故でしょうか教えて頂きたい。 ******************************************** #include <stdio.h> /*--- 三つの引数を受け取る関数 ---*/ void func(int a, long b, char *c) { int x; long y; /* … */ } int main(int argc, char *argv[]) { int a = 1; char s[] = "abc"; func(a + 3, 2, s); return (0); } *************************************************************
- ベストアンサー
- C・C++・C#
- C言語の実数型の足し算
C言語初心者です。関数の勉強していて、実数型計算に出くわしました。 #include <stdio.h> float add(float a, float b) { return a+b; } int main(void) { float x=10.5,y=20.3; printf("%f %f\n",x,y); printf("%f\n",add(x,y)); return 0; } としたら、 10.500000 20.299999 30.799999 という結果になりました。今のところint型でずーっと勉強していたので、20.3の20.299999表記が怪しく感じられ、結果も同様に怪しく感じられます。どうして、10.5+20.3=30.8とすっっきり表示してくれないのでしょうか。
- ベストアンサー
- C・C++・C#
- 至急お願いします！
至急お願いします！ a,b,c,dを定数とする。またwはx,y,zから w=ax+by+cz+dによって定まるものとする。以下の命題を考える。 命題1: x≧0かつy≧0かつz≧0 ⇒ w≧0 命題2: 「x≧0かつz≧0」または「y≧0かつz≧0」 ⇒ w≧0 命題3: z≧0 ⇒ w≧0 以下の問いに答えよ。 (1) b=0かつc=0のとき、命題1が真であれば、a≧0かつd≧0であることを示せ。 (2) 命題1が真であれば、a,b,c,dはすべて0以上であることを示せ。 (3) 命題2が真であれば、命題3も真であることを示せ。 どなたかお願いします(>_<)
- ベストアンサー
- 数学・算数
- C言語：構造体、自作関数についての質問
こんばんは C言語の問題を提示されてなんとか作成していますが構造体と自作関数の変数の値を返したりするのが上手くいきません。 問題 「(1)x座標およびy座標のペアとして構成される構造体pointを定義せよ（両座標は整数であるとする） (2)x座標およびy座標のメンバに値を設定し、その構造体を返す関数 struct point pointof(int a,int b){………}を作成せよ。 (3)二つの座標a,b間の距離を計算する関数 double distanceod(struct point a,struct point b); を作成せよ。 ※sqrt関数を使用せよ」 という問題です。メンバについてもいまいちよくわかりません。 どこでintを使うのか、またmainに値を返すやり方も上手くいかずコマンドプロンプトにはねられてばかりです。 どなたか解説おねがいしますm(_ _)m
- ベストアンサー
- C・C++・C#
- 関数の引数と実引数の取り扱いについて
C言語初心者です． 関数の引数と実引数の取り扱いについて，教えていただきたいことがあります． 例えば，2変数の和を求める関数を考えると，以下のようになると思います． #include <stdio.h> double sum(double x, double y); int main(void) { double a, b, wa; a=2.0; b=3.0; wa=sum(a,b); return 0; } double sum(double x, double y) { double total; total=x+y; return total; } このとき，mainプログラムでは，a,bふたつの変数を定義しておいて，関数sumに入れて計算させているわけですが，mainプログラムで変数x,yを定義しておいて，以下のようなプログラムにするのはありでしょうか？ 参考書などをみると，前者のように取り扱っているようなのですが，試しに後者で実行させてみても同じ結果となりました． #include <stdio.h> double sum(double x, double y); int main(void) { double a, b, wa; a=2.0; b=3.0; wa=sum(a,b); return 0; } double sum(double x, double y) { double total; total=x+y; return total; }
- ベストアンサー
- C・C++・C#
- 二つ以上の値を返す関数
たとえば、a,bという値を関数に入れて、関数の中で変わったa,bを受け取るような方法はないでしょうか。 http://oshiete1.goo.ne.jp/kotaeru.php3?q=138798 の int main(void) { int a=1, b=2; func(&a, &b); printf("%d, %d\n", a, b); return 0; } void func(int *x, int *y) { *x++; *y++; } を実行してみましたが、 「関数 'func' は定義されていません。int 型の値を返す外部関数と見なします。」 と出てきました。 助言をよろしくお願いします。
- ベストアンサー
- C・C++・C#
補足
回答ありがとうございます。 早速prologを使ってみましたが、果たしてprologに反例を出す能力はあるのでしょうか。 出力はtrueかfalse、もしくは変数を持つ述語を真にするその変数の中身、ぐらいだと思いました。 また調べたところ、prolog内の変数は全て全称量化されてるらしいです。 これでは存在量化子を用いた証明がやりにくくなります。 prologが僕がやろうとしていることの手助けになるとは思えません。 よろしくお願いします。