関数型プログラミング言語Haskell Part34 (667ﾚｽ)
上下前次1-新
417: 2024/10/02(水)21:18 ID:JUMm5MLB(1/2) AAS
数学の研究には有用かも知れないが
プログラミングで
直接役に立つようなことはまず無い
418: 2024/10/02(水)21:42 ID:Xrjxo4NT(1) AAS
どっ白け
419: 2024/10/02(水)21:51 ID:OPLMo7z3(1/8) AAS
プログラミング言語もどんどん数学に寄せているし、上のカキコみたいにプログラムの記述を
そのまま数学的対象とみなせるように改造していってると思う。本来は別物と考えるべきだと思う。
数学の研究といってもプログラム意味論の研究で、プログラムを数学の世界に写像したら
どう表現できるかということを研究していると言えるんじゃないかと思う。
数学の世界には、式の評価途中に発生する副作用といった概念がないので、現実のプログラムを
そのまま数学の世界に移そうと思ってもできないことの方が多い。
計算効果を圏論的に表現できたというのは、そういうプログラミング言語の数学化の一端みたいな
もんだと思う。
420: 2024/10/02(水)22:00 ID:YWEZQEUD(1/7) AAS
副作用ってどうでもよくね
Haskellとかだとそもそも副作用ないし
421: 2024/10/02(水)22:12 ID:OPLMo7z3(2/8) AAS
現実のプログラムだと式を評価する途中で発生する副作用というのは普通だけれど、
これを表示的意味論、操作的意味論で数学の世界に写そうと思うと途端に難しくなる。
数学で式の途中に文字列をディスプレイに映し出す、みたいな概念はないから。
それを整理して副作用と呼んでも差し支えない概念を提唱してHaskellに実装しているんだよ。
実際、ＩＯモナドの圏論的定式みるとこれが副作用？という表式してる。
全部後回しにしてフラッシュするというアイディアみたい。副作用をプログラムの最終局面で
実行しているから、式の評価途中の参照透明性も壊さない。なるほど、って感じ。
422(2): 2024/10/02(水)22:20 ID:sFAdPyYV(1) AAS
ID:OPLMo7z3 = ID:AFS53MaU 本人か同レベル
複おじってレベル
423(1): 2024/10/02(水)22:24 ID:YWEZQEUD(2/7) AAS
途端に難しくなるか？
副作用のない計算に変換する手順が教科書に書いてあるはずだが？
424(3): 2024/10/02(水)22:29 ID:OPLMo7z3(3/8) AAS
>>422
別の人。自分ならプログラムの記述を一回数学の世界に写すし。
>>423
副作用のある数学的関数ってある？
プログラム→数学
に変換するんだぜ。
副作用のない計算に変換する手順が数学の本に書いてあんの？
425: 2024/10/02(水)22:43 ID:+kVmY7U4(1/3) AAS
>>424
別人とのことなので便乗
ID:OPLMo7z3 は ID:AFS53MaU が
> 大文字小文字の変換が自然変換になる事を(Haskellの例で)証明して
と問われて
>>413,414 を出してきたのは数学的証明だと思ってるの？
426: 2024/10/02(水)22:46 ID:+kVmY7U4(2/3) AAS
>>424
或いはもっと直接的に、>>424は「大文字小文字の変換が自然変換」の真偽をどう考えているの？
427(1): 2024/10/02(水)22:51 ID:OPLMo7z3(4/8) AAS
定義が何もないのに何も言えるわけないじゃん。
数学でこういうものを定義します、これをプログラムのこれこれと対応付けます。
てプロセスないじゃん。
428(1): 2024/10/02(水)22:52 ID:YWEZQEUD(3/7) AAS
>>424
先に副作用のないプログラムに変換するって言ってるんですけど
Haskellなら最初から副作用がないからそのままでいいけど
プログラミング言語の理論の本ならどれにでも書いてないか？
429: 2024/10/02(水)22:55 ID:+kVmY7U4(3/3) AAS
>>427
了解
>>422の指摘通りだと納得しました
430: 2024/10/02(水)22:56 ID:OPLMo7z3(5/8) AAS
いや。プログラム意味論の本結構探し回ったけど副作用の記述は漠然としてて
扱えないわけじゃないらしいけど、具体的な変換なんて見たことない。
ちょうど伝統的なプログラム意味論で副作用どう扱われているか調べているんだ。
なんて本に書いてありましたか？
431: 2024/10/02(水)23:02 ID:YWEZQEUD(4/7) AAS
どれにでも書いてあるだろ、whileプログラムをラムダ計算に変換する手順とか書いてないなんてことがあるわけがない
432: 2024/10/02(水)23:06 ID:OPLMo7z3(6/8) AAS
なんだ。いや聞きたいのは入出力とかの副作用だよ。
433: 2024/10/02(水)23:17 ID:YWEZQEUD(5/7) AAS
入出力なんて代入に比べたら自明だろ…
そんなのいちいち教科書に書くかよ
434: 2024/10/02(水)23:26 ID:OPLMo7z3(7/8) AAS
書いてないのは自明だからではなくて、研究の方向性がどう転ぶかわからないからだと思う。
表示的意味論も出た当時の文献では副作用について語ってることが多い。
現代的な本になるほどD∞モデルつくってはいおしまいで数学的にきれいなところしかやらない。
435(1): 2024/10/02(水)23:36 ID:JUMm5MLB(2/2) AAS
プログラムの仕様とその証明を数学で記述する本にあるだろうね。
436(1): 2024/10/02(水)23:37 ID:YWEZQEUD(6/7) AAS
どこが非自明なのかさっぱりわからん
代入と違って入出力は垂れ流しだし、入出力は代入の特別な場合だろ
437: 2024/10/02(水)23:46 ID:OPLMo7z3(8/8) AAS
>>435
ホーア論理とか公理的意味論か。いやそれはないな。あっても一般に適用できないし。
>>436
関数型プログラミングだとプログラムをλ式に対応させて、プログラムの実行をそのλ式の簡約に
対応させるというのが理想的なモデルとして想定されることが多いと思う。
でもλ式はλ項からλ項への対応でしかないから、λ項を値(value)と呼ぶとすると
value から valueへの数学的関数でしかない。これには入出力とかの副作用を表現する余地がない。
つまり、
入出力があるプログラム→value から valueへの数学的関数
という対応付けをすると、入出力という特徴が数学世界では失われてしまう。
省1
438: 2024/10/02(水)23:54 ID:YWEZQEUD(7/7) AAS
代入が書けるんだから、入出力なんて自明だろ…
こいつ何いってんだ…
439: 2024/10/03(木)00:02 ID:B2Xmf+Xl(1/9) AAS
だから、入出力がある数学的関数なんてないだろって言ってんの。
数学的関数で入出力は非自明だと思うんだが。
440: 2024/10/03(木)00:09 ID:B2Xmf+Xl(2/9) AAS
Haskellでいうと、
純粋関数は、λ式（valueからvalueへの数学的関数）
に対応付けられるけど、
IOモナド使ったプログラムは、その現実のプログラムが持つ特徴を表現できるλ式がないので対応付けられない
って言ってんの。
441: 2024/10/03(木)00:21 ID:omgk7HiD(1) AAS
入出力なんてただの値のリストだろ…
442: 2024/10/03(木)03:50 ID:KCHr29fD(1) AAS
圏論持ち出して愚にもつかないことをグダグダと…
それで何か効率良くなるならいいんだけど，何のメリットもないんだよね
443: 2024/10/03(木)04:21 ID:zyXzLypu(1/6) AAS
圏論なんかより、遅延評価ならIOがwhnfの先頭に出てきたら実行すればいいって人類が気づいたのが本質なんじゃねーの
444: 2024/10/03(木)08:29 ID:LNI2TnSo(1) AAS
最近の人類はseqのメリットを直接的に利用するコツに気づいとるんか
順調に進化しとるな
445: 2024/10/03(木)14:31 ID:1wv2Oz28(1) AAS
コンパクトな言語仕様だが表現力は強力
数学をプログラミングに取り入れるメリットってまぁこんなもんでしかないでしょ
一方で静的に性質を決定しようとするやり方は一般的な人間の能力を簡単に超えてしまう
446: 2024/10/03(木)16:46 ID:TkNlnb1D(1) AAS
急にポエマーだらけw
上下前次1-新書関写板覧索設栞歴
あと 221 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.018s