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