関数型プログラミング言語Haskell Part34 (692ﾚｽ)
関数型プログラミング言語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
ﾒﾓ帳
(0/65535文字)
上
下
前
次
1-
新
書
関
写
板
覧
索
設
栞
歴
あと 246 ﾚｽあります
ｽﾚ情報
赤ﾚｽ抽出
画像ﾚｽ抽出
歴の未読ｽﾚ
AAｻﾑﾈｲﾙ
Google検索
Wikipedia
ぬこの手
ぬこTOP
0.009s