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