haskell-jp / mokumoku-online #88

S.K.です。遅くなってしまいましたが、今週もお世話になります。よろしくお願いいたします。
「Implementing Functional Languages: a tutorial」のやり残した部分の続きを進めようと思います。

山本悠滋です。例の如く昼寝が長引いて遅くなってしまいましたが、引き続き github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます

終わります！

意外に苦戦したのと別件が入って読了できず:melting_face:
圏同値の定義あたりまで読みました

今回読んだ話ではないですが、6章の
ER図風のグラフから作った自由圏から、
集合の圏Setsへの関手がデータベースの実態である
みたいな話がなんとなくイメージできたつもりになれて心地よかったです

進捗ゼロなんでもうちょっと頑張ります

Project Euler #144 Laser Beam Reflections 解けた 　楕円内部で反射の航跡を求めるのがカギ
後半で Lean4 のこの章の出だしはなじみ深いプログラムの諸作法の事だったのでサクサク進むが　なんか途中で証明に関する事で次第に難しくなり　寝落ちしてしまった　後日再挑戦また読み直します　今日の結論： Lean4 は熟睡できるので身体に良い

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
depthFirstSearch 関数の処理対象となるグラフは、テキストのサンプルを見ると循環があるものも受け付けるようなので、グラフに循環があった場合にも矛盾しないような、トポロジカルにソートされた列の条件を検討中です。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。

相変わらずSharedWorkerがうまく動いていないように見える問題が直ってませんでした :disappointed:
デバッグコードを少し増やして終わり。

前半は Project Euler を Haskell で解いて　後半は Lean の 9. Next Steps をヤリます　何はともあれ最終章です

S.K.です。遅くなってしまいましたが、今週もお世話になります。よろしくお願いいたします。
「Implementing Functional Languages: a tutorial」のやり残した部分の続きを進めようと思います。

山本悠滋です。例の如く昼寝が長引いて遅くなってしまいましたが、引き続き github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます

前回 https://haskell-jp.slack.com/archives/CUPBC8WCE/p1786274378078779?thread_ts=1786270566.847309&cid=CUPBC8WCE で計画したとおり MessageChannel を使う実装に変えてみましたが、よーく考えたらそれ以前の 、Shared Workerに対する connect イベントが発火していない問題だったので全然意味がありませんでした :expressionless:

Project Euler #145 Reversible Numbers 解けた　ただし場合分けが多く煩雑　愚問と思う
後半の Lean4 でこの章は次に読むべき文献の紹介だけだった　次週から何をしようか考えたが　ここは igrep さんご推薦の The Hitchhiker's Guide to Logical Verification (2025 edition) の一択あるのみ　ここから今まで Lean で積み残した疑問やら　ついに得られなかった修得感を　今度こそ取り戻すべくやり直したい

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
depthFirstSearch 関数の処理対象となるグラフに循環があった場合にも矛盾しないような、「トポロジカルにソートされた列」の条件を設定してみました。
また、頂点集合 V の定義についても、テキストのままだと本来の意図と異なりそうなので、思い切って正しいと思われる定義に変更して証明を進めることにしました。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。

あ、あとそう言えばMDNの MessageChannelについてのページをついでに一部修正しました。
github.com/mdn/translated-content/pull/37811

前半は Project Euler を Haskell で解いて　後半は the Hitchhiker's Guide to Logical Verification (2025 edition) の Chapter 1 Types and Terms をヤリます

山本悠滋です。引き続き github.com/haskell-jp/makeMistakesToLearnHaskell/issues/121 に取り組みます。が、今日は用事があるのでちょっとだけ！

S.K.です。遅くなってしまいましたが、今週もお世話になります。よろしくお願いいたします。
「Implementing Functional Languages: a tutorial」のやり残した部分の続きを進めようと思います。

最低限の目標である、buildができたのでこの辺にします。どうやらbuildしたバージョンだとworkerにちゃんとmain threadからのメッセージが届いているらしい...
https://haskell-jp.slack.com/archives/CUPBC8WCE/p1786876037542819?thread_ts=1786871435.831739&cid=CUPBC8WCE

Project Euler #981 The Quaternion Group II　難しい　寝落ちしてしまった
the Hitchhiker's Guide to Logical Verification (2025 edition)　朦朧としたまま 1.2 Terms までとりあえず読む　ここまでは Haskell に酷似

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
先週までに設定した、トポロジカルにソートされた列の条件と頂点集合 V の定義と二つの補題をもとに、主定理(問題文の主張)の証明のスケッチを作成してみました。
その後、二つの補題のうち、上位の補題について証明のスケッチを作成中です。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。