関数型プログラミング言語Haskell Part34 (694ﾚｽ)
関数型プログラミング言語Haskell Part34 http://mevius.5ch.net/test/read.cgi/tech/1639713446/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
422: デフォルトの名無しさん [sage] 2024/10/02(水) 22:20:07.75 ID:sFAdPyYV ID:OPLMo7z3 = ID:AFS53MaU 本人か同レベル 複おじってレベル http://mevius.5ch.net/test/read.cgi/tech/1639713446/422
423: デフォルトの名無しさん [sage] 2024/10/02(水) 22:24:19.37 ID:YWEZQEUD 途端に難しくなるか？ 副作用のない計算に変換する手順が教科書に書いてあるはずだが？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/423
424: デフォルトの名無しさん [] 2024/10/02(水) 22:29:49.51 ID:OPLMo7z3 >>422 別の人。自分ならプログラムの記述を一回数学の世界に写すし。 >>423 副作用のある数学的関数ってある？ プログラム→数学 に変換するんだぜ。 副作用のない計算に変換する手順が数学の本に書いてあんの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/424
425: デフォルトの名無しさん [sage] 2024/10/02(水) 22:43:26.42 ID:+kVmY7U4 >>424 別人とのことなので便乗 ID:OPLMo7z3 は ID:AFS53MaU が > 大文字小文字の変換が自然変換になる事を(Haskellの例で)証明して と問われて >>413,414 を出してきたのは数学的証明だと思ってるの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/425
426: デフォルトの名無しさん [sage] 2024/10/02(水) 22:46:45.28 ID:+kVmY7U4 >>424 或いはもっと直接的に、>>424は「大文字小文字の変換が自然変換」の真偽をどう考えているの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/426
427: デフォルトの名無しさん [] 2024/10/02(水) 22:51:00.95 ID:OPLMo7z3 定義が何もないのに何も言えるわけないじゃん。 数学でこういうものを定義します、これをプログラムのこれこれと対応付けます。 てプロセスないじゃん。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/427
428: デフォルトの名無しさん [sage] 2024/10/02(水) 22:52:03.28 ID:YWEZQEUD >>424 先に副作用のないプログラムに変換するって言ってるんですけど Haskellなら最初から副作用がないからそのままでいいけど プログラミング言語の理論の本ならどれにでも書いてないか？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/428
429: デフォルトの名無しさん [sage] 2024/10/02(水) 22:55:13.15 ID:+kVmY7U4 >>427 了解 >>422の指摘通りだと納得しました http://mevius.5ch.net/test/read.cgi/tech/1639713446/429
430: デフォルトの名無しさん [] 2024/10/02(水) 22:56:24.21 ID:OPLMo7z3 いや。プログラム意味論の本結構探し回ったけど副作用の記述は漠然としてて 扱えないわけじゃないらしいけど、具体的な変換なんて見たことない。 ちょうど伝統的なプログラム意味論で副作用どう扱われているか調べているんだ。 なんて本に書いてありましたか？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/430
431: デフォルトの名無しさん [sage] 2024/10/02(水) 23:02:49.62 ID:YWEZQEUD どれにでも書いてあるだろ、whileプログラムをラムダ計算に変換する手順とか書いてないなんてことがあるわけがない http://mevius.5ch.net/test/read.cgi/tech/1639713446/431
432: デフォルトの名無しさん [] 2024/10/02(水) 23:06:08.21 ID:OPLMo7z3 なんだ。いや聞きたいのは入出力とかの副作用だよ。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/432
433: デフォルトの名無しさん [sage] 2024/10/02(水) 23:17:44.98 ID:YWEZQEUD 入出力なんて代入に比べたら自明だろ… そんなのいちいち教科書に書くかよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/433
434: デフォルトの名無しさん [] 2024/10/02(水) 23:26:30.50 ID:OPLMo7z3 書いてないのは自明だからではなくて、研究の方向性がどう転ぶかわからないからだと思う。 表示的意味論も出た当時の文献では副作用について語ってることが多い。 現代的な本になるほどD∞モデルつくってはいおしまいで数学的にきれいなところしかやらない。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/434
435: デフォルトの名無しさん [sage] 2024/10/02(水) 23:36:01.67 ID:JUMm5MLB プログラムの仕様とその証明を数学で記述する本にあるだろうね。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/435
436: デフォルトの名無しさん [sage] 2024/10/02(水) 23:37:10.87 ID:YWEZQEUD どこが非自明なのかさっぱりわからん 代入と違って入出力は垂れ流しだし、入出力は代入の特別な場合だろ http://mevius.5ch.net/test/read.cgi/tech/1639713446/436
437: デフォルトの名無しさん [] 2024/10/02(水) 23:46:11.64 ID:OPLMo7z3 >>435 ホーア論理とか公理的意味論か。いやそれはないな。あっても一般に適用できないし。 >>436 関数型プログラミングだとプログラムをλ式に対応させて、プログラムの実行をそのλ式の簡約に 対応させるというのが理想的なモデルとして想定されることが多いと思う。 でもλ式はλ項からλ項への対応でしかないから、λ項を値(value)と呼ぶとすると value から valueへの数学的関数でしかない。これには入出力とかの副作用を表現する余地がない。 つまり、 入出力があるプログラム→value から valueへの数学的関数 という対応付けをすると、入出力という特徴が数学世界では失われてしまう。 という難問があった、けどモナドで一つ解答が出た。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/437
438: デフォルトの名無しさん [sage] 2024/10/02(水) 23:54:51.93 ID:YWEZQEUD 代入が書けるんだから、入出力なんて自明だろ… こいつ何いってんだ… http://mevius.5ch.net/test/read.cgi/tech/1639713446/438
439: デフォルトの名無しさん [] 2024/10/03(木) 00:02:36.12 ID:B2Xmf+Xl だから、入出力がある数学的関数なんてないだろって言ってんの。 数学的関数で入出力は非自明だと思うんだが。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/439
440: デフォルトの名無しさん [] 2024/10/03(木) 00:09:13.65 ID:B2Xmf+Xl Haskellでいうと、 純粋関数は、λ式（valueからvalueへの数学的関数） に対応付けられるけど、 IOモナド使ったプログラムは、その現実のプログラムが持つ特徴を表現できるλ式がないので対応付けられない って言ってんの。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/440
441: デフォルトの名無しさん [sage] 2024/10/03(木) 00:21:32.37 ID:omgk7HiD 入出力なんてただの値のリストだろ… http://mevius.5ch.net/test/read.cgi/tech/1639713446/441
442: デフォルトの名無しさん [sage] 2024/10/03(木) 03:50:19.64 ID:KCHr29fD 圏論持ち出して愚にもつかないことをグダグダと… それで何か効率良くなるならいいんだけど，何のメリットもないんだよね http://mevius.5ch.net/test/read.cgi/tech/1639713446/442
443: デフォルトの名無しさん [sage] 2024/10/03(木) 04:21:38.74 ID:zyXzLypu 圏論なんかより、遅延評価ならIOがwhnfの先頭に出てきたら実行すればいいって人類が気づいたのが本質なんじゃねーの http://mevius.5ch.net/test/read.cgi/tech/1639713446/443
444: デフォルトの名無しさん [sage] 2024/10/03(木) 08:29:58.17 ID:LNI2TnSo 最近の人類はseqのメリットを直接的に利用するコツに気づいとるんか 順調に進化しとるな http://mevius.5ch.net/test/read.cgi/tech/1639713446/444
445: デフォルトの名無しさん [sage] 2024/10/03(木) 14:31:37.97 ID:1wv2Oz28 コンパクトな言語仕様だが表現力は強力 数学をプログラミングに取り入れるメリットってまぁこんなもんでしかないでしょ 一方で静的に性質を決定しようとするやり方は一般的な人間の能力を簡単に超えてしまう http://mevius.5ch.net/test/read.cgi/tech/1639713446/445
446: デフォルトの名無しさん [sage] 2024/10/03(木) 16:46:40.39 ID:TkNlnb1D 急にポエマーだらけw http://mevius.5ch.net/test/read.cgi/tech/1639713446/446
447: デフォルトの名無しさん [] 2024/10/03(木) 19:56:29.70 ID:B2Xmf+Xl 入出力があるプログラムをどう数学的に整合する概念に対応させるかについて書いてみる。 こういう説明が通るものなのか興味があるし。 まず、仮想的なシェルスクリプト風の行番号付き手続き型言語を想定して、 その言語で入出力があるプログラムを定義するとする。 000 procedure prog1(int n) { 001 double res 002 （なにか込み入った計算） .... 020 echo "hogehoge" 021 （なにか込み入った計算） .... 050 echo "fugafuga" 051 （なにか込み入った計算） ... 100 return res } このプログラムは実行 $(prog1) すると、行番号001版から順に評価していって複雑な計算をしつつ途中 hogehoge ← 行番号０２０の命令を評価 fugafuga ← 行番号０５０の命令を評価 と表示した上で、返り値 res を返す、という動作をする。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/447
448: デフォルトの名無しさん [] 2024/10/03(木) 19:57:08.78 ID:B2Xmf+Xl 現実のよくあるプログラムとはこういう感じのものだけれども、実行 $(prog1) をしてその結果が返ってくるという現実的に 必要な点だけを考えると、途中の行番号020を評価したとかそういう情報はいらなくて、結局 $(prog1) して hogehoge fugafuga を表示して、複雑な計算の結果 res が返ってくれさえすればいいともいえる。 だったら、数学的に取り扱いがしづらい、式の評価途中で入出力が発生するみたいな部分を取っ払って 000 procedure prog2(int n) { 001 double res 002 （なにか込み入った計算） .... 020 ## echo "hogehoge" #コメントアウト 021 （なにか込み入った計算） .... 050 ## echo "fugafuga" #コメントアウト 051 （なにか込み入った計算） ... 100 return ("hogehoge"を表示する予約1、"fugafuga"を表示する予約2、返り値 res) } というように、返り値の部分に全部まとめるということをするということが考えられる。こうしても、プログラムのユーザー側からすると 実行すると$(prog2) hogehoge fugafuga と表示されて複雑な計算した結果 res が返ってくるということは変わらない。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/448
449: デフォルトの名無しさん [] 2024/10/03(木) 19:57:34.71 ID:B2Xmf+Xl というわけで、入出力があるプログラムというのは、こういう返り値の部分というか評価の最終段階の部分に「入出力の予約情報と返り値の情報がまとめられたもの」だったんだ、と整理しよう。 ただ、こういう「入出力の予約情報と返り値の情報がまとめられたもの」と長い文で表すのはよろしくないので、何か名前を与えた方がいいということで computationと呼ぶことにする。 そうすると、Haskellでいえば、 純粋関数は、valueからvalueへの数学的関数 に割り当てることができたけれど、 入出力付きのプログラムについては、valueからcomputationへの対応 に割り当てるということが数学的に正当化できそうだ、ということになるわけだ。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/449
450: デフォルトの名無しさん [] 2024/10/03(木) 20:00:39.07 ID:B2Xmf+Xl 訂正 computationというか、今でいう「入出力の予約情報と返り値の情報がまとめられたもの」を 数学的にうまく正当化するということが達成することができるのであれば、 入出力つきのプログラムを、valueからcomputationへの対応 に割り当てるということが正当化できるはずだ、と考えられる。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/450
451: デフォルトの名無しさん [sage] 2024/10/03(木) 20:23:28.46 ID:zyXzLypu 何言ってるのか全然わからん ぶっちゃけ入力は関数の引数にして、出力は返り値にするように変換するだけでいいだろ 読み出し位置のカーソル管理が必要なら代入を使えばできるじゃん http://mevius.5ch.net/test/read.cgi/tech/1639713446/451
452: デフォルトの名無しさん [] 2024/10/03(木) 20:39:38.40 ID:B2Xmf+Xl よくわかんないけど、そういう入出力プログラムがあったとする。 そしてそれを引数付きで実行することを考えると $(prog n) こうなる。ここで、引数の部分の n はプログラムの記述に属さないといけない。 なぜかというと現実世界の「入力」部分をそのまま引数のところには持ってこれないから。 引数部分を入力にするにしても、別途入力されたものをプログラムの変数に割り当てる概念 みたいなのが必要になるし、それは関数の引数だからということでは説明にならないと思う。 だから、少なくともprogの引数部分はvalueじゃないといけない。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/452
453: デフォルトの名無しさん [sage] 2024/10/03(木) 20:45:47.19 ID:zyXzLypu ポエムすぎて意味わからん。値のリストはvalueじゃないと？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/453
454: デフォルトの名無しさん [] 2024/10/03(木) 20:59:58.72 ID:B2Xmf+Xl 値のリスト自体をそのまま持ってくればvalueということになるんだろうけれど、 $(prog n) の実行結果として出てくるもので、計算効果の説明になるものであって、返り値の型を包含するもの であればcomputationと判断せざるを得ないとかそういうことしか言えないです。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/454
455: デフォルトの名無しさん [sage] 2024/10/03(木) 21:11:15.46 ID:zyXzLypu 判断するって何言ってるの？ computationって定義は何なの？ ラムダ項を書き換えていく手続きが計算じゃないの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/455
456: デフォルトの名無しさん [] 2024/10/03(木) 21:22:37.64 ID:B2Xmf+Xl valueとcomputationの違いは微妙で$(prog n)の実行結果として出てくるかどうかとか 計算効果が発露しているかというところで見極めるしかない、と理解している。判断する というのは専門用語としては使ってない。 computationの定義はまた微妙だけれど、$(prog n)の計算効果込みの実行結果みたいな概念。 最後は超個人的見解だけど、「λ項を書き換えていく行為」というのは、どういう方法で表現して どういう方法で簡約していくか？というところが決まってない。λ計算じゃないけれど、 １＋１＝２ という計算を暗算でやるか、電卓でやるか、そろばんでやるかという違いを出しても計算することに 変わりない。 暗算でやると、脳内物質の分量が変わるし、電卓だと電位が変わる。そして、そろばんでやると 「ぱちぱち」という音が出る。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/456
457: デフォルトの名無しさん [sage] 2024/10/03(木) 21:30:24.72 ID:zyXzLypu ❌決まってない ⭕知らない 間違えるなよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/457
458: デフォルトの名無しさん [sage] 2024/10/03(木) 21:31:19.82 ID:zyXzLypu お前の脳内にしかないお花畑に巻き込むのやめてもらっていいですか？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/458
459: デフォルトの名無しさん [sage] 2024/10/03(木) 22:10:04.42 ID:/brOvmjG おそらくメンタルヘルスに問題がある方なのかな？ 自分の頭の中の映像をそのまま言葉にしたような感じを受ける http://mevius.5ch.net/test/read.cgi/tech/1639713446/459
460: デフォルトの名無しさん [] 2024/10/04(金) 05:46:29.14 ID:vLDssEdm >>428 Haskellの副作用については2つの解釈がある。 １．副作用も含めてアクションという単位で値としてみる。 （アクションを受け取って、アクションを返す関数） ２．Haskellは指示書を発行しているだけで、実際に実行するのは数学（Hakell）の外だから、Haskellそのものには副作用が無い。 （（末尾にHaskellに値を返す形の）マシン語を返して、ハードウェアに実行してもらうと考えるアウトソーシング方式） http://mevius.5ch.net/test/read.cgi/tech/1639713446/460
461: デフォルトの名無しさん [sage] 2024/10/04(金) 05:52:21.21 ID:EogKDI3R >>460 ようするに副作用はないってことじゃん http://mevius.5ch.net/test/read.cgi/tech/1639713446/461
462: デフォルトの名無しさん [] 2024/10/04(金) 05:57:16.46 ID:vLDssEdm >>461 Javaは変数をクラスの外で作れないから、グローバル変数は存在しない。 けど、事実上のグローバル変数は作れてしまう。 ってのと、同じ。 アクションの中に副作用があろうが、マシン語を返していると解釈しようが、事実として副作用はある。 ただ、重要なのは副作用を伴っても参照透明性が保たれているってこと。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/462
463: デフォルトの名無しさん [sage] 2024/10/04(金) 06:07:02.79 ID:4jD3Hbcp 副作用が隔離できていることが大切 スレの基地外の隔離スレのように http://mevius.5ch.net/test/read.cgi/tech/1639713446/463
464: デフォルトの名無しさん [sage] 2024/10/04(金) 06:24:04.70 ID:EogKDI3R >>462 それは例えばwhileプログラムから副作用のない言語に変換したあとの形式と同じ状態にすでになってるってことで、計算のルール上はもう副作用はないでしょ http://mevius.5ch.net/test/read.cgi/tech/1639713446/464
465: デフォルトの名無しさん [] 2024/10/04(金) 07:22:19.19 ID:vLDssEdm >>464 そうなんだけど、結局普通のプログラミング言語を使ってる人にしてみれば屁理屈でしかない。 見た目そのままで伝えるなら、純粋関数型言語の定義のまんま、「副作用を伴っても参照透明性が保たれている」でいい。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/465
466: デフォルトの名無しさん [sage] 2024/10/04(金) 07:38:19.23 ID:EogKDI3R >>465 まあそのほうがいいか 上の方にいた彼はなんか脳内にこだわりがあって、普通の型付きラムダ計算以上のことをやってると思ってるフシがあったね http://mevius.5ch.net/test/read.cgi/tech/1639713446/466
467: デフォルトの名無しさん [] 2024/10/04(金) 07:48:51.79 ID:vLDssEdm >>466 そうそう。 副作用は無い！って、こっちが必死になって弁を述べれば述べるほど、屁理屈感が出てくる。 それよりは副作用を認めて、「副作用を分離」「副作用を伴っても参照透明性が保たれている」って言った方が、納得感がある。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/467
468: デフォルトの名無しさん [] 2024/10/04(金) 19:23:08.02 ID:tixO3LDq とりあえず続きを書いてみる。 Haskellでいうところの 純粋関数は、valueからvalueへの数学的関数 入出力プログラムは、valueから（入出力）computationへの対応 に割り当てることで、数学上にプログラミング行為を写し出せそうだ、というところまで書いた。 ただ、やっぱり（入出力）computationって何？とか、valueと形式的にどう違うの？という疑問は拭い去ることができない。 そこでMoggiは、次のようなアイディアを２つ出して（結構ムリヤリに）疑問を解決した。 ただし、ここで入出力プログラム prog は A型の引数を取って（computationの整理をする前は）B型の返り値を返すとする。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/468
469: デフォルトの名無しさん [] 2024/10/04(金) 19:23:42.06 ID:tixO3LDq Moggiのアイディア１ ・返り値の型がBのcomputationは、何か型構築子をIOとすると、その型構築子を適用した型 IO B のvalueに対応する。 ※Moggiの原理ともいう。 つまり、上で挙げた入出力プログラム prog の型は、具体的に A → IO B になると言っている。 IO B 型の実装で、入出力の予約だか、値のリストだか指示書だか表現はいろいろあるが、そういう機構を実装すれば、 prog :: A → IO B は参照透過性を保ったまま入出力を行うプログラムになる。 もっと広がりが出そうなcomputation概念なのに、急に狭窄な感じがするアイディアだけれど、 実装と折り合いをつけるという観点からすると仕方ないともいえる。 なお、代数的効果のPlotkinとPowerが批判しているのはこのMoggiのアイディア１である感じがする（あんまわかってない）。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/469
470: デフォルトの名無しさん [] 2024/10/04(金) 19:24:13.18 ID:tixO3LDq Moggiのアイディア２ ・入出力プログラム（に対応する数学的概念）は、圏をなすはずだ。 Moggiのアイディア１の段階でもprog :: A → IO Bは参照透過性を保ったまま入出力を行うプログラムになるはずだが、 入出力プログラム同士の合成が考えられていない。入出力プログラム prog1、prog2と開発したら、できるだけ再利用するというのが 現実のプログラミングだと思う。わざわざprog1とprog2の合成として定義できそうなプログラムを得るために、イチイチいちから 開発するということを理論的に要請されるというのは不合理。 純粋関数は、λ式に割り当てられることになって、当然、圏をなすだろうに、 プログラムに割り当てられるものが圏を成さないというのはおかしい。 でも、入出力プログラムはMoggiのアイディア１から、 prog :: A → IO B という特殊な返り値の型を持っているため単純な合成ができない。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/470
471: デフォルトの名無しさん [] 2024/10/04(金) 19:29:03.13 ID:tixO3LDq Moggiのアイディア１の段階でcomputationの概念というのは解消してしまう。 PlotokinとPowerはそこが不満なんだろうか？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/471
472: デフォルトの名無しさん [sage] 2024/10/04(金) 20:18:31.78 ID:WSIC8Xt5 だから、副作用を隠してラムダ計算に変換する手続きは、世界をステートにする変換をした時点で達成されてるわけで、そんなの太古の昔から分かってたことだろ IO aの定義読んでから出直せよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/472
473: デフォルトの名無しさん [sage] 2024/10/04(金) 20:30:15.44 ID:SclsbEZF 日を跨ぐつもりならコテハンでも付けてくれんか 追えん http://mevius.5ch.net/test/read.cgi/tech/1639713446/473
474: デフォルトの名無しさん [] 2024/10/04(金) 20:44:30.01 ID:tixO3LDq >>472 だからそれはわかっているって。評価途中では実際の入出力はせず指示書だか値のリストだけ作成して 参照透過性を保証して、参照透過性が要求されなくなったプログラムの最終段階でリストに従って 入出力を実行するような仕組みがあれば、参照透過性を保ったまま入出力はできるという話でしょ。 それを数学的にどう正当化するかという話を書いているんだって。 >>473 水曜日あたりからだからそんな分量ないよ。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/474
475: デフォルトの名無しさん [sage] 2024/10/04(金) 20:49:17.68 ID:WSIC8Xt5 >>474 どこが正当化されてないのか意味不明なんだけど ていうか正当化って何？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/475
476: デフォルトの名無しさん [] 2024/10/04(金) 20:51:48.70 ID:tixO3LDq だから、入出力がある数学的関数なんてないじゃん。 入出力があるプログラムを数学的に表現しようと思っても詰むからどうしようって話。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/476
477: デフォルトの名無しさん [sage] 2024/10/04(金) 20:57:28.69 ID:6lZW+X9H こんなところで長文書くのはやめてもろて 読む価値があるものならzennとかnoteに書けば？ 関数型言語界隈の人たちがクソミソにレビューしてくれるよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/477
478: デフォルトの名無しさん [sage] 2024/10/04(金) 20:58:08.93 ID:WSIC8Xt5 >>476 型付きラムダ計算の時点で数学的に表現されてるだろ… 意味不明すぎる http://mevius.5ch.net/test/read.cgi/tech/1639713446/478
479: デフォルトの名無しさん [sage] 2024/10/04(金) 21:00:48.64 ID:qBjLuAvO メインの入力とメインの出力は数学にもある 主じゃないやつを副作用といってる http://mevius.5ch.net/test/read.cgi/tech/1639713446/479
480: デフォルトの名無しさん [] 2024/10/04(金) 21:11:30.04 ID:tixO3LDq >>478 なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。 でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？ >>479 よくわかんない。具体的に言うとどういうのある？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/480
481: デフォルトの名無しさん [] 2024/10/04(金) 21:11:31.21 ID:tixO3LDq >>478 なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。 でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？ >>479 よくわかんない。具体的に言うとどういうのある？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/481
482: デフォルトの名無しさん [sage] 2024/10/04(金) 21:18:24.66 ID:WSIC8Xt5 >>480 アセンブルって何？ 後半も何言ってるのかちゃんと分かるように書いて http://mevius.5ch.net/test/read.cgi/tech/1639713446/482
483: デフォルトの名無しさん [sage] 2024/10/04(金) 21:25:06.50 ID:WSIC8Xt5 そうだよ、こんなとこじゃなくてzennとかに煽った感じのタイトルつけて炎上する記事書いてコメントもらって来いよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/483
484: デフォルトの名無しさん [] 2024/10/04(金) 21:28:05.10 ID:tixO3LDq λ計算を機械語とかアセンブラと見立てて、λ計算ですべて数学世界を組み立てれば、 入出力がある数学的関数も定義できるだろうから、あえて数学的正当性なんて与えようとする 理由がわからない、ということだろうと思った。 プログラムの部分は全てλ計算で組み立てれば完全に同じものが作れると思っているということ だけれども、じゃあ文字列をディスプレイに表示するというプログラムの構成要素である ディスプレイはハードウェア部分だけれども、それはλ計算で組み立てるという範疇にはいるんですか？ 入らないなら、なにか数学的概念を持ち出してきてそれに対応付けるということをしないといけないんじゃ ないですか？ という趣旨のことを書いた。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/484
485: デフォルトの名無しさん [] 2024/10/04(金) 21:33:15.17 ID:tixO3LDq これ読んだらわかるけどMoggi論文の読書感想文。いまさらの。 匿名以外でいまさら突っ込んでくるわけないじゃん。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/485
486: デフォルトの名無しさん [] 2024/10/04(金) 21:33:16.29 ID:tixO3LDq これ読んだらわかるけどMoggi論文の読書感想文。いまさらの。 匿名以外でいまさら突っ込んでくるわけないじゃん。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/486
487: デフォルトの名無しさん [sage] 2024/10/04(金) 21:34:24.07 ID:qBjLuAvO 関数の「型」を見ろ 入力が何で出力が何かが宣言されている http://mevius.5ch.net/test/read.cgi/tech/1639713446/487
488: デフォルトの名無しさん [] 2024/10/04(金) 21:39:26.17 ID:tixO3LDq >>484 ディスプレイに表示するまでの概念はよく考えたら既存の例でもなかったわ。 焦って変なこといったスマン。 ちょっと説明を考える。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/488
489: デフォルトの名無しさん [sage] 2024/10/04(金) 21:39:59.29 ID:WSIC8Xt5 >>484 意味不明すぎる ラムダ計算は数学的に正当化されてるだろ 例えば合流性があるとか数学的に証明されてる これのどこに非数学的要素があるんだって言ってるんだよ すでに数学的な説明がされてるものに対して、数学的に正当化されてないとか言うのやめろよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/489
490: デフォルトの名無しさん [] 2024/10/04(金) 21:48:55.49 ID:tixO3LDq λ計算が数学的に正当化されてないというような話はしてなくて、 現実のプログラムをλ計算に反映させようと思っても入出力とか非決定計算の部分は表現しきれない そのλ計算からはみ出す部分をどう正当化させようかという話。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/490
491: デフォルトの名無しさん [sage] 2024/10/04(金) 21:52:13.21 ID:WSIC8Xt5 >>490 じゃあHaskellは純粋にただの型付きラムダ計算なんだから、数学的に正当化されてない部分などない おしまい http://mevius.5ch.net/test/read.cgi/tech/1639713446/491
492: デフォルトの名無しさん [] 2024/10/04(金) 22:03:12.33 ID:tixO3LDq >>491 うーん。例えば、数学は集合論上で展開されているから、集合論があればその上で展開される 解析学とか、線形代数学とかいらない、みたいな論法じゃない？ この現象は、解析学でモデル化できるけれども、解析学は集合論上で展開できるから、 そんなモデル化はいらなくていちいち集合論の言葉で書けばいいじゃん的な。 みんなそこに興味あるわけじゃないと思いますよ。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/492
493: デフォルトの名無しさん [] 2024/10/04(金) 22:08:30.14 ID:vLDssEdm >>484 横からというか >460 書いた者だけど、あなたの疑問は解釈1の「アクションを受け取ってアクションを返す関数」だとざっくりし過ぎて納得いかないって感じでしょうか？ でしたら、解釈2では納得出来ませんでしょうか？ 解釈２は、モナドの効能の一つに追加して「数学の世界にアウトソーシングという概念を持ち込む」というものです。 モナドの例えとして、床下配線というのがありますが、MaybeやListの様な通常のモナドも、>>=の中に関数適用部分を押し込んで、表から見えないようにしています。 （これも、見ようによってはアウトソーシングです。同じ数学の世界なので、隣の席に頼んだ感じですが） IOモナドは、>>=の中すら見えない状態で関数適用しているわけですが、 >460 でも書いたとおり、「数学の外（ハードウェア）」で関数適用されていると考えるわけです。 IOモナドの>>= は、外の世界と遣り取りする受付窓口というわけですね。 （実際、バッファの様な振る舞いをします） main = do x <- return 0 _________x <- return (x + 1) _________print x http://mevius.5ch.net/test/read.cgi/tech/1639713446/493
494: デフォルトの名無しさん [sage] 2024/10/04(金) 22:14:36.08 ID:WSIC8Xt5 >>492 ラムダ計算も集合論上で展開されてるだろ だから、Haskellも集合論の言葉で書かれてるじゃん そんな誰もが分かってるけど、いちいち書いても何の得もないことを話したかったの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/494
495: デフォルトの名無しさん [] 2024/10/04(金) 22:16:42.74 ID:vLDssEdm この場合、IOモナドを使って変数ｘを書き換えているのではなく、シャドーイングによって同じｘという名前の変数を新しく作って、古い x に +1 した値を束縛しています。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/495
496: デフォルトの名無しさん [] 2024/10/04(金) 22:21:54.69 ID:tixO3LDq >>493 ごめんなさい。全然違う。入出力を題材にしているのはあくまで例で別に疑問はないです（実装をちゃんと知っているわけではないですが）。 モナドを導入する動機はMoggi論文読んだ読書感想文なので途中まで書いてますが、圏をなすかどうかです。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/496
497: デフォルトの名無しさん [] 2024/10/04(金) 22:27:08.92 ID:vLDssEdm 無理やりハードウェアも数学と言い張るなら、ハードウェアもチューリングマシンという計算モデルなので数学が元と言えなくはない？ そういうこじつけは置いておいても、IOモナドをアウトソーシングと考えると、じゃあ外の世界はめちゃくちゃか？と考えて、そうではないと気付く。 ハードウェアも一定の秩序がある。 数学だけが全てではないのかもしれない。 何かしらの秩序というか、法則性を持った世界（数学、数学以外含む）どうしのやり取りにモナドが橋渡しとして働いているのでは？とか、考えたりする。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/497
498: デフォルトの名無しさん [] 2024/10/04(金) 22:28:17.05 ID:tixO3LDq >>494 モナドの原論文（Moggiの論文）の読書感想文を入出力の計算効果を題材に解説してみているんだって。 ブログに書いても今更突っ込むなんて恥ずかしいことができる人はいるわけないので、ここに書いている。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/498
499: デフォルトの名無しさん [sage] 2024/10/04(金) 22:32:08.56 ID:WSIC8Xt5 >>498 その人はHaskellは数学的に正当化されてないけしからんって言ってたの？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/499
500: デフォルトの名無しさん [sage] 2024/10/04(金) 22:34:04.82 ID:WSIC8Xt5 最低限、論文に書いてある正しいこととお前の妄想がはっきり区別できるように感想文を書けよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/500
501: デフォルトの名無しさん [] 2024/10/04(金) 22:44:05.60 ID:tixO3LDq >>499 はっきりそうは言ってない。 プログラムをλ項に対応させて単純化させると、valueからvalueへの全域関数となるけれど、 そう考えると、非停止性とか非決定性、副作用といった現実のプログラムにある特徴が失われる（だからそれを何とかしようと読める）。 >>500 そんなことできるほど力量ないです。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/501
502: デフォルトの名無しさん [] 2024/10/04(金) 22:46:51.98 ID:vLDssEdm >>496 少なくともコマンド系のプログラムは圏をなしますね。 Haskellで作ると実感しますが、Haskellに限らず、 （ユーザーから見て）プログラムそのものが関数になります。 Linuxでコマンドをパイプライン処理するのは関数（射の）合成に相当しますし。 id相当のプログラムは作れますし。 ・・・と考えると圏をなすと思うのですが。 （GUIプログラムもボタン単位とかで関数と言えますが、合成は…押した順序？） 例えば {(x,2x+1) | x ∈ R} と 2x+1のグラフは同型だと直感的に分かりますが、その関数（射）は数式で表せません。 圏論では、可換図を受け取って可換図を返すとか出てきますので、{(x,2x+1) | x ∈ R} と 2x+1のグラフを結ぶ関数（射）が人間って言うのも有かな？とか、考えます。 （圏論では同型と分かれば（証明できれば）よくて、射の中身には言及しない） http://mevius.5ch.net/test/read.cgi/tech/1639713446/502
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 192 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.014s