関数型プログラミング言語Haskell Part34 (667ﾚｽ)
関数型プログラミング言語Haskell Part34 http://mevius.5ch.net/test/read.cgi/tech/1639713446/
上
下
前
次
1-
新
通常表示
512ﾊﾞｲﾄ分割
ﾚｽ栞
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
503: デフォルトの名無しさん [sage] 2024/10/04(金) 22:50:56.01 ID:WSIC8Xt5 >>501 なんでラムダ項に対応させると全域関数になるわけ？ラムダ計算は停止しない計算も表現できるモデルでしょ 言ってることが意味不明なんだよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/503
504: デフォルトの名無しさん [] 2024/10/04(金) 22:52:29.23 ID:tixO3LDq ただの圏じゃなくてクライスリ圏じゃないといけない（Moggiのアイディア１から）。 そして、クライスリ圏を定義するためにはクライスリ・トリプル（モナド）がいる http://mevius.5ch.net/test/read.cgi/tech/1639713446/504
505: デフォルトの名無しさん [] 2024/10/04(金) 22:52:30.15 ID:tixO3LDq ただの圏じゃなくてクライスリ圏じゃないといけない（Moggiのアイディア１から）。 そして、クライスリ圏を定義するためにはクライスリ・トリプル（モナド）がいる http://mevius.5ch.net/test/read.cgi/tech/1639713446/505
506: デフォルトの名無しさん [sage] 2024/10/04(金) 22:54:07.35 ID:WSIC8Xt5 そもそもラムダ項は関数ではないし、集合ではあるということはできるけど、それは自然数1は集合であるみたいな話でそれに意義なんてないよ http://mevius.5ch.net/test/read.cgi/tech/1639713446/506
507: デフォルトの名無しさん [] 2024/10/04(金) 23:02:32.42 ID:vLDssEdm >>504 >398 じゃ答えにならない？ http://mevius.5ch.net/test/read.cgi/tech/1639713446/507
508: デフォルトの名無しさん [sage] 2024/10/04(金) 23:02:43.19 ID:6lZW+X9H 流石にこれじゃ関数型界隈の人達にボコボコにされて終わるね やめといた方がいい http://mevius.5ch.net/test/read.cgi/tech/1639713446/508
509: デフォルトの名無しさん [] 2024/10/04(金) 23:04:12.66 ID:tixO3LDq βη簡約するとλ項が別の簡約されたλ項になる。この対応関係を数学的関数とみなせると言ってると解釈してる。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/509
510: デフォルトの名無しさん [sage] 2024/10/04(金) 23:12:30.87 ID:WSIC8Xt5 >>509 みなせるって何？ ようするにラムダ項は関数じゃないってことでしょ当たり前だけど http://mevius.5ch.net/test/read.cgi/tech/1639713446/510
511: デフォルトの名無しさん [] 2024/10/04(金) 23:14:09.18 ID:tixO3LDq 全域関数となる理由はわからん。全域関数＝数学的関数ということを言いたいんだろうと思ってたけどそこから詰めてなかった。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/511
512: デフォルトの名無しさん [sage] 2024/10/04(金) 23:22:52.03 ID:WSIC8Xt5 >>511 お前が言い出したんだろ http://mevius.5ch.net/test/read.cgi/tech/1639713446/512
513: デフォルトの名無しさん [sage] 2024/10/04(金) 23:30:08.11 ID:6lZW+X9H これがワードサラダか http://mevius.5ch.net/test/read.cgi/tech/1639713446/513
514: デフォルトの名無しさん [] 2024/10/04(金) 23:41:03.02 ID:tixO3LDq すまんね。準備不足だったわ。詰めるところわかったし、 詰めるところ詰めることができたらひっそりどっかに書くことにするわ。 いろいろコメント参考になったわ。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/514
515: デフォルトの名無しさん [sage] 2024/10/05(土) 00:27:27.96 ID:aeHKoAMv 集合と写像の区別がついてないんだから、何を準備しようが時間の無駄 http://mevius.5ch.net/test/read.cgi/tech/1639713446/515
516: デフォルトの名無しさん [sage] 2024/10/05(土) 07:57:53.70 ID:jwoAd9Km ZFでは集合しか無いから。写像だろうが、自然数だろうが何でも集合。全てを集合で実装する世界。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/516
517: デフォルトの名無しさん [] 2024/10/05(土) 08:14:37.65 ID:JByJwyk5 圏論は逆で、対象（集合で言う元）を恒等写像と同一視して全てを射（写像）として扱うね。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/517
518: デフォルトの名無しさん [sage] 2024/10/05(土) 08:53:09.61 ID:jwoAd9Km 対象Aに対しA=id_Aとする圏の定義は、射のクラスの上での全域的で無い結合的2項演算⚪︎を持つ代数系としての簡潔な定式化。この定義では圏には射しかなくて、対象とは恒等射の別名に過ぎない。 ただ、この圏の実装は入門者には分かり難い。 Aが圏Cの対象であることを古い文献はA in Ob(C)と書くことが多いけど、最近の文献はA in Cと書いてしまう。fが圏Cの射f:A --> Bなことはf in Hom_C(A,B)かf in Mor_C(A,B)。 http://mevius.5ch.net/test/read.cgi/tech/1639713446/518
519: デフォルトの名無しさん [sage] 2024/10/05(土) 10:51:32.56 ID:KE+ltgGd 普通のλはどの順序で適用しても同じ計算結果になる（Church-Rosserの定理）けど 副作用を伴うλは適用順序が入れ替わると副作用の順序も変わって同じ結果とは言えなくなるから 順序を保証する仕組みとしてモナドが応用されてるはず IO a >>= (a -> IO b) -> IO b は(a -> IO b)が(IO a)を受け取れないから (IO a)からaを取り出せるところまで計算しないと(a -> IO b)を適用できない 仮に IO a -> (IO a -> IO b) -> IO b みたいな形だと(IO a)の計算を保留したまま(IO a -> IO b)を適用できる 圏論はよく分からないけど 圏Aに便宜的な時間軸をつけたA_t0, A_t1, A_t2, …を用意して関手 A_t0 → A_t1, A_t1 → A_t2, … を作るとA_t0, A_t1…は全部AのクローンだからA_t0 → A_t1, …は自己関手になって その自己関手の集合がなんやかんやでモナドに相当するみたいなイメージ http://mevius.5ch.net/test/read.cgi/tech/1639713446/519
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 148 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.021s