Lisp Scheme Part26

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) 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 なんで１６年前のメールが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が成り立たない。 831 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 04:13:43 ] >>828 805です。自分でも何を知りたいのか混乱していました。 表示的意味論です。 「プログラム意味論」横内寛文著（赤本）は持っているのですが よく理解できていません。R^5RSに収録されているのは表示的意味論 とのことで理解したいとは思うのですが。 ところでR^6RSでは表示的意味論が放棄されて操作的意味論になった そうですが何故なのかと思っています。 832 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 05:12:42 ] Operational Semanticsは意味論を勉強してなくても簡単に理解できるからな。 833 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 05:18:25 ] > 「プログラム意味論」横内寛文 その本読んでみたいんだけど売ってないんだよね。 834 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 12:17:28 ] >>831 ＞ところでR^6RSでは表示的意味論が放棄されて操作的意味論になった ＞そうですが何故なのかと思っています。 表示的意味論が分かり難い上に実装にも証明にもあまり役に立たないから。 しかもR5RSのは矛盾だかあいまいさが証明されてたはず。 835 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 17:43:24 ] >>805 意味論を理解することが目的なら、もう少し具体的に今どこがわからないのかを 示せばここで解説される可能性はある。 意味論がさっぱりわからん、ということでしかないとすると、本読め、以外にない。 意味論を理解することが目的じゃなくて、何かをするために意味論を理解したい なら、目的を示した方がいいと思う。それについて助言可能かもしれない。 836 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 18:08:29 ] >>828 いや、変数、変項、というのは形式的な数学では日常茶飯事だから、 代入というのは数学でもよくある概念じゃないか? それは人間の 頭の中で実施されることが多いが、何かを証明するときに紙に 書いたりもする。 よくある概念であるがゆえ、それ自体が明示的な対象となるのは数学基礎論 にはなるが。 あと、一見代入だからといって副作用を伴うとは限らない。 述語論理のユニフィケーションとかもあるし。 837 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 18:17:42 ] 代入？いいえ項書換えです 838 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 18:25:32 ] >>835 805です。数学がわからないと数学を必要とするコンピューターの理論も 理解できないのではないかと思いしばらくの間、数学の勉強に行っていました。 目的はプログラムと数学との関連の理解です。 本を読みつつ、ご助言を仰ぐこともあるかもしれません。よろしくお願いいたします。 839 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 18:49:37 ] 真面目に勉強するなら２ｃｈにレスしてないで本読めでぶ 840 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 19:03:00 ] >>839 ああ、ここは2chだってことを忘れてた。でも玉石混交だから。 841 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 19:18:18 ] >>838 それなら、まずは計算可能性理論を勉強してみると良いな。 842 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 20:27:45 ] >>838 上にでてきたfjとか。2chだとせっかくの話が消えてしまう。 ただ、迷惑にならないようにしたほうがいいだろうけど。 843 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 21:04:29 ] >>802 >また、重ねて恐縮なのだが、対象間の関係を記述するのが数学の >すべてという意味なら、それは正しくない。 難しい話になるとは思うのですが、現時点では”数学”とは何を指している 言葉だといえるのですか。 マックレーンはアイディアを抽出化して形式化したものが数学だ、形式機能主義だ と言ってるんですけど、それって、つまり数学的対象とはあくまで形式という事なんですか。 確かに、理解していないバカではある。書いてて確かに思う。 けど、表立っては出ないがこういう話が問題になる分野領域は存在する気がするんだよね。 844 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 21:16:33 ] もう十分以上の情報が出ているぞ 耳学問としょうもないプライドのせいで 無知だとかバカだとか思われたくないからいつまでも演説を続けるんだろうが いいかげん黙れ 845 名前：デフォルトの名無しさん mailto:sage [2009/07/15(水) 21:19:29 ] 805=815で釣りでもやってるのかと思ったが 846 名前：802 mailto:sage [2009/07/15(水) 22:41:53 ] >>844 おお、すまなかった。誰を指しているかがイマイチわからんが、 この流れをつくった私がいけないのだろう。 >>843 というわけで、すまんが退散しようと思う。844の言うとおり、 結構いろいろな情報が出ているので、参考にして欲しい。 お邪魔しました。 847 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 01:17:17 ] >>844 混在してわけがわからないことになってるけど、いくつか独立した話しが 並行して進んでいるんだよ。 それに、そんなぶっきらぼうに言っちゃうとみんなびっくりしてしまうよ。 848 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 01:43:59 ] たまに情報学板のことも思い出してあげてください。 849 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 01:48:23 ] 確かに最近の話題は情報学板の方が向いてるな。 あそこ過疎りすぎだけど、見てる奴はそれなりにいるっぽい。 850 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 03:37:46 ] >>838 数学とか理論計算機科学の話題だったらプログラム板はやめておいたほうがいいよ。 でたらめな情報が多すぎてろくなことがないから。 851 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 04:02:29 ] >>850 情報学板に移動するよ。ありがとう。 852 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 08:45:47 ] ERR5RS（だっけ？）って幾らかでも流行ってるんですか？ 853 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 13:51:52 ] 顧みるにR5RS自体流行ってるかな？ お察しください 854 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 16:05:08 ] LOL邦訳本ってamazonじゃ普通に買えないんだろうか。 ページはあるんだけど、なぜかプレミア価格の出品しかない。(´・ω・`) 855 名前：デフォルトの名無しさん mailto:sage [2009/07/16(木) 22:57:07 ] まさかすぐに絶版にしたりしないよね？ 856 名前：デフォルトの名無しさん mailto:sage [2009/07/17(金) 00:11:40 ] SICPの悪文と格闘している間にLOL翻訳が出てしまったんだな。 On Lispも積読になってるが、LOLも積読しとく事にしよう。 以上チラ裏でした（・∀・）

---

---

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

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