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 の定義と二つの補題をもとに、主定理(問題文の主張)の証明のスケッチを作成してみました。
その後、二つの補題のうち、上位の補題について証明のスケッチを作成中です。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。

@shibuya has joined the channel

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

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

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

ここまでにします。Wasm版GHCなどが入ったディレクトリーを ビルドした dist ディレクトリーに向けてsymlinkを作れた... はずですがまだうまく行ってない模様でfetchしても404になる。
やっぱりShared Workerのデバッグはしづらい！

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
先週までに設定した、二つの補題のうち、上位の補題について証明のスケッチを一通り作成してみて、怪しそうな箇所や飛躍してそうな箇所を見直し中です。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。

Project Euler #146 Investigating a Prime Pattern　解いた　Miller–Rabin primality test を初めて書いたが 　実はよく分かってない
the Hitchhiker's Guide to Logical Verification (2025 edition)　途中で眠くなるも 2.2 Function Definitions までとりあえず読む　ドーモ　身につかない感じがして　そしたら　AI 勉強法というのがあるそうで　文頭や勘所で AI 先生に聞いて　そのお気持ちやら　展望・発展やら　その意味を解説してもらうそうな　何か唯我独学派には良さそうな気がするではないか　今度試してみよう　おやすみなさい　Zzz..

Verifying Verifying Algorithm は優れた Haskell と Lean4 の比較論考と確信したので　比較研究として Lean4 を堂々と（モクモクと）この場でヤッテも良いのではないかと思う
それで例によって　前半は Project Euler を Haskell で解いて　後半は the Hitchhiker's Guide to Logical Verification (2025 edition) の Chapter 3 Backward Proofs をヤリます

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

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

ビルドしたら onconnect が呼ばれない問題は治っているかのように見えていたが、違ったらしい。あと、Edgeでビルドしたバージョンを開いてみたら、そもそもworkerが起動していないこともわかった。EdgeのDevToolsのNetworkタブを見たらworkerをダウンロードしようとしたところでpendingになってる。相変わらずヒントが少ない。

Project Euler #148 Exploring Pascal's Triangle　実験的に７進数解法を思いつく　理論的には Lukas' Theorem らしい　良問（解けたからこんな事言えるのだが）
The Hitchhiker's Guide to Logical Verification (2025 edition)　途中で眠くなるも 3.3 Reasoning about Connectives and Quantifiers までとりあえず読む　AI 勉強法はまずまずといったところ　"intro ha hb" hypotheses について　冗長だなと思って質問したら『「煩わしい」と感じるのは自然な感覚』との返答をいただいて　安心した
みなさんは　いろいろな AI ChatGPT Claude Gemini 等のどれを使っていますか？　一長一短で「それぞれだなぁ」が率直な感想

今週も「Mark 6: Dependency analysisy」の Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)の続きを進めました。
設定した二つの補題の上位の補題について作成した証明のスケッチを見直した結果、下位の補題の条件定義が不十分で、上位の補題の証明でうまく適用できないことがわかり、下位の補題の条件定義を修正中です。
今週もまだ終わりませんでしたが、またほんの少しは進んだかなという感じです。
自分にとってはまだまだ先は長いですが、可能なペースで進めて行こうと思います。