文献リスト:計算機科学における Posets の利用・扱い(1)

by Akihiko Koga
22nd Dec. 2017 (Updated)
22nd Dec. 2017 (First)

束論を勉強しようへ戻る

ここでは,半順序集合 (Partial order),前順序集合 (Preorder/Quasiorder), 束 (Lattices) などの 理論を計算機科学で扱った文献で,私が読もう/読まなければならないと 思っているものをリストアップしておく.所謂,「積読」ですね.読んだものも 載せているかもしれない.当面,分類もあまりされていないと思う.文献へのリンクは 特に張らない.興味があれば,タイトルと著者で探してほしい.

21st Dec. 2017

    ガロア接続, Closure, 形式概念分析 (Formal Concept Analysis), Abstract Interpretation

  1. Jouni Järvinen, Michiro Kondo, Jari Kortelainen : Logics from Galois connections, 2008, pp595-606

  2. Nathalie Caspard, Bernard Monjardet : The lattices of closure systems, closure operators, and implicational systems on a finite set: a survey, 2003, pp241-269

  3. Erné, M.; Koslowski, J.; Melton, A.; Strecker, G. E : A Primer on Galois Connections, 1992, pp1-22
    これはチュートリアル.探せば Postscript で見つかります.残念ながら,PDF では見たことがありません.

  4. Erné : Closure, 2008, pp163-238
    これもチュートリアル.内容は以下の図の通り,だと思う.目次やら内容やらを 斜め読みして適当につけた表紙です.大きく見るためには図をピックしてください. クロージャーとは,例えば,位相空間で,集合に対してその集積点を加えて 閉集合にするような操作です.大学1年生の「集合と位相」というような教科で ちょっとだけは出てくると思います.これと反対に開集合にする操作をカーネル操作と 言います.どちらにしても,位相が決まればクロージャー操作(カーネル操作)が 決まり,その逆もしかりです.クロージャーの概念は位相空間だけでなく,例えば, 概念集合の階層構造を表現する形式概念分析など,いろいろな領域で使われます.

    一応,言葉でも説明しておきます(図に書いてあることを自然語にするだけですが).

    最初に19世紀からのクロージャーの歴史が章があります.これはすでにある程度内容を 知ってないと読めません.著者も,予備知識が無い人は次の章を読んでからこちらに戻ってくれ と書いています.

    次は集合論的な閉包操作と古典的な設定でのクロージャーシステムの話があります. クロージャーの基礎的な知識がここで示されます.

    次は順序集合的な設定でのクロージャーの理論です.クロージャー操作(閉包操作)と ガロア接続,随伴(Adjunctions)の相互関係が説明されます.随伴(Adjunction)は 次の章でも説明される圏論の概念です.実は順序集合は圏と見ることができます. ガロア接続は順序集合を圏としてみたときの随伴の関係になっています.

    最後に,クロージャーを圏の立場から見たときの話があります.ここでは拡張された 束論的な設定で完備なクロージャーのなす代数について説明があります. このような見方をすることにより,古典的な問題はより透明に,澄んだ見通しが可能になり よりエレガントな解法が可能になります.

    この著者はイラストが上手で漫画っぽい挿絵がところどころあります.

  5. Roland Backhouse : Galois Connections and Fixed Point Calculus, 2001, p105
    これもチュートリアル.上と同じようにガロア接続などのことが書かれています.こちらは かなり計算機よりの話で具体例が沢山書いてあります.

    アブストに書いてある程度の概要ですが,上の図に書いたようにものです.すなわち, 不動点計算 (fixed point calculus) というのは順序集合の自己単調関数 f : P → P の解に関する 理論のことです.ここでは,この理論のチュートリアルとして, を述べます.

  6. David Darais, David Van Horn : Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory, 2016, pp1-14

  7. P.F. Silva and J.N. Oliveira : Report on the Design of a Galculator, 2008(?), 16p

    Galculator は Galois 接続を利用して任意のドメインでの証明を導出するツールだそうです. これと,Point free transform および Indirect equality principle を組み合わせれば,プログラム検証の複雑な証明に対する強力で汎用的な道具になるということです.この論文ではガロア接続の性質から導出された書き換え規則を Haskell で書いた Strategic rewriting system のプロトタイプに入れることで証明を生成することができることを示します.また,この論文では, Galculator とそのほかの証明支援システム,例えば,Coq と統合する展望を議論します.

  8. Gregor Snelting : Concept Lattices in Software Analysis, 2005, pp 272-287

  9. R. Al-msie'deen, M. Huchard, A.-D Seriai : Concept lattices: A representation space to structure software variability, 2014, p6
    ソフトウェアの可変性を表現する概念束だそうです.ソフトウェアの可変性とは,例えば, 似たソフトウェアをたくさん作らないといけないとき,その一部をパラメータ化して, そこだけを変更することにより,それらのソフトウェアを作るようなことを意味します. 短い論文です.

  10. 鈴木 治, 室伏 俊明 : 形式概念分析 : 入門・支援ソフト・応用, 2007, pp103-142
    解説です.貴重な日本語の解説.

    ----- Abstract Interpretation -----

    ソフトウェアの意味論に関係していて,ガロア接続を活用してソフトウェアの検証などを行う技術です.

  11. A Salcianu : Notes on Abstract Interpretation, 2001, pp1-14

  12. Maria Jenkins, Leif Andersen, Thomas Gilray, Matthew : Concrete and Abstract Interpretation: Better Together, 2014, p10

    オートマトン,言語理論

  13. David Lee, Mihalis Yannakakis : Closed Partition Lattice and Machine Decomposition, 2010, pp1-31

  14. Orna Kupferman, Yoad Lustig : Lattice Automata, 2007, pp1-24
    A = A* ∪ Aω の文字列を命題と考えて,それを 入力として状態遷移を行い,命題の真偽値として束の値を割り当てるオートマトンです. Semiring あるいは重み付きオートマトンの方法より,図の下に書いてある性質についてより 強い結果が得られると書いてあります.

  15. M. Ćirić, S. Bogdanović, T. Petković : THE LATTICE OF SUBAUTOMATA OF AN AUTOMATON: A SURVEY, 1998, pp165-182

  16. Alexander Clark : Learning Context Free Grammars with the. Syntactic Concept Lattice, 2010, p14
    Syntactic Concept Lattice というのは形式言語の分配法則性に基づいた Residual Lattice のことです.通常,これは Context-sensitive な言語に関係しますが,この論文で著者らは これを図の下半分に書いてあるように言語の要素と対応付けて Context-free 言語に適用します.

  17. Alexander Clark : The syntactic concept lattice: Another algebraic theory of the context-free languages?, 2015, pp1203–1229

  18. M. P. Desai, H. Narayanan, Sachin B. Patkar : The realization of finite state machines by decomposition and the principal lattice of partitions of a submodular function, 2003, pp299-310

    その他計算機への応用

  19. Vijay K. Garg, Neeraj Mittal, Alper Sen : Using Order in Distributed Computing, 2006, p20

  20. Vijay K. Garg, Neeraj Mittal : On Slicing a Distributed Compution, 2001, p8

  21. Viktor Kuncak Ruzica Piskac Philippe Suter : Ordered Sets in the Calculus of Data Structures, 2010, pp 34-48

    基礎的な技術

  22. JD Farley : Chain Decomposition Theorems for Ordered Sets, 1997, p12

  23. P. Jipsen and C. Tsinakis : A Survey of Residuated Lattices, 2002, pp19-56
    上で出てきた residuated lattice のサーベイです.

    Posets, Lattices の描画,生成,数え上げなど

    束や順序集合を実際に目で見える形に表現したり,必要な束を次々に生成したり,いくつあるか数え上げる技術は計算機屋さんにとってはとても興味深く,重要なことですね.タイトルそのままですが.

  24. R Freese : Automated Lattice Drawing, 2004, pp 112-127

  25. Peter Jipsen, Nathan Lawless : Generating all finite modular lattices of a given size, 2015, pp 253–264

  26. D.J. BENSON, J.H. CONWAY : Diagrams for modular lattices, 1985, pp111-116

  27. L Nourine, Olivier Raynaud : A fast algorithm for building lattices, 1999, pp199-204

  28. Joseph Culberson, G. J. E. Rawlins : Counting Posets and the Structure of the Poset of Posets, 1988, pp1-16


Let's Study Lattice Theory (Japanese)

Top of My Homepage (Japanese)