haskell-jp / mokumoku-online #85 at 2026-05-24 18:46:34 +0900

「Mark 6: Dependency analysisy」の Ex.6.13 (「(グラフの)同じ強連結成分内」という関係が頂点集合を同値類に分割することの(非形式的な)証明)を何とか済ませた後、Ex.6.14 (depthFirstSearch 関数の性質に関する(非形式的な)証明)にとりかかろうとしています。(その前に「プログラミング Haskell 第2版」の「第16章 プログラムの論証」を読んでおいた方がいいかもしれません。)

間違えてるかもしれませんが、Ex.6.13 の解答案を貼付させていただきます。
証明のうち、同値類に分割する部分については、以下の資料を参考にさせていただきました。
https://www.math.is.tohoku.ac.jp/~obata/student/subject/file/2018-5_douchi.pdf