Lisp Scheme Part19

1 名前：デフォルトの名無しさん mailto:sage [2008/01/14(月) 00:14:56 ] 過去スレ Part18: ttp://pc11.2ch.net/test/read.cgi/tech/1186922295/ Part17: ttp://pc11.2ch.net/test/read.cgi/tech/1177065699/ Part16: ttp://pc11.2ch.net/test/read.cgi/tech/1172404795/ Part15: ttp://pc10.2ch.net/test/read.cgi/tech/1151025773/ Part14: ttp://pc8.2ch.net/test/read.cgi/tech/1132275726/ Part13: ttp://pc8.2ch.net/test/read.cgi/tech/1115901841/ Part12: ttp://pc8.2ch.net/test/read.cgi/tech/1100229366/ Part11: ttp://pc5.2ch.net/test/read.cgi/tech/1091456033/ Part10: ttp://pc5.2ch.net/test/read.cgi/tech/1075630259/ Part9: ttp://pc2.2ch.net/test/read.cgi/tech/1069594582/ Part8: ttp://pc5.2ch.net/tech/kako/1058/10582/1058263391.html Part7: ttp://pc5.2ch.net/tech/kako/1042/10421/1042167213.html Part6: ttp://pc3.2ch.net/tech/kako/1031/10315/1031560687.html Part5: ttp://pc3.2ch.net/tech/kako/1023/10230/1023091882.html Part4: ttp://pc.2ch.net/tech/kako/1016/10162/1016211619.html Part3: ttp://pc.2ch.net/tech/kako/1008/10082/1008220265.html Part2: ttp://pc.2ch.net/tech/kako/1002/10025/1002584344.html Part1: ttp://piza2.2ch.net/tech/kako/987/987169286.html 49 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 07:41:10 ] なんでここの人たちって、延々言語の事話してるの? そんなもの自分で決められないんだから、そんな事話してる暇有ったら Lispでアプリケーションの一つでも書いたらどうなの? プログラミング言語なんで、ただの道具でしょ。 C言語に例えたら、延々ポインタの表記法の是非について語ってるみたいで キモイんだけれど。 50 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 07:45:08 ] キモければ来なければいい。 51 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 07:52:04 ] >>50 >キモければ来なければいい。 そんな排他的な事言ってるからいつまでたっても 広がらないんじゃないの? お前達は象牙の塔の住人なのか? このスレの中に一人でも「Lispを使ってこんな事が出来るんだ!」 と人を驚かすようなアプリケーション書いた奴いるの? グダグダ言語の事はなしてるより、アプリケーション書いた方が 万倍、計算機科学の発展に役立つと思うのだけれど。 グダグダ話してる内容も、外国の本の読み合いなんだしさ、意味ないよ。 52 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 07:54:13 ] それ以前に、何がどういう風にキモイのかが、その例ではわからないなぁ。 たぶん>>49は、「自分にとってキモイ」ということが、自分以外の人間にとっても通用する 普遍的で価値のあることで、だから詳細もすっ飛ばすし上から目線にもなってるんだろうけど、 それは自意識過剰ってもんでしょう。 「>>49にとってキモイ」という事実は、悪いけどゴミみたいな価値しかないことだから、 意味が無いし、もっとちゃんと話さないと通じないです。 53 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 07:56:36 ] >>51 じゃあまぁ、頑張ってアプリケーション書いてくれ。 他人に要求することや、他人をジャッジする内容を、まず自分に適用して生き続けるのが 厨と卒業する上で大事なことだから。 54 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 07:58:04 ] Lispで書くのって言語自身を拡張していく感じがあるから、Cなんかとは少し感覚が違うのかもしれん。 55 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:04:33 ] あらまぁ、あっというまの反論。 プログラマって人種はクリエイティブって言うし、 Lisp使う人は最高のプログラマって称号もあるけれどさ。 実際このスレ覗くと、延々使い古された古典の読み合いと紹介。 新規性の欠片もなくて、どこがクリエイティブなんだか。 56 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:05:14 ] こんな時にようかんマンが居ればなあ… 57 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:07:34 ] >>55 で、君どうしたいの？ そろそろ学校行ったら。 58 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:10:18 ] >>55 なんか君の言ってることの内容が、相手の対応によってどんどん変わってきてるな。 君の最初の疑問「なぜ延々言語の事話してるのか」の答は、ここが言語のことを話すスレであって、 ここで何かアプリケーションを作るスレではないからだよ。 あと、「そんな事話してる暇有ったらLispでアプリケーションの一つでも書いたらどうなの?」ってのは、 2chに書き込む行為を一切やめて、その時間をすべてプログラミングにあてろ、 そういう生活をしないならお前らはキモイ、という意味？ 59 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:13:41 ] 「クリエイティブ」と「新規性」も別に直結するものではないよなぁ。 なんか、切れ切れに言葉をしってるだけの二十歳くらいの坊やに思えてきた。 60 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:23:56 ] >「そんな事話してる暇有ったらLispでアプリケーションの一つでも書いたらどうなの?」ってのは、 >2chに書き込む行為を一切やめて、その時間をすべてプログラミングにあてろ、 >そういう生活をしないならお前らはキモイ、という意味？ 違うよ。 >このスレの中に一人でも「Lispを使ってこんな事が出来るんだ!」 >と人を驚かすようなアプリケーション書いた奴いるの? って事だよ。 Lispで今まで解けると思われていなかった問題を解けるようなアプリケーションを書けって事だよ。 それなのにお前らは、延々古典の読み合いばかり。 ガッカリだ。 とても新しい発想が生まれるとは思えない。 悔しかったら、「コレスゲー」ってもの出してみろ。 61 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 08:47:38 ] 「悔しかったら出してみろ」じゃ、誰も出さないと思うよ。 言ってることが間抜け過ぎて、誰も悔しくないだろうから・・・。 62 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 09:31:11 ] くやしい・・・ビクビク 63 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 10:58:30 ] > 64 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 10:59:58 ] ごめん、間違えてREPL > 65 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 11:19:18 ] 個人的には新しい発想といえば.NETだな .NETは言語じゃないけどな 言語じゃないというのが新しいよな つまり.NETでLispを使えということだな 66 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 11:27:25 ] > 延々古典の読み合いばかり ここはそういうところだから。 残念ながらLisp系でプロダクトコード書ける環境にいる人間は希少種だし。 というか他の言語スレも似たようなもんだが Lisper/Schemerにはなんか期待しちゃうところがあるんかな？ 67 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 11:31:36 ] 正直ここに身元がばれるようなことは書きにくいw ネタにされるだけだし 68 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 12:22:03 ] ここで煽る前に自分でやればぁw 自分が書いてるものの話なんかこんなところでできるかよ。 特定されたら面倒でかなわん。 69 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 16:22:20 ] そうだな。俺様のように社会的地位が高いと2chに来てるとバレるだけで恥だ。ｗ 70 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 17:13:01 ] >>69 竹内郁雄先生ですか？ 71 名前：竹内郁雄 mailto:sage [2008/01/15(火) 17:37:12 ] そうだよ。 良くわかったね。 実はtao/elisのソースを公開したいんだが、 電電公社が持っててね。 学術振興になると思うんだけれど、残念だ。 72 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 17:48:36 ] ポールグレアムからひとこと ↓ 73 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:01:42 ] SRFI-45:lazyの使いどころがいまいちよくわからない (delay (force ...))をforceすると末尾再帰でないforceの呼出しになって メモリを食いつぶすのを防ぐために使うのはわかったんだけど 末尾呼出しでない関数にlazyをつけると逆にメモリを食いつぶすようになる 末尾呼出しされるストリームを返す関数に使えばいいのかな 74 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:07:27 ] ｰ-ニ _　 ＿ヾV, --､丶､ し-､ ﾆ-‐'' ／／　ヾｿ　､　!ヽ　 `ヽ ヽ _／,.ｲ /　/ミ;j〃ﾞ〉 }�U ｝ ハ ヽ､} ..ノ /ﾊ　 〔　　 ∠ノ乂 ｛ヽ　ヾ丶ヽ　 　 ヽ　　　>>60 　ノﾉ　.>､_＼　{ j∠=, }、 l ＼ヽヽ ',　　_ノ ｰ-=ﾆ二ﾆ=一`'´__,.ｲ<::ヽリ　j　`､ ）　＼　　そもそも『悔しかったら、「コレスゲー」ってもの出してみろ』とは何なのか {¨丶､＿__,. イ　|{.　 |::::ヽ（　{　〈　（　 　　〉 '|　　| 　 　 　　小,　|:::::::|:::l＼i　',　ｌ　　 く　　君の意見を聞こうッ！ _| 　｜　 　　`ヾ:ﾌ　|::::::::|:::|　 }　}　|　　　） ､|　　| 　　 ∠ﾆﾆ}　|:::::::::|/　/　/ /　　／-‐-､ トl、　ｌ 　　{⌒ヽr{　|:::::::::|,／／／　　　　　　　 ＼／⌒＼/⌒丶/´￣` ::＼丶、 　 ヾ二ｿ　|:::::::/∠-''´ /＼＼.丶、 ｀''''''′!:::::::ﾚ〈 　　 〉::￣::｀'ｧ--‐''ﾞ:::::::/::::ヽ ＼;/:::::::::::::/::／::::::::::::/／:::::〉 ::`ヽ:::ｰ-〇'´::::::::::::::::/-ﾆ::::（ 　　　　　　　　　　　/　　　　＼ 75 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:24:58 ] ポールグレアム日本語達者だなぁ 76 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:29:04 ] arcのソースが公開されるって？ 77 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:31:27 ] いや、多分Lispで翻訳してるんだよ。 Emacsで2ch開くとAA以外は英語に翻訳され、 レスは自動で日本語になって書き込まれる。 ポールグレアムほどのｽﾊﾟｰﾊｶｰなら1秒以内にそのくらいは考えつくはず。 78 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:43:39 ] >>47 アラバマ物語もじってたのか。原題知らなかったｗ　「ものまね鳥を殺すには」が直訳かな。 ものまね鳥って「危害を加えない人」をたとえてるから、スマリヤンのタイトルでは「副作用のない演算」ぐらいの意味だろうか？ てことは「副作用のない演算に似たものを作るには」ぐらいの意味のタイトルみたいだ。「ものまね鳥をまねる」じゃ意味が伝わらないよなぁ。 役者も意味が取れていなかったのがいまさらながらわかった希ガス。 79 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:47:24 ] >>73 具体的にどういうコード? 80 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 18:50:30 ] 「副作用のない演算に似たものを作るには」の『副作用のない演算に似たもの』＝『コレスゲーってプログラム』と読み替えると、 スマリヤンの本が>>60への答えになってるなｗ 「ものまね鳥をまねる」　＝　「コレスゲーってプログラムを作るには」 81 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:03:21 ] こういう会話でまとめておこうｗ スマリヤン：「コレスゲーってプログラムを作るには？」 グレアム　：「Ｙコンビネータ・On・Lisp」 82 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:07:55 ] arcの言語仕様って公開されたの？ 83 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:13:35 ] >>81 "On Lisp"の内容、マクロが中心だたから、「コンビネータ使って副作用のないマクロを書け。そうすれば『コレスゲープログラム』が作れるぞ！」って意味なのねん？ 84 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:17:28 ] >>80 どうだろう。彼が要求しているのは 「今まで解けると思われていなかった問題を解けるような"アプリケーション"」 だからなぁ。 それってつまり、チューリング等価を越えろっていう要求ではないかと思うんだ。 彼は言語のパワーというものが、あるものを「どう」実現できるかという"how"の領分の話だということが まるで理解できていないんでは？ 「Lispが凄いのなら、Lispで書いたプログラムにしか為し得ない動作があるのだろう」 という発想でモノを言ってるように窺える。てかそもそも「アプリケーション」って言い方が猛烈に素人臭いしｗ 85 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:21:43 ] >>79 ;(define (stream-cdr stream) ; (srfi-45:lazy (cdr (srfi-45:force stream)))) これはプロミスを受け取ってプロミスを返す関数だからlazyをつけたいとこだけど ;(define (stream-tail stream k) ; (srfi-45:lazy ; (if (zero? k) ; stream ; (stream-tail (stream-cdr stream) (- k 1))))) とかで末尾呼出しされない場合メモリを食いつぶす 86 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:27:11 ] >>84 プログラミング言語なんて所詮は「λ算法＝チューリングマシン」の糖衣構文に過ぎないからねぇ。 スマリヤンの本の趣旨は「コレスゲーってプログラムをつくるには（ゲーデルのいうように限界があるのだよ）」ということだからねぇ。 87 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:39:14 ] (delay (force ...))とかしなくても call/ccでdelayを包めばいいじゃん とか思ったりもしたけど 遅延される計算量がエラいことになって使い物にならないことに 実行するまで気づかなかった('A`) というか実行しても暫く気づかなかったorz 88 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:40:05 ] >>85 forceはどこいった? 89 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:41:51 ] これテンプレに入れようよｗ www.asahi-net.or.jp/%7Eki4s-nkmr/lisp20061121/lisp.html 90 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:41:59 ] >>88 stream-tailがプロミスを返すので (srfi-45:force (stream-tail s 10))とかするつもり 91 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 19:52:19 ] >>90 srfi-45のルール通りにやれ 92 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 20:03:54 ] >>91 どこらへんがルールと違う？ * wrap all constructors (e.g., '(), cons) with delay, * apply force to arguments of deconstructors (e.g., car, cdr and null?), * wrap procedure bodies with (lazy ...). は守ってるつもりだけど 93 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 20:06:30 ] >>89 朝日ネットのURLは /~KI4S-NKMR/ こう書くほうが好みだな 94 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 20:33:04 ] >>83-84,>>86 ループまたは再帰のあるチューリング完全なプログラミング言語は等価であるということですか。やっとわかりました。（汗 等価であるなら個別の問題に対して実装しやすい言語を使えば良いということですよね。 でLisp/Schemeの場合、マクロで拡張してその問題に特化したDSLを作成して実装したらいいというのがグレアムのスタンス。 >>54が言ってた言語の拡張性がこの言語のユーザーの強みといえるかな。SLLGENとかもソレ系ですし。 95 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 20:58:31 ] >>83-84,>>86,>>94 そういう流れのLisp本、チャイティン著「知の限界」「数学の限界」という本がありますよ。 Lisp使ってゲーデルの不完全性定理やチューリングの停止問題を説明してます。 96 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 21:09:22 ] ググってたらゲーデルもLisperだったって書いてあった。 97 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 21:16:06 ] >>93 うるさいことを言うと、URLの中の ~ はエスケープしなければいけないという「規格」になっておる。 98 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 21:17:44 ] 87は計算量以外に初歩的かつ致命的な欠点があった 忘れてくださいorz 99 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 21:27:29 ] Sho"nfinkel Rules!!! 100 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 21:50:27 ] >>96 ホフスタッターの本にそんなのあったね。 あった！「メタ、マジックゲーム」ｐ４４５ 「ゲーデルはリスプ(Lisp）を思いついておくべきだった。 もし彼がリスプを思いついていたならば．．．」 101 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 22:12:48 ] >>97 > >>93 > うるさいことを言うと、URLの中の ~ はエスケープしなければいけないという「規格」になっておる。 RFC 1738 ではそうですね。 URI (RFC 2396) ではおkです。 102 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 22:14:20 ] みんな学があるなあ 103 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 22:47:42 ] 学々古々 104 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:01:11 ] >>95 「知の限界」読み直してみようと思う。ｐ７１のLISPによるゲーデルの証明、 これSchemeで書きなおせるかやってみる。 チャイティンの書いたLispインタープリタってネットで公開されていたような... 105 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:02:24 ] lex/yacc&flex/bisonでパーサー作るより>>94みたくDSLで拡張すれば、既存のLisp/Schemeのプログラムとくっ付けることでいとも簡単に新しい処理系が出来てしまうのか。 しかもPrologとかAIを組み合わせればちょっと他の処理系では作りにくいものも作れてしまうのか。ガンダムの教育型ＯＳってこんなイメージかなｗ がんばってLittle Schemerシリーズ読んでみようかな。Ocaml/Haskellはかじったけどこっちの方が面白杉。 106 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:05:54 ] >>104 あれ、emacsやxyzzyでも動くのかな？Scheme版出来たらうｐｷﾎﾞﾝﾇ 107 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:10:14 ] >>95,>>100,>>104達、すごい本読んでるね。 108 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:13:16 ] >>103 そんなｵﾏｴにｶﾞｸｶﾞｸﾌﾞﾙﾌﾞﾙｗ 109 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:18:14 ] 「げー出る、エッシャー、バッハ」と「メタマジック・ゲーム」は俺も本棚に飾ってあるぜー！ 前者は箱入りなのに後者は箱がなくて悲しいぜ。 110 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:19:24 ] このスレで紹介された本 [1] Little Schemer [2] Seasoned Schemer [3] Reasoned Schemer [4] To Mock a Mockingbird（ものまね鳥をまねる） [5] To kill a mocking bird（アラバマ物語） [6] On Lisp [7] 知の限界 [8] 数学の限界 [9] メタ、マジックゲーム [10] SICP 111 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:20:26 ] [11] ｹﾞｰﾃﾞﾙ・ｴｯｼｬｰ・ﾊﾞｯﾊ 112 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:27:42 ] 前ｽﾚからだけどこれもあった。2月が楽しみ。ｗｋｔｋ [12] 「プログラミングGauche」 川合史朗　監修 Kahuaプロジェクト　著 113 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:40:25 ] >>45 Ｙコンビネータまで８羽理解すればいいのか。今、気がついたｗ Ｓ　（ムクドリ：Starling） Ｋ　（チョウゲンボウ：Kestrel） Ｉ　（？？？：Identity bird）＝ＳＫＫ Ｂ　（？？？：Blue bird）＝Ｓ（ＫＳ）Ｋ C　（コウカンチョウ：Cardinal）＝Ｓ（ＢＢＳ）（ＫＫ） Ｍ　（ものまね鳥：Mocking bird）＝SII Ｌ　（ヒバリ：Lark）＝ＣＢＭ Ｙ　（賢人鳥：Why bird）＝ＳＬＬ 114 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:50:00 ] >>113 ホレ。 (define S (lambda (f) (lambda (g) (lambda (x) ((f x) (g x)))))) (define K (lambda (x) (lambda (y) x))) (define I (lambda (x) x)) (define-macro (define-combinator name body) `(define ,name (lambda (arg) (,body arg)))) (define define-combinator define) (define-combinator B ((S (K S)) K)) (define-combinator C ((S((S(K((S(K S))K)))S))(K K))) (define-combinator M ((S I) I)) (define-combinator L ((C B) M)) (define Y (lambda (F) ((lambda (my-make-f) (F (lambda (x) ((my-make-f my-make-f) x)))) (lambda (my-make-f) (F (lambda (x) ((my-make-f my-make-f) x))))))) 115 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:52:45 ] (define (Fact my-fact) (lambda (n) (if (= n 0) 1 (* n (my-fact (- n 1)))))) (define fact (Y Fact)) (fact 10) 3628800 116 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:53:43 ] (define (Fib my-fib) (lambda (n) (if (<= n 1) 1 (+ (my-fib (- n 1)) (my-fib (- n 2)))))) (define fib (Y Fib)) (fib 10) 89 117 名前：デフォルトの名無しさん mailto:sage [2008/01/15(火) 23:55:09 ] これでもいいﾊｽﾞだけどｗ (define-combinator Y ((S L) L)) 118 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 00:00:31 ] >>110 > [9] メタ、マジックゲーム 超なつかしい 高校の夏休みにY.M.O.ベストと一緒に図書館で借りて読んだのをおぼえてる。 いま思うと充実してたなあの頃は。 119 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 00:02:22 ] 　　　　　　　　 ,. -‐'''''""¨¨¨ヽ　　　それじゃあ僭越ながら 　　　　 　 　 (.＿＿_,,,... -ｧァﾌ|　　　あ…ありのまま 今　起こった事を話すぜ！ 　 　 　 　 　 |i i|　 　 }!　}} /／| 　　　　 　 　 |l､{　 　j}　/,,ｨ//｜　　　　『おれは階乗計算のために無名関数をいじっていたと 　　　　　　　 i|:!ヾ､_ﾉ／ u {:}//ﾍ　　　　　思ったらいつのまにかいじる前の状態に戻っていた』 　　　　　　　 |ﾘ u' }　 ,ﾉ　_,!V,ﾊ | 　　 　 　 ／´fト､_{ﾙ{,ィ'ｅﾗ　, ﾀ人　　　　　　な…　何を言ってるのか　わからねーと思うが 　　　　 /' 　 ヾ|宀| {´,)⌒`/ |<ヽﾄiゝ　　　　　おれも何をされたのかわからなかった… 　　　　,ﾞ　 ／ )ヽ iLﾚ 　u' |　| ヾｌﾄﾊ〉 　　 　 |／_／　 ﾊ !ニ⊇　'／:} 　V:::::ヽ　　　　　　頭がどうにかなりそうだった… 　　　 /／ 二二二7'T'' ／u'　__ /:::::::/｀ヽ 　　　/'´r　ー---ｧ‐ﾞＴ´　'"´ ／::::／-‐ 　＼　　　　グラハムだとかチャイティンだとか 　　 / // 　 广¨´ 　/'　　 ／:::::／´￣｀ヽ ⌒ヽ　　　　そんな大層なもんじゃあ　断じてねえ 　　ﾉ ' /　 ノ:::::`ー-､___／:::::／/ 　 　 　 ヽ　　} _／｀丶　/::::::::::::::::::::::::::￣`ー-{:::...　　　 　　　ｲ　　　 もっと恐ろしい「普通の再帰」と「Ｙコンビネータ」の違いを味わったぜ… 120 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 02:29:41 ] とりあえず、グレアムな 121 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 06:00:52 ] >>114 「計算論」（高橋正子著）を読み始めていたので参考になった。 ありがとう。 122 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 11:45:06 ] 急に難しい話題が増えたね 俺はバカだから、理由もなく難しいことを考えるのは非合理的だと思うけど 君らにとっては難しくなくて、難しくないことを考えるのに理由は要らない なんというかバカの壁を実感したよ 123 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 12:26:41 ] バカであることに気がついてる奴は大したバカではないよ 124 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 14:35:15 ] じゃあ俺も壁感じたから大した馬鹿じゃないな＼(^o^)／ﾖｶﾀｰ ところで、新宿ジュンク堂にならLittle schemerあるかもと思ったけど無かった。 MITの本はいくつかあったけど。 注文したらアマゾンの方が早いかな。 125 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 18:06:49 ] >>113-114 チラ見だけど、SKKとかSIIとかSLLとかがやたら目に付いた。なんか深遠なパターンがあるんだろうな。 126 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 18:14:00 ] >>80-86 その「コレスゲープログラム」はunlambdaのことｼﾞｬﾏｲｶ？ 難読化してもちゃんと動くぜってノリだった希ガス。 127 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 19:39:36 ] ポルナレフに突っ込み入れる>>120はアブドゥルなのか？ｗ 128 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 19:53:02 ] >>126 ﾁｬｳﾁｬｳ。このｽﾚの流れで言ってるコレスゲープログラムは定理証明機としての意味。だから>>95,>>104の話が出てきた。 >>100の紹介した本が言ってるのは「ｹﾞｰﾃﾞﾙがもっと便利な定理証明機（Lisp）を思いついていれば」という意味だ。 つまりスマリヤンが言ってるコレスゲープログラムとはスゲー定理ということ。 129 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 19:54:52 ] コレスゲープログラム　＝　スゲー定理　＝　ゲーデルの不完全性定理 130 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 19:59:59 ] つまり>>60はスマリヤンやチャイティン嫁ってことかｗ 131 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 20:19:26 ] タオイズムか！ 132 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 20:55:13 ] 「ものまね鳥をまねる」って「定理証明機＝ラムダ算法＝結合子論理＝プログラミング言語」って意味だったのか。マジで知らなかった（汗 このスレ勉強になるな。 133 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 21:05:52 ] >>126 UnlambdaやBrainf*ckの意味ではなく、CoqやIsabella等の定理証明機が正解かな常考。 134 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 21:13:32 ] >>124 まちがいない。 135 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 21:27:01 ] >>86と>>132をみてチューリングマシーンが定理証明機だということに初めて気がついた。そういうことだったのか。 136 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 21:34:08 ] なら>>60が求めてるのは「公理データベースによって結果が異なる自動定理証明機」というところか？ 137 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 23:00:18 ] >>135 チューリングマシーンがハードウェア型の定理証明機とするならラムダ算法とか結合子論理はソフトウェア型の定理証明機になってるよね。 でも>>100にあるようにもしもゲーデルがLispのようなプログラミング言語を知っていれば、ゲーデルの証明はもっと理解しやすかったのにということだよ。 つまり、たとえ等価でももっと分かり易くできるプログラミング言語があるならそれを使うべきだというのが結論じゃないかな。 教養として難しいことも知っておくのも意義はあるけどね。UnlambdaやBrainf*ckもそういう意味でしかないと思う。 138 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 23:13:01 ] 自力では歯が立たなかったので下記を参考にやってみた。 ttp://www.unfindable.net/~yabuki/article/unknowable/godel.html ;;不動点 (define (f x) `(',x ',x)) > (f 'x) ((quote x) (quote x)) > (f f) ((quote #<procedure:f>) (quote #<procedure:f>)) > (equal? (f f) (eval (f f))) #t > (equal? (f f) (eval (eval (eval (eval (eval (f f))))))) #t > 続く 139 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 23:14:00 ] ;;チャイティン　Lispによるゲーデルの証明 ;;(valid-proof? x) の定義があると仮定する。ｘが妥当な証明なら'() ;;xが妥当な証明なら実証された定理を返す。 ;;ｓ式ｙが証明できない⇔すべてのｓ式ｘについて (valid-proof? x)が ;;ｙと等価とは限らない。 ;;これを肯定する述語が (is-unprovable y) (define (g x) `(is-unprovable (value-of (',x ',x)))) > (g 'x) (is-unprovable (value-of ((quote x) (quote x)))) > (g g) (is-unprovable (value-of ((quote #<procedure:g>) (quote #<procedure:g>)))) > (equal? (g g) (eval (cadr (cadr (g g))))) #t > 証明できないということは証明できない　＝　（証明できないということは証明できない）ということは証明できない。 こういう意味なのだろうか？頭が痛くなりそうだ。 140 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 23:32:34 ] 訂正 誤　;;(valid-proof? x) の定義があると仮定する。ｘが妥当な証明なら'() 正　;;(valid-proof? x) の定義があると仮定する。ｘが妥当な証明でないなら'() 141 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 23:37:03 ] >>139 その入れ子になっている計算が無限に続いた入れ子と仮定して、その計算はいつか止まるのかという意味になっている。 それがチューリングの停止性問題だ。1931年にゲーデルがやったことを1937年にチューリングがチューリングマシンで説明した問題。 それをチャイティンはLispで書いてみたってこと。チューリングの停止性問題でｸﾞｸﾞﾚばわかりやすい説明が見つかるだろう。 （チャイティンにケチをつけるわけじゃないが、無限のメモリがないと同じことにはならない） 142 名前：デフォルトの名無しさん mailto:sage [2008/01/16(水) 23:50:09 ] >>140 Little Schemerの９章に出てくるＹコンビネータも無限に続いた入れ子（＝再帰関数）を作るためだよね。 >>114-119のＹコンビネータがそれに相当するかな。 143 名前：138 mailto:sage [2008/01/16(水) 23:58:33 ] >>141 >>142 なるほど〜。勉強になりました。 144 名前：デフォルトの名無しさん mailto:sage [2008/01/17(木) 00:06:45 ] 無限ループは止まらないだろ常考。ということは、「証明できないということは証明できないということは・・・」の答えが返ってこないから証明できないわけ。 145 名前：デフォルトの名無しさん mailto:sage [2008/01/17(木) 00:08:35 ] >>143 おぉ、理解早いね。 146 名前：デフォルトの名無しさん mailto:sage [2008/01/17(木) 00:20:21 ] >>144 ゲーデルとチューリングって無限ループは止まらないってことを言ってるのか。なんか意外だなぁ。 147 名前：デフォルトの名無しさん mailto:sage [2008/01/17(木) 00:23:36 ] ・止まる無限ループが存在すると仮定する ・矛盾する ・従ってすべての無限ループは止まらない ・証明終わり 148 名前：デフォルトの名無しさん mailto:sage [2008/01/17(木) 00:25:33 ] >>146 無限という概念は数学的には不可解なのです。 149 名前：デフォルトの名無しさん mailto:sage [2008/01/17(木) 00:33:04 ] ループや再帰を持つものはチューリング完全である。 ↓ 無限のループや再帰は止まらないことがある。 ↓ 判定不能な問題が存在する。 ↓ チューリング完全なプログラミング言語は万能ではない！ ↓ プログラマーに出来ることには限界がある。 ↓ バカの壁（Q.E.D.）

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef