関数型プログラミング言語Haskell Part34 (667ﾚｽ)
上下前次1-新
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
447: 2024/10/03(木)19:56 ID:B2Xmf+Xl(3/9) AAS
入出力があるプログラムをどう数学的に整合する概念に対応させるかについて書いてみる。
こういう説明が通るものなのか興味があるし。
まず、仮想的なシェルスクリプト風の行番号付き手続き型言語を想定して、
その言語で入出力があるプログラムを定義するとする。
000 procedure prog1(int n) {
001 double res
002 （なにか込み入った計算）
....
020 echo "hogehoge"
021 （なにか込み入った計算）
省9
448: 2024/10/03(木)19:57 ID:B2Xmf+Xl(4/9) AAS
現実のよくあるプログラムとはこういう感じのものだけれども、実行 $(prog1) をしてその結果が返ってくるという現実的に
必要な点だけを考えると、途中の行番号020を評価したとかそういう情報はいらなくて、結局 $(prog1) して
hogehoge
fugafuga
を表示して、複雑な計算の結果 res が返ってくれさえすればいいともいえる。
だったら、数学的に取り扱いがしづらい、式の評価途中で入出力が発生するみたいな部分を取っ払って
000 procedure prog2(int n) {
001 double res
002 （なにか込み入った計算）
....
省12
449: 2024/10/03(木)19:57 ID:B2Xmf+Xl(5/9) AAS
というわけで、入出力があるプログラムというのは、こういう返り値の部分というか評価の最終段階の部分に「入出力の予約情報と返り値の情報がまとめられたもの」だったんだ、と整理しよう。
ただ、こういう「入出力の予約情報と返り値の情報がまとめられたもの」と長い文で表すのはよろしくないので、何か名前を与えた方がいいということで
computationと呼ぶことにする。
そうすると、Haskellでいえば、
純粋関数は、valueからvalueへの数学的関数
に割り当てることができたけれど、
入出力付きのプログラムについては、valueからcomputationへの対応
に割り当てるということが数学的に正当化できそうだ、ということになるわけだ。
450: 2024/10/03(木)20:00 ID:B2Xmf+Xl(6/9) AAS
訂正
computationというか、今でいう「入出力の予約情報と返り値の情報がまとめられたもの」を
数学的にうまく正当化するということが達成することができるのであれば、
入出力つきのプログラムを、valueからcomputationへの対応
に割り当てるということが正当化できるはずだ、と考えられる。
451: 2024/10/03(木)20:23 ID:zyXzLypu(2/6) AAS
何言ってるのか全然わからん
ぶっちゃけ入力は関数の引数にして、出力は返り値にするように変換するだけでいいだろ
読み出し位置のカーソル管理が必要なら代入を使えばできるじゃん
452: 2024/10/03(木)20:39 ID:B2Xmf+Xl(7/9) AAS
よくわかんないけど、そういう入出力プログラムがあったとする。
そしてそれを引数付きで実行することを考えると
$(prog n)
こうなる。ここで、引数の部分の n はプログラムの記述に属さないといけない。
なぜかというと現実世界の「入力」部分をそのまま引数のところには持ってこれないから。
引数部分を入力にするにしても、別途入力されたものをプログラムの変数に割り当てる概念
みたいなのが必要になるし、それは関数の引数だからということでは説明にならないと思う。
だから、少なくともprogの引数部分はvalueじゃないといけない。
453: 2024/10/03(木)20:45 ID:zyXzLypu(3/6) AAS
ポエムすぎて意味わからん。値のリストはvalueじゃないと？
454: 2024/10/03(木)20:59 ID:B2Xmf+Xl(8/9) AAS
値のリスト自体をそのまま持ってくればvalueということになるんだろうけれど、
$(prog n)
の実行結果として出てくるもので、計算効果の説明になるものであって、返り値の型を包含するもの
であればcomputationと判断せざるを得ないとかそういうことしか言えないです。
455: 2024/10/03(木)21:11 ID:zyXzLypu(4/6) AAS
判断するって何言ってるの？
computationって定義は何なの？
ラムダ項を書き換えていく手続きが計算じゃないの？
456: 2024/10/03(木)21:22 ID:B2Xmf+Xl(9/9) AAS
valueとcomputationの違いは微妙で$(prog n)の実行結果として出てくるかどうかとか
計算効果が発露しているかというところで見極めるしかない、と理解している。判断する
というのは専門用語としては使ってない。
computationの定義はまた微妙だけれど、$(prog n)の計算効果込みの実行結果みたいな概念。
最後は超個人的見解だけど、「λ項を書き換えていく行為」というのは、どういう方法で表現して
どういう方法で簡約していくか？というところが決まってない。λ計算じゃないけれど、
１＋１＝２
という計算を暗算でやるか、電卓でやるか、そろばんでやるかという違いを出しても計算することに
変わりない。
暗算でやると、脳内物質の分量が変わるし、電卓だと電位が変わる。そして、そろばんでやると
省1
457: 2024/10/03(木)21:30 ID:zyXzLypu(5/6) AAS
❌決まってない
⭕知らない
間違えるなよ
458: 2024/10/03(木)21:31 ID:zyXzLypu(6/6) AAS
お前の脳内にしかないお花畑に巻き込むのやめてもらっていいですか？
459: 2024/10/03(木)22:10 ID:/brOvmjG(1) AAS
おそらくメンタルヘルスに問題がある方なのかな？
自分の頭の中の映像をそのまま言葉にしたような感じを受ける
460(2): 2024/10/04(金)05:46 ID:vLDssEdm(1/9) AAS
>>428
Haskellの副作用については2つの解釈がある。
１．副作用も含めてアクションという単位で値としてみる。
（アクションを受け取って、アクションを返す関数）
２．Haskellは指示書を発行しているだけで、実際に実行するのは数学（Hakell）の外だから、Haskellそのものには副作用が無い。
（（末尾にHaskellに値を返す形の）マシン語を返して、ハードウェアに実行してもらうと考えるアウトソーシング方式）
461(1): 2024/10/04(金)05:52 ID:EogKDI3R(1/3) AAS
>>460
ようするに副作用はないってことじゃん
上下前次1-新書関写板覧索設栞歴
あと 206 ﾚｽあります
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.025s