関数型プログラミング言語Haskell Part34 (667ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
468: 2024/10/04(金)19:23 ID:tixO3LDq(1/22) AAS
とりあえず続きを書いてみる。
Haskellでいうところの
純粋関数は、valueからvalueへの数学的関数
入出力プログラムは、valueから（入出力）computationへの対応
に割り当てることで、数学上にプログラミング行為を写し出せそうだ、というところまで書いた。
ただ、やっぱり（入出力）computationって何？とか、valueと形式的にどう違うの？という疑問は拭い去ることができない。
そこでMoggiは、次のようなアイディアを２つ出して（結構ムリヤリに）疑問を解決した。
ただし、ここで入出力プログラム prog は A型の引数を取って（computationの整理をする前は）B型の返り値を返すとする。
469: 2024/10/04(金)19:23 ID:tixO3LDq(2/22) AAS
Moggiのアイディア１
・返り値の型がBのcomputationは、何か型構築子をIOとすると、その型構築子を適用した型 IO B のvalueに対応する。
※Moggiの原理ともいう。
つまり、上で挙げた入出力プログラム prog の型は、具体的に A → IO B になると言っている。
IO B 型の実装で、入出力の予約だか、値のリストだか指示書だか表現はいろいろあるが、そういう機構を実装すれば、
prog :: A → IO B
は参照透過性を保ったまま入出力を行うプログラムになる。
もっと広がりが出そうなcomputation概念なのに、急に狭窄な感じがするアイディアだけれど、
実装と折り合いをつけるという観点からすると仕方ないともいえる。
なお、代数的効果のPlotkinとPowerが批判しているのはこのMoggiのアイディア１である感じがする（あんまわかってない）。
470: 2024/10/04(金)19:24 ID:tixO3LDq(3/22) AAS
Moggiのアイディア２
・入出力プログラム（に対応する数学的概念）は、圏をなすはずだ。
Moggiのアイディア１の段階でもprog :: A → IO Bは参照透過性を保ったまま入出力を行うプログラムになるはずだが、
入出力プログラム同士の合成が考えられていない。入出力プログラム prog1、prog2と開発したら、できるだけ再利用するというのが
現実のプログラミングだと思う。わざわざprog1とprog2の合成として定義できそうなプログラムを得るために、イチイチいちから
開発するということを理論的に要請されるというのは不合理。
純粋関数は、λ式に割り当てられることになって、当然、圏をなすだろうに、
プログラムに割り当てられるものが圏を成さないというのはおかしい。
でも、入出力プログラムはMoggiのアイディア１から、
prog :: A → IO B
という特殊な返り値の型を持っているため単純な合成ができない。
471: 2024/10/04(金)19:29 ID:tixO3LDq(4/22) AAS
Moggiのアイディア１の段階でcomputationの概念というのは解消してしまう。
PlotokinとPowerはそこが不満なんだろうか？
474(1): 2024/10/04(金)20:44 ID:tixO3LDq(5/22) AAS
>>472
だからそれはわかっているって。評価途中では実際の入出力はせず指示書だか値のリストだけ作成して
参照透過性を保証して、参照透過性が要求されなくなったプログラムの最終段階でリストに従って
入出力を実行するような仕組みがあれば、参照透過性を保ったまま入出力はできるという話でしょ。
それを数学的にどう正当化するかという話を書いているんだって。
>>473
水曜日あたりからだからそんな分量ないよ。
476(1): 2024/10/04(金)20:51 ID:tixO3LDq(6/22) AAS
だから、入出力がある数学的関数なんてないじゃん。
入出力があるプログラムを数学的に表現しようと思っても詰むからどうしようって話。
480(1): 2024/10/04(金)21:11 ID:tixO3LDq(7/22) AAS
>>478
なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。
でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？
>>479
よくわかんない。具体的に言うとどういうのある？
481: 2024/10/04(金)21:11 ID:tixO3LDq(8/22) AAS
>>478
なるほどそう考えていたのか。全部λ計算でアセンブルすりゃ数学的に還元できるだろうってわけね。
でもそうだとすると文字列を表示するハードウェアの部分はどう還元するの？
>>479
よくわかんない。具体的に言うとどういうのある？
484(3): 2024/10/04(金)21:28 ID:tixO3LDq(9/22) AAS
λ計算を機械語とかアセンブラと見立てて、λ計算ですべて数学世界を組み立てれば、
入出力がある数学的関数も定義できるだろうから、あえて数学的正当性なんて与えようとする
理由がわからない、ということだろうと思った。
プログラムの部分は全てλ計算で組み立てれば完全に同じものが作れると思っているということ
だけれども、じゃあ文字列をディスプレイに表示するというプログラムの構成要素である
ディスプレイはハードウェア部分だけれども、それはλ計算で組み立てるという範疇にはいるんですか？
入らないなら、なにか数学的概念を持ち出してきてそれに対応付けるということをしないといけないんじゃ
ないですか？
という趣旨のことを書いた。
485: 2024/10/04(金)21:33 ID:tixO3LDq(10/22) AAS
これ読んだらわかるけどMoggi論文の読書感想文。いまさらの。
匿名以外でいまさら突っ込んでくるわけないじゃん。
486: 2024/10/04(金)21:33 ID:tixO3LDq(11/22) AAS
これ読んだらわかるけどMoggi論文の読書感想文。いまさらの。
匿名以外でいまさら突っ込んでくるわけないじゃん。
488: 2024/10/04(金)21:39 ID:tixO3LDq(12/22) AAS
>>484
ディスプレイに表示するまでの概念はよく考えたら既存の例でもなかったわ。
焦って変なこといったスマン。
ちょっと説明を考える。
490(1): 2024/10/04(金)21:48 ID:tixO3LDq(13/22) AAS
λ計算が数学的に正当化されてないというような話はしてなくて、
現実のプログラムをλ計算に反映させようと思っても入出力とか非決定計算の部分は表現しきれない
そのλ計算からはみ出す部分をどう正当化させようかという話。
492(1): 2024/10/04(金)22:03 ID:tixO3LDq(14/22) AAS
>>491
うーん。例えば、数学は集合論上で展開されているから、集合論があればその上で展開される
解析学とか、線形代数学とかいらない、みたいな論法じゃない？
この現象は、解析学でモデル化できるけれども、解析学は集合論上で展開できるから、
そんなモデル化はいらなくていちいち集合論の言葉で書けばいいじゃん的な。
みんなそこに興味あるわけじゃないと思いますよ。
496(1): 2024/10/04(金)22:21 ID:tixO3LDq(15/22) AAS
>>493
ごめんなさい。全然違う。入出力を題材にしているのはあくまで例で別に疑問はないです（実装をちゃんと知っているわけではないですが）。
モナドを導入する動機はMoggi論文読んだ読書感想文なので途中まで書いてますが、圏をなすかどうかです。
498(1): 2024/10/04(金)22:28 ID:tixO3LDq(16/22) AAS
>>494
モナドの原論文（Moggiの論文）の読書感想文を入出力の計算効果を題材に解説してみているんだって。
ブログに書いても今更突っ込むなんて恥ずかしいことができる人はいるわけないので、ここに書いている。
501(1): 2024/10/04(金)22:44 ID:tixO3LDq(17/22) AAS
>>499
はっきりそうは言ってない。
プログラムをλ項に対応させて単純化させると、valueからvalueへの全域関数となるけれど、
そう考えると、非停止性とか非決定性、副作用といった現実のプログラムにある特徴が失われる（だからそれを何とかしようと読める）。
>>500
そんなことできるほど力量ないです。
504(1): 2024/10/04(金)22:52 ID:tixO3LDq(18/22) AAS
ただの圏じゃなくてクライスリ圏じゃないといけない（Moggiのアイディア１から）。
そして、クライスリ圏を定義するためにはクライスリ・トリプル（モナド）がいる
505: 2024/10/04(金)22:52 ID:tixO3LDq(19/22) AAS
ただの圏じゃなくてクライスリ圏じゃないといけない（Moggiのアイディア１から）。
そして、クライスリ圏を定義するためにはクライスリ・トリプル（モナド）がいる
509(1): 2024/10/04(金)23:04 ID:tixO3LDq(20/22) AAS
βη簡約するとλ項が別の簡約されたλ項になる。この対応関係を数学的関数とみなせると言ってると解釈してる。
511(1): 2024/10/04(金)23:14 ID:tixO3LDq(21/22) AAS
全域関数となる理由はわからん。全域関数＝数学的関数ということを言いたいんだろうと思ってたけどそこから詰めてなかった。
514: 2024/10/04(金)23:41 ID:tixO3LDq(22/22) AAS
すまんね。準備不足だったわ。詰めるところわかったし、
詰めるところ詰めることができたらひっそりどっかに書くことにするわ。
いろいろコメント参考になったわ。
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.037s