日々の流転

λ. A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments

A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments by Joseph A. Goguen and R. M. Burstall

To ease constructing institutions, and to clarify various notions, this paper introduces two further concepts. A charter consists of an adjunction, a “base” functor, and a “ground” object; we show that “chartering” is a convenient way to “found” institutions. Parchments provide a notion of sentential syntax, and a simple way to “write” charters and thus get institutions. Parchments capture the insight that the syntax of logic is an initial algebra. Everything is illustrated with the many-sorted equational institution. Parchments also explicate the sense of finitude that is appropriate for specifications. Finally, we introduce generalized institutions, which generalize both institutions and Mayoh's “galleries”, and we introduce corresponding generalized charters and parchments.

昔、向井先生にハードコピーを貰ったまま積読になっていた論文。 institutionの幾つかの定義と、典型的な場合についてinstitutionを作るためのcharterとparchmentという枠組みについての紹介。

institutionの定義に関しては通常の定義に加えて、以下の三つ組みによる定義があって、これ何で自分でこれ気づけなかったのかと思った。そして、この定義から一般化することで generalized institution が得られる。

• 関手 Mod : Sign^op → Cat
• 関手 Sen : Sign → Cat
• 対角自然変換 ⊧ : |Mod(_)|×Sen(_) → 2

charter は随伴から insitution を定義するためのもので、図で書くとこんな感じのもの。

ここで Syn は syntactic system で、「文」だけでなく他の構文的な要素も含むような圏で、Bはそのなかから「文」の成分だけを取り出してくるような関手。こうしておいて Sen を BF で定義する。G は syntactic system の全ての解釈を集めてきたようなもの。 ただ、equational charter での G の定義はサイズの問題が無いのかちょっと不安。

parchment は、自由代数を使うことにして随伴になることを自動的に保障するもの。 関手 Lang : Sign → SigAlg を用意しておいて、Syn は Lang(Σ)代数の圏をΣに関してつぶして作る。

あと、個人的には「The original motivation for developing institutions was to do the “Clear tricks” once and for all, over any (suitable) logical system」と書いてあって、institutionのそもそもの動機が分かってスッキリした。ここで言っている“Clear tricks”というのは代数的仕様記述言語Clearで使われている以下のような手法のこと。

• use colimits to put theories together
• use diagrams as environments to keep track of shared subtheories
• use data constraints to define particular structures (i.e., abstract data types)
• use pushouts to apply generic theories to their “actual” arguments, and
• use theory morphisms to describe the bindings of actuals at interface theories (also called “requirement” theories).