ここでは,半順序集合 (Partial order),前順序集合 (Preorder/Quasiorder), 束 (Lattices) などの 理論を計算機科学で扱った文献で,私が読もう/読まなければならないと 思っているものをリストアップしておく.所謂,「積読」ですね.読んだものも 載せているかもしれない.当面,分類もあまりされていないと思う.文献へのリンクは 特に張らない.興味があれば,タイトルと著者で探してほしい.
一応,言葉でも説明しておきます(図に書いてあることを自然語にするだけですが).
最初に19世紀からのクロージャーの歴史が章があります.これはすでにある程度内容を 知ってないと読めません.著者も,予備知識が無い人は次の章を読んでからこちらに戻ってくれ と書いています.
次は集合論的な閉包操作と古典的な設定でのクロージャーシステムの話があります. クロージャーの基礎的な知識がここで示されます.
次は順序集合的な設定でのクロージャーの理論です.クロージャー操作(閉包操作)と ガロア接続,随伴(Adjunctions)の相互関係が説明されます.随伴(Adjunction)は 次の章でも説明される圏論の概念です.実は順序集合は圏と見ることができます. ガロア接続は順序集合を圏としてみたときの随伴の関係になっています.
最後に,クロージャーを圏の立場から見たときの話があります.ここでは拡張された 束論的な設定で完備なクロージャーのなす代数について説明があります. このような見方をすることにより,古典的な問題はより透明に,澄んだ見通しが可能になり よりエレガントな解法が可能になります.
この著者はイラストが上手で漫画っぽい挿絵がところどころあります.
Galculator は Galois 接続を利用して任意のドメインでの証明を導出するツールだそうです. これと,Point free transform および Indirect equality principle を組み合わせれば,プログラム検証の複雑な証明に対する強力で汎用的な道具になるということです.この論文ではガロア接続の性質から導出された書き換え規則を Haskell で書いた Strategic rewriting system のプロトタイプに入れることで証明を生成することができることを示します.また,この論文では, Galculator とそのほかの証明支援システム,例えば,Coq と統合する展望を議論します.
ソフトウェアの意味論に関係していて,ガロア接続を活用してソフトウェアの検証などを行う技術です.
Let's Study Lattice Theory (Japanese)