関数型プログラミング言語Haskell Part34 (692ﾚｽ)
上下前次1-新
431: デフォルトの名無しさん [sage] 2024/10/02(水) 23:02:49.62 ID:YWEZQEUD(4/7) AAS
どれにでも書いてあるだろ、whileプログラムをラムダ計算に変換する手順とか書いてないなんてことがあるわけがない
432: デフォルトの名無しさん [] 2024/10/02(水) 23:06:08.21 ID:OPLMo7z3(6/8) AAS
なんだ。いや聞きたいのは入出力とかの副作用だよ。
433: デフォルトの名無しさん [sage] 2024/10/02(水) 23:17:44.98 ID:YWEZQEUD(5/7) AAS
入出力なんて代入に比べたら自明だろ…
そんなのいちいち教科書に書くかよ
434: デフォルトの名無しさん [] 2024/10/02(水) 23:26:30.50 ID:OPLMo7z3(7/8) AAS
書いてないのは自明だからではなくて、研究の方向性がどう転ぶかわからないからだと思う。
表示的意味論も出た当時の文献では副作用について語ってることが多い。
現代的な本になるほどD∞モデルつくってはいおしまいで数学的にきれいなところしかやらない。
435(1): デフォルトの名無しさん [sage] 2024/10/02(水) 23:36:01.67 ID:JUMm5MLB(2/2) AAS
プログラムの仕様とその証明を数学で記述する本にあるだろうね。
436(1): デフォルトの名無しさん [sage] 2024/10/02(水) 23:37:10.87 ID:YWEZQEUD(6/7) AAS
どこが非自明なのかさっぱりわからん
代入と違って入出力は垂れ流しだし、入出力は代入の特別な場合だろ
437: デフォルトの名無しさん [] 2024/10/02(水) 23:46:11.64 ID:OPLMo7z3(8/8) AAS
>>435
ホーア論理とか公理的意味論か。いやそれはないな。あっても一般に適用できないし。
>>436
関数型プログラミングだとプログラムをλ式に対応させて、プログラムの実行をそのλ式の簡約に
対応させるというのが理想的なモデルとして想定されることが多いと思う。
でもλ式はλ項からλ項への対応でしかないから、λ項を値(value)と呼ぶとすると
value から valueへの数学的関数でしかない。これには入出力とかの副作用を表現する余地がない。
つまり、
入出力があるプログラム→value から valueへの数学的関数
という対応付けをすると、入出力という特徴が数学世界では失われてしまう。
という難問があった、けどモナドで一つ解答が出た。
438: デフォルトの名無しさん [sage] 2024/10/02(水) 23:54:51.93 ID:YWEZQEUD(7/7) AAS
代入が書けるんだから、入出力なんて自明だろ…
こいつ何いってんだ…
439: デフォルトの名無しさん [] 2024/10/03(木) 00:02:36.12 ID:B2Xmf+Xl(1/9) AAS
だから、入出力がある数学的関数なんてないだろって言ってんの。
数学的関数で入出力は非自明だと思うんだが。
440: デフォルトの名無しさん [] 2024/10/03(木) 00:09:13.65 ID:B2Xmf+Xl(2/9) AAS
Haskellでいうと、
純粋関数は、λ式（valueからvalueへの数学的関数）
に対応付けられるけど、
IOモナド使ったプログラムは、その現実のプログラムが持つ特徴を表現できるλ式がないので対応付けられない
って言ってんの。
441: デフォルトの名無しさん [sage] 2024/10/03(木) 00:21:32.37 ID:omgk7HiD(1) AAS
入出力なんてただの値のリストだろ…
442: デフォルトの名無しさん [sage] 2024/10/03(木) 03:50:19.64 ID:KCHr29fD(1) AAS
圏論持ち出して愚にもつかないことをグダグダと…
それで何か効率良くなるならいいんだけど，何のメリットもないんだよね
443: デフォルトの名無しさん [sage] 2024/10/03(木) 04:21:38.74 ID:zyXzLypu(1/6) AAS
圏論なんかより、遅延評価ならIOがwhnfの先頭に出てきたら実行すればいいって人類が気づいたのが本質なんじゃねーの
444: デフォルトの名無しさん [sage] 2024/10/03(木) 08:29:58.17 ID:LNI2TnSo(1) AAS
最近の人類はseqのメリットを直接的に利用するコツに気づいとるんか
順調に進化しとるな
445: デフォルトの名無しさん [sage] 2024/10/03(木) 14:31:37.97 ID:1wv2Oz28(1) AAS
コンパクトな言語仕様だが表現力は強力
数学をプログラミングに取り入れるメリットってまぁこんなもんでしかないでしょ
一方で静的に性質を決定しようとするやり方は一般的な人間の能力を簡単に超えてしまう
446: デフォルトの名無しさん [sage] 2024/10/03(木) 16:46:40.39 ID:TkNlnb1D(1) AAS
急にポエマーだらけw
447: デフォルトの名無しさん [] 2024/10/03(木) 19:56:29.70 ID:B2Xmf+Xl(3/9) AAS
入出力があるプログラムをどう数学的に整合する概念に対応させるかについて書いてみる。
こういう説明が通るものなのか興味があるし。
まず、仮想的なシェルスクリプト風の行番号付き手続き型言語を想定して、
その言語で入出力があるプログラムを定義するとする。
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 を返す、という動作をする。
448: デフォルトの名無しさん [] 2024/10/03(木) 19:57:08.78 ID:B2Xmf+Xl(4/9) AAS
現実のよくあるプログラムとはこういう感じのものだけれども、実行 $(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 が返ってくるということは変わらない。
449: デフォルトの名無しさん [] 2024/10/03(木) 19:57:34.71 ID:B2Xmf+Xl(5/9) AAS
というわけで、入出力があるプログラムというのは、こういう返り値の部分というか評価の最終段階の部分に「入出力の予約情報と返り値の情報がまとめられたもの」だったんだ、と整理しよう。
ただ、こういう「入出力の予約情報と返り値の情報がまとめられたもの」と長い文で表すのはよろしくないので、何か名前を与えた方がいいということで
computationと呼ぶことにする。
そうすると、Haskellでいえば、
純粋関数は、valueからvalueへの数学的関数
に割り当てることができたけれど、
入出力付きのプログラムについては、valueからcomputationへの対応
に割り当てるということが数学的に正当化できそうだ、ということになるわけだ。
450: デフォルトの名無しさん [] 2024/10/03(木) 20:00:39.07 ID:B2Xmf+Xl(6/9) AAS
訂正
computationというか、今でいう「入出力の予約情報と返り値の情報がまとめられたもの」を
数学的にうまく正当化するということが達成することができるのであれば、
入出力つきのプログラムを、valueからcomputationへの対応
に割り当てるということが正当化できるはずだ、と考えられる。
451: デフォルトの名無しさん [sage] 2024/10/03(木) 20:23:28.46 ID:zyXzLypu(2/6) AAS
何言ってるのか全然わからん
ぶっちゃけ入力は関数の引数にして、出力は返り値にするように変換するだけでいいだろ
読み出し位置のカーソル管理が必要なら代入を使えばできるじゃん
452: デフォルトの名無しさん [] 2024/10/03(木) 20:39:38.40 ID:B2Xmf+Xl(7/9) AAS
よくわかんないけど、そういう入出力プログラムがあったとする。
そしてそれを引数付きで実行することを考えると
$(prog n)
こうなる。ここで、引数の部分の n はプログラムの記述に属さないといけない。
なぜかというと現実世界の「入力」部分をそのまま引数のところには持ってこれないから。
引数部分を入力にするにしても、別途入力されたものをプログラムの変数に割り当てる概念
みたいなのが必要になるし、それは関数の引数だからということでは説明にならないと思う。
だから、少なくともprogの引数部分はvalueじゃないといけない。
453: デフォルトの名無しさん [sage] 2024/10/03(木) 20:45:47.19 ID:zyXzLypu(3/6) AAS
ポエムすぎて意味わからん。値のリストはvalueじゃないと？
454: デフォルトの名無しさん [] 2024/10/03(木) 20:59:58.72 ID:B2Xmf+Xl(8/9) AAS
値のリスト自体をそのまま持ってくればvalueということになるんだろうけれど、
$(prog n)
の実行結果として出てくるもので、計算効果の説明になるものであって、返り値の型を包含するもの
であればcomputationと判断せざるを得ないとかそういうことしか言えないです。
455: デフォルトの名無しさん [sage] 2024/10/03(木) 21:11:15.46 ID:zyXzLypu(4/6) AAS
判断するって何言ってるの？
computationって定義は何なの？
ラムダ項を書き換えていく手続きが計算じゃないの？
上下前次1-新書関写板覧索設栞歴
あと 237 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.021s