1 名前:デフォルトの名無しさん mailto:sage [2009/04/24(金) 19:12:39 ] ※ ここはCommon Lisp、SchemeをはじめとするLisp族全般のスレです ※ ■過去スレ Part25: ttp://pc12.2ch.net/test/read.cgi/tech/1231856193/ Part24: ttp://pc11.2ch.net/test/read.cgi/tech/1224939205/ Part23: ttp://pc11.2ch.net/test/read.cgi/tech/1215875388/ Part22: ttp://pc11.2ch.net/test/read.cgi/tech/1211381920/ Part21: ttp://pc11.2ch.net/test/read.cgi/tech/1207300697/ Part20: ttp://pc11.2ch.net/test/read.cgi/tech/1205021786/ Part19: ttp://pc11.2ch.net/test/read.cgi/tech/1200237296/ 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://pc11.2ch.net/test/read.cgi/tech/1151025773/ Part14: ttp://pc11.2ch.net/test/read.cgi/tech/1132275726/ Part13: ttp://pc11.2ch.net/test/read.cgi/tech/1115901841/ Part12: ttp://pc11.2ch.net/test/read.cgi/tech/1100229366/ Part11: ttp://pc11.2ch.net/test/read.cgi/tech/1091456033/ Part10: ttp://pc11.2ch.net/test/read.cgi/tech/1075630259/ Part09: ttp://pc11.2ch.net/test/read.cgi/tech/1069594582/ Part08: ttp://pc5.2ch.net/tech/kako/1058/10582/1058263391.html Part07: ttp://pc5.2ch.net/tech/kako/1042/10421/1042167213.html Part06: ttp://pc3.2ch.net/tech/kako/1031/10315/1031560687.html Part05: ttp://pc3.2ch.net/tech/kako/1023/10230/1023091882.html Part04: ttp://pc.2ch.net/tech/kako/1016/10162/1016211619.html Part03: ttp://pc.2ch.net/tech/kako/1008/10082/1008220265.html Part02: ttp://pc.2ch.net/tech/kako/1002/10025/1002584344.html Part01: ttp://piza2.2ch.net/tech/kako/987/987169286.html ■テンプレート置き場 ttp://wiki.fdiary.net/lisp/ (id:guest pass:cl)
730 名前:デフォルトの名無しさん mailto:sage [2009/07/06(月) 20:59:14 ] 2000年問題、文字コード、IP枯渇・・・
731 名前:デフォルトの名無しさん mailto:sage [2009/07/06(月) 21:38:55 ] >>727 チャーチ=チューリングのテーゼによれば、アルゴリズムのある関数は全て計算可能である。 つまり、アルゴリズムを学ぶことが計算可能関数を学ぶことに相当している。 そしてアルゴリズムを学ぶ際にはSchemeが理解の助けになる。 簡単にまとめると、「Yコンビネータがあるチューリング完全な言語ではアルゴリズムのある関数は全て計算可能である」ということになる。 あたりまえの事だけど、数学的に保証してくれてるので安心してプログラミングして計算ができるわけだ。
732 名前:デフォルトの名無しさん mailto:sage [2009/07/06(月) 23:58:44 ] Yコンビネータの話とλ計算の話をごっちゃにしてはいけない。 コンビネータの話とλ計算の話はもともと別の話。それが途中で コンビネータの理論はλ計算の理論に翻訳可能だとわかったので、 同時に語られることが多いというだけ。 コンビネータ理論の歴史は古くて1920年代にSchonfinkelと言う人が始めて Curry(カリー化のカリー)が発展させた。
733 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 00:18:57 ] Yコンビネータに関する疑問について言えば、Yコンビネータの存在意義という のは、確か再帰の概念が存在しない言語において再帰と同等の物を導入するため、 だったと思う。
734 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 00:50:34 ] そういえば、ものまね鳥、あれからすぐに図書館に 返したんだけど。借りられたかな。
735 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 01:25:05 ] ここで>>368 のリンク先にあるラムダ式を簡約するArcのプログラムを読むと感動すること請け合いである。
736 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 07:39:45 ] >>713 詳しいことはドキュメントに書いてあるよ
737 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 11:14:49 ] まだ実験的なものかと思ってたのでドキュメント見てなかった でも、英語の説明しかねーや。 読むのめんどい。 ところで、 sparse って名前だと sparse な何かわからんので、 モジュール名はあんまりよくないと思った。 Scheme 処理系に入ってたら、 S式をパースするものっぽい気もしてしまう…
738 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 11:28:27 ] 保守的GCと心中する気がなければ、ただの一時しのぎだろ
739 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 20:07:45 ] >>737 > Scheme 処理系に入ってたら、 S式をパースするものっぽい気もしてしまう… その発想は鳴かった
740 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 23:26:48 ] >>731 計算可能な関数には3つの系譜があるようだ。 ○ゲーデル〜クリーニ 一般帰納的関数 ○チャーチ λ−定義可能な関数 ○チューリング チューリングマシンで実行できる関数 ゲーデルの流れだと原始帰納的関数は計算可能関数。 Lispの本の例題に登場するアッカーマン関数は原始帰納的関数ではないのだけど 帰納的関数であり計算可能関数らしい。階乗計算とかフィボナッチ数とかは 原始帰納的関数なんだと思う。詳しい方、間違ってたら補正してください。
741 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 23:49:28 ] >>740 チューリングマシンと等価なのは部分再帰関数であって、原始再帰関数は 部分再帰関数の部分集合に過ぎない。
742 名前:デフォルトの名無しさん mailto:sage [2009/07/07(火) 23:54:14 ] >>740 あんまりわかんないなら,書き込まなくていいと思う.
743 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 00:23:08 ] ボイスコッド正規形ならクリーニアンクロージャ作れるからラムディ
744 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 00:46:46 ] 帰納的定義のackermann functionってこんな感じ? (define (iter f n) (if (= n 0) (f 1) (f (iter f (- n 1))))) (define (ack n) (if (= n 0) (lambda (m) (+ m 1)) (lambda (m) (iter (ack (- n 1)) m)))) (display ((ack 3) 5)) ;; nice curried...
745 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 08:32:21 ] >>741 740ではないが, 原始帰納関数 ⊆ 部分再帰関数 ⊆ 一般帰納関数 ということになるってこと? 部分再帰関数と一般帰納関数の違いって何?
746 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 09:48:29 ] function = partial function∪total function
747 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 09:58:51 ] >>745 一般再帰(帰納的)関数の定義は?Kleeneの言うgeneral recursive function の意味で言っているのなら、部分再帰関数の真部分集合。なぜなら部分再帰関数は 全域関数でもありうるから。 つまり、 原始再帰関数 c 一般再帰関数 c 部分再帰関数 ということ。ちなみに、原始再帰関数も真部分集合だぞ。Ackermann関数がその一例。 つーかおまい情報系出身か?この辺は一般常識だぞ。 門外漢なら計算理論の教科書を読むべき。
748 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 10:11:31 ] >>746 partial function ⊃ total function
749 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 13:01:30 ] オレ、門外漢なんで高橋先生の「計算論」を読んでみた。 関数と部分関数ってのがあるんだね。そこを強調するのに 部分帰納的関数という言い方をするんだそうだ。 一般帰納的関数はゲーデルの本にあった言い方で クリーニの1936年の論文らしい。邦訳があったら読んでみたい。
750 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 15:57:45 ] →ゲーデルのセミナーでの言い方 ゲーデルは共同研究やセミナーで使っただけで、 帰納的関数について長らく公表しなかった。 ゲーデルにとっては公表するほどの成果ではなかったらしい。
751 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 16:26:45 ] ゲーデルは算定可能という概念も提案した。 結局、これら6つの同等性が証明されてチャーチの提唱へ。
752 名前:baka mailto:sage [2009/07/08(水) 17:40:48 ] すいません、LittleSchemerが難しいと感じるのってやばいですか? いま2章のand again, and again...のとこなんですが意味わかめです。
753 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 18:17:37 ] どこがわからないんですか?
754 名前:baka mailto:sage [2009/07/08(水) 18:59:32 ] >>753 すいみません自己解決しました。 >What is the meaning og the line >((null? l) #t) を(#f #t) と勘違いしてました。 先に出てるdefine lat中の文章のことなんですね。もっとしっかりと読まねば。
755 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 19:11:45 ] しっかりしろバカ
756 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 21:27:55 ] 再帰関数(帰納的関数)は数学的に扱いやすい良い性質があるようですが、 なぜ関数プログラミングが世の中の主流になれないのですか?
757 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 21:29:43 ] >>747 情報出身じゃないっす。興味あるだけの人。 そうか一般再帰関数って最小解操作を許す全域関数(total function)の ことだったのか。
758 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 21:33:58 ] >>756 世の中の現象を反映させるにはオブジェクト(対象)指向じゃないとだめだろ 世の中にあるのは対象なのだから。 んでもって、対象間の関係が数学である。 オブジェクト指向開発されたシステムの真に理想的な姿というか関係が ”数学”になる、んだろ。 関数だけ持ってきても対象が無い(というか対象とは?と言う話になる) からどうしようもないとかそういう話じゃない?よく知らんが。
759 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 22:17:21 ] >>758 アフォ
760 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 22:41:17 ] >>758 ほんとに知らなすぎでワロタ
761 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 22:49:49 ] いえいえ。
762 名前:デフォルトの名無しさん mailto:sage [2009/07/08(水) 23:00:31 ] “不運”(ハードラック)と“踊”(ダンス)っちまったんだよ に似てる
763 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 01:43:38 ] schemeってすばらしいですねぜひきわめたい。
764 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 01:50:35 ] 頑張れ Lisp/Schemeは面白いぞ
765 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 04:37:15 ] リリカルlisp ベルカ式はパターンマッチを主体としている
766 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 15:04:18 ] ΣxΣyf(x,y)な計算をSchemeで処理するはどう書けばいいんでしょうか。 Rubyで書くとこんな感じなんですが… v = 0.0 (0..10).to_a.each do |x| (0..10).to_a.each do |y| v += f(x, y) end end
767 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 15:23:06 ] 色々あると思うけど例えば (dotimes (i 10) (dotimes (j 10) (set! v (f i j))))
768 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 15:25:47 ] SRFI-42で (sum-ec (: x 11) (: y 11) (f x y))
769 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 17:02:45 ] (fold (lambda (n i) (+ i (f (car n) (cdr n)))) 0 (map (lambda (x) (map (lambda (y) (cons x y) ) (iota 11)) ) (iota 11)) ) unko
770 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 17:13:02 ] これぐらいならやはりlist comprehensionが一番かな
771 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 17:20:17 ] List comp(ryはlexical syntaxで読みやすさを獲得するから、 あまりLisp向きじゃないね。 blog.superadditive.com/2007/11/09/list-comprehensions-in-common-lisp/
772 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 19:52:27 ] 素直に再帰で考えてみたけど (define (sum1 n m f) (if (= m 1) (f n m) (+ (f n m) (sum1 n (- m 1) f)))) (define (sum n m f) (if (= n 1) (sum1 n m f) (+ (sum1 n m f) (sum (- n 1) m f))))
773 名前:デフォルトの名無しさん mailto:sage [2009/07/09(木) 22:39:10 ] 竹内関数って原始帰納的関数なのですか? それともアッカーマン関数のように原始帰納的関数ではない帰納的関数なのでしょうか? (define (tak x y z) (if (> x y) (tak (tak (- x 1) y z) (tak (- y 1) z x) (tak (- z 1) x y)) y))
774 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 09:42:18 ] >>773 再帰関数ではあるが、原始再帰関数ではない。
775 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 16:26:55 ] >>774 ありがとうございました。 区別がわかってきました。
776 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 17:24:17 ] set! による破壊的代入がなければ絶対に書けないプログラムって どういう種類のものですか?
777 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 17:26:59 ] 無限リストとかじゃね
778 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 18:11:07 ] クリンゴン、エンタープライズの位置座標 フェイザー砲の残りエネルギー、ダメージ
779 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 20:56:17 ] lispでStar Trekか www.xn--t8jcq9c.jp/~take/trek/trek-manj.html
780 名前:デフォルトの名無しさん mailto:sage [2009/07/10(金) 21:51:43 ] >>779 あるんだねぇ。GCLで動いたよ。 あっけなくやられてしまった。
781 名前:デフォルトの名無しさん mailto:sage [2009/07/11(土) 16:46:50 ] さっき知ったんだが schemeのcondって継続渡しみたいな構文をサポートしているんだな (cond ((or #f '(1 2 3)) => cdr))
782 名前:デフォルトの名無しさん mailto:sage [2009/07/11(土) 23:04:55 ] 今日ずっと考えてるんですが解けないので もしわかる人いたら教えてください (cata n)で、n個の要素の括弧の付け替えからなる リストを生成する関数を作ろうとしてます 規則がよくわからなくてどうもうまくいきません 例えば (cata '(1 2)) ((1 2)) (cata '(1 2 3)) (((1 2) 3) (1 (2 3))) (cata '(1 2 3 4)) ((1 (2 (3 4))) (1 ((2 3) 4))) ((1 2) (3 4)) ((1 (2 3)) 4) (((1 2) 3) 4)) 要素数はカタラン数になるそうです (define (cataran n) (define (nck n k) (cond ((or (= k 0) (= n k)) 1) (else (+ (nck (- n 1) k) (nck (- n 1) (- k 1)))))) (/ (nck (+ n n) n) (+ n 1)))
783 名前:デフォルトの名無しさん mailto:sage [2009/07/11(土) 23:18:25 ] >n個の要素の括弧の付け替えからなるリスト もうちょっと厳密に
784 名前:デフォルトの名無しさん mailto:sage [2009/07/11(土) 23:48:43 ] >>783 わかりにくくてすみません 言い換えると 一度に2つの要素の足し算しかできない+を使って n個の要素を全て足すとしたときの 可能な計算の順序の指定の仕方と同じです 1+2+3は(1+2)+3と1+(2+3)の計算法があります これは(cata '(1 2 3))に対しての ((1 2) 3) (1 (2 3)) に相当します
785 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 00:01:04 ] ・二分木である ・葉にしか要素がない (>>784 で言えば数) ・分岐には要素がない (>>784 で言えば+) という場合、要素数がn個なら木の種類は? と同じ問題。 ・要素の間の何処に分岐点を持ってくるかの数え上げ ・二つの部分木に分けた後の分割統治 を考えればわかるでしょ。
786 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 01:16:07 ] 規則とかいってるからサンプル眺めるだけでえいやっと思い付こうとしてるのかな。 n=1からn=4, 5くらいまで自分で書き出してみれば考え方もわかりそうなものだが。
787 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 07:18:12 ] >>785 出来ました。ありがとうございます (define (cata l) (define (flat1 x) (fold append () x)) (define (aux n l) (map (lambda (x) (map (lambda (y) (if (and (pair? x) (null? (cdr x))) (cons (car x) y) (cons x y))) (cata (drop l n)))) (cata (take l n)))) (define (aux2 n l) (if (<= n 0) () (append (flat1 (aux n l)) (aux2 (- n 1) l)))) (if (< (length l) 3) (list l) (aux2 (- (length l) 1) l)))
788 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 08:28:51 ] ()を評価したら()でええの? エラーではないの?
789 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 09:08:13 ] 規定ではエラーだねぇ
790 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 09:11:14 ] >>787 (cata '(1 2 3 4)) の実行結果が、最初に書いてあった実行例と違うんですが (cata '(1 2 3 4)) (((1 2 3) 4) (((1 2) 3) 4) ((1 2) 3 4) (1 (2 3) 4) (1 2 3 4))
791 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 10:40:02 ] >>788 '()のがいいですね。Gaucheだとエラーにならないので 他の処理系使うまで気づきませんでした >>790 (1 2 3)を(1 . (2 3))のように見たら >>784 を満たしているので 中途半端ですが満足してしまいました 多分ちょっといじればその出力に出来ると思います
792 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 11:01:56 ] >>791 自分も考えてみたけどけっこう難しい例題だと思うよ。 根本的に書き直さないといけないんじゃない?悪いけど。
793 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 11:21:17 ] そんなことない、ちょっと書き直したら動きましたよ >>792 さんも考えてるかもしれないのでヒントだけ ネストしたmapの中身を修正するだけです
794 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 11:28:04 ] ちなみに srfi-42 使えばこんなに簡単 (define (cata l) (if (< (length l) 2) l (list-ec (: pos 1 (length l)) (: fst (cata (take l pos))) (: snd (cata (drop l pos))) (list fst snd))))
795 名前:785 mailto:sage [2009/07/12(日) 11:34:56 ] 実はドット対で二分木を構成した方が分かりやすい とアドバイスを入れるかどうか迷った。 結局元の問題と違っちゃうから書かなかったけど。
796 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 11:42:04 ] (define (cata xs) (cond ((null? xs) '()) ((null? (cdr xs)) (list (list (car xs)))) ((null? (cddr xs)) (list (list (car xs) (cadr xs)))) (#t (let ((a (car xs)) (b (cadr xs)) (rest (cata (cddr xs)))) (define (patr x) (list a (list b x))) (define (patl x) (list (list a b) x)) (append (map patr rest) (map patl rest)))))) うんこーどですが、どうでしょうか
797 名前:796 mailto:sage [2009/07/12(日) 11:43:40 ] 駄目ですた
798 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 11:50:51 ] >>794 これは神コード・・srfi-42かぁ
799 名前:792 mailto:sage [2009/07/12(日) 17:53:13 ] >>793 やっぱ、難しい。考えて相互再帰のこんなの↓考えた。 fooの部分はそれぞれのリストの直積みたいにすれば いいと思うのだけど、どうもうまくいかない。 また、考えてみるよ。 (define (cata ls) (if (<= (length ls) 1) ls (cata1 ls 1))) (define (cata1 ls i) (if (= i (length ls)) '() (cons (foo (cata (take ls i)) (cata (drop ls i))) (cata1 ls (+ i 1)))))
800 名前:792 mailto:sage [2009/07/12(日) 19:37:44 ] やっとできた。勉強になった。 (define (cata ls) (if (<= (length ls) 1) ls (cata1 ls 1))) (define (cata1 ls i) (if (= i (- (length ls) 1)) (product (cata (take ls i)) (cata (drop ls i))) (append (product (cata (take ls i)) (cata (drop ls i))) (cata1 ls (+ i 1))))) (define (product ls1 ls2) (if (null? ls1) '() (append (map (lambda (x) (cons (car ls1) (list x))) ls2) (product (cdr ls1) ls2)))) > (cata '(1 2 3 4)) ((1 (2 (3 4))) (1 ((2 3) 4)) ((1 2) (3 4)) ((1 (2 3)) 4) (((1 2) 3) 4)) >
801 名前:デフォルトの名無しさん mailto:sage [2009/07/12(日) 20:35:35 ] >>800 おめでとん 自分の環境では、 3つのコード中>>800 が最速でした 参考までに >>787 の修正版も張っておきます (define (cata l) (define (flat1 x) (fold append '() x)) (define (single? x) (and (pair? x) (null? (cdr x)))) (define (aux n l) (map (lambda (x) (map (lambda (y) (cons (if (single? x) (car x) x) (if (single? y) y (list y)))) (cata (drop l n)))) (cata (take l n)))) (define (aux2 n l) (if (<= n 0) '() (append (flat1 (aux n l)) (aux2 (- n 1) l)))) (if (< (length l) 3) (list l) (aux2 (- (length l) 1) l)))
802 名前:デフォルトの名無しさん [2009/07/13(月) 11:09:33 ] >>758 すまん、まじめに反応してみるが、 それは命題論理->一階述語論理の流れでは歴史的事実だが、 そこでの対象指向自体は、関数プログラミングとOOプログラミング を篩にかけるものではない。FOLレベルのオブジェクトであれば、 関数プログラミングだろうがなんだろうがまあ存在する。 また、重ねて恐縮なのだが、対象間の関係を記述するのが数学の すべてという意味なら、それは正しくない。
803 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 15:42:48 ] 何も理解してないバカと説明する気のないバカ
804 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 16:29:33 ] 数値計算に比べて数式処理は世の中の主流になれないみたいな感じなのかな? map f (map g xs) == map (f . g) xsとか、数式処理みたいなものだと思うんだけど。
805 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 17:05:23 ] う〜ん、難しくてよくわからないな。 x = x + 1 みたいな変なのがプログラミングの世界ではまかり通ってる のだけど、こんなの普通の高校や大学初年で習う数学じゃ扱えないはず。 高度な数学なら扱えるのかな?もっと詳しくお聞きしてみたいです。
806 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 17:19:31 ] 数式処理が主流になれない理由は、解析的に解けない問題がたくさんあるから、だね。
807 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 17:38:25 ] >>805 en.wikipedia.org/wiki/Fixpoint_theorem
808 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 18:44:18 ] set-car!とset-cdr!を使って (define a (list 1 2)) このaを'()にすることは可能ですか?
809 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 18:54:26 ] gosh> (define a (list 1 2)) a gosh> (set-car! a 'quote) #<undef> gosh> (set-cdr! a '(())) #<undef> gosh> a '()
810 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 19:11:28 ] 手品みたいですね ()にも出来るのでしょうか?
811 名前:デフォルトの名無しさん [2009/07/13(月) 19:22:14 ] >>804 それは、より正しくは、Numeric ComputationとSymbolic Computationとの 比較のことだと思うが、そうであるとして、 それと、関数プログラミングとそれ以外(おそらく命令型?)の比較は同型ではない。 NCとSCは、806の言うとおり、そもそも活用できる問題領域に大きな差がある。 >>805 x = x + 1 は算数の意味論で言えば明らかに偽な文だが、数学の世界であってもこれが 有意義になる意味論を定義することはできる。 なので一般性をもってその観点でそれを否定することはできない。 命令型プログラミング言語において、この式または文が、x + 1 が環境への参照であり、 x = は環境への束縛の操作であるという意味論であることを想起させにくいという点で いえば同意。
812 名前:デフォルトの名無しさん [2009/07/13(月) 20:43:07 ] >>810 set-car!,set-cdr!は対象がpairであることまでは破壊しないので、 pairとしての表現を持たない空リストにするのは無理じゃないかな。
813 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 20:53:23 ] gosh> (let ((src (list 'a 'a)))(set-car! src 'quote) (set-cdr! src '(()))(eval src (interaction-environment))) () ;; unko-
814 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 21:42:37 ] >>805 > x = x + 1 C/C++ では lvalue と rvalue を区別してフォーマルな意味論を与えられている。 後付けの感は拭えないが、ちゃんと扱える理屈は存在する。 厳密な意味においては数学的とは言えない面はあるけど、 プログラミングに必要な要素ってのを考えると充分な妥協だと思う。
815 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 22:25:27 ] >>805 Hoare Logicだな 実行文の前でのxの値をX,実行文の後ではYとすると このプログラムが正常に動作すると仮定すれば {x=X} x:=x+1 {x=Y}というHoare Tripleが構成できて、代入の規則から x=X ≡ (x+1=Y) <=> x=X ≡ (x=Y-1) ← X = Y - 1 ≡ Y = X + 1 ってな具合にxに1を加えるっていう動作をする事が証明できたりする 代入を感覚で理解できなくて、 a=10,b=20; a=b; a=?,b=?;っていう問題を解けない人でも、この技法を使えば 計算で解くことができる、素晴しい!! 勿論、こういう単純な例だけでなく分岐やループも扱えるんだけど 「ループで配列内要素の総和を求める」っていうような問題でも A4レポート用紙2枚に収まるか怪しいような長い証明を 書く羽目になるから、そうバシバシ使っていけるものでもないな これと比べるとdependently typeとcurry-howard対応の何と実用的なことか…
816 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 22:39:18 ] >>805 代入と等式を混乱していないか
817 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 23:02:30 ] tinyurl.com/mwees3 なんで16年前のメールがgoogleグループにあるんだ?
818 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 23:09:09 ] ログが残っているから
819 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 23:34:06 ] tinyurl.com/m92nbe 5月には圏論をやっとる。
820 名前:デフォルトの名無しさん mailto:sage [2009/07/13(月) 23:42:43 ] 直リン張らないほうがいいな。すまん。
821 名前:805 mailto:sage [2009/07/14(火) 07:36:23 ] >>815 知りたかったのはそういうことです。 関数プログラミングは高校で習った帰納的定義、数学的帰納法など 普通の数学の延長にあるように思えました。 一方、命令型の破壊的代入を主体とするものには理屈はあるのだろうか? と思っていました。実用的なものが関数型だけで書けるとは思ってないのですが。
822 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 07:58:33 ] Static single assignment的に、 X_1 = X_0 + 1 と考えると面白い。 あるlambda式をlambda droppingすると、それは、 対応するSSA文をoptimal変換したことと同じ。
823 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 09:11:10 ] >>821 それならホーア論理じゃなくてチューリング機械じゃないの?
824 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 11:49:11 ] ・表示的意味論(ピラミッドの頂点=神) 数学の延長。 ・公理的意味論 ホーア論理。長い証明を書く羽目に。 ・操作的意味論(食われるだけの存在=ミジンコ) 抽象機械。
825 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 16:03:26 ] >>824 言いたいことはわからなくもないが、3つとも数学だろ。
826 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 16:25:00 ] >>821 意味論というより、命令型プログラミングの根拠となる計算モデルを 知りたいということではないのか? だとすれば、RAMモデルでは破壊的代入が定義されている。
827 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 22:34:41 ] >>824 Aczelの項書換えシステム。文脈原理。
828 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 23:08:19 ] >>805 が知りたいこととは違うかもしれないが プログラミング言語論に関しては 構文論(syntax)と意味論(semantics)という大きな分類がある >>824 の分類は意味論(semantics)の中での分類 構文論はx=x+1の数学的な意味は考えずに これら言語の構造自体について扱う 式の「意味」という意味では 代入に=ではなく:=や<-を代入に割り当てている言語もあるわけで 構文と意味は独立なわけ そもそも数学は代入のような副作用ってあまり扱ってないように思う 俺が知っている中で副作用を扱っているのは 線形論理ぐらいかなぁ A:「100円持っている」 B:「80円以上持っていればパンが買える」 C:「50円以上持っていればチョコレートが買える」 A→Bは真 A→Cは真 よって「100円持っているならばパンとチョコレートが買える」
829 名前:デフォルトの名無しさん mailto:sage [2009/07/14(火) 23:31:26 ] 線形論理ってアスペルガー症候群みたいな感じだね。
830 名前:デフォルトの名無しさん mailto:sage [2009/07/15(水) 00:14:28 ] 逆では? 線形論理では、上の例でA→B∧Cが成り立たない。