このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

仕様技術への道 -- インスティチューションを縮めてみる

以前のエントリーを振り返って

イデアルと論理」シリーズで、番号がついたエントリー((0)から(5))は、(割り込みの“よしなしごと”があるけど)いちおう番号順に読めるだろうと思う。それ以外に、「ベキ等元」「ベキ零元」「連結性」「コンパクト空間」のエントリーが関連ネタだ(タクソノミーにまとめてありますよ)。

さて、「イデアルと論理 (3)」 に「どこが仕様やねん?! これは仕様です」というタイトルを付けているが、これは「論理なイデアル」という小見出し以下の4段落ほどの文章を強調したいから。僕のなかでは、イデアルも連結性もコンパクト空間も論理/モデル論のための道具だ。そして、論理/モデル論は仕様技術のための道具なのだ。

以上に述べた気分/気持ちは、「論理(学)と仕様」という短いエントリーでも表明している、このエントリーに出てくる用語「含意<がんい>」「伴意<ばんい>」については、次の2つの(やっぱり短い)エントリーで触れている。

インスティチューション

論理/モデル論をベースとした仕様技術といえば、現状利用できる最も便利な枠組みはインスティチューション(Institution)だろう。以下に、キマイラ・サイトの記事からインスティチューションに関する注釈を引用する:

インスティチューションは、(僕は読んでないけど)Joseph Goguen & Rod Burstall "Institutions: Abstract model theory for specification and programming" (1992) で導入された概念。Goguen自身による紹介institutionsがある。

どうでもいいことだが、Goguen先生の奥様(Ryoko Goguen)は日本人らしい。The Tatami ProjectのTatamiは「畳」なのか? 2003年来日のときのご夫妻の写真がココにあります。

[追記]
いま、上のリンクを念のためたどってみたのだけど:
> Joseph Goguen氏による講義
うん、これはいいですが、
> Ryoko Goguen<し>による生演奏
こっ、これはまずいだろう、これは! 不吉なtypo直せ!! >慶応の人
typoは直っています。 [/追記]

インスティチューション(抽象モデル論)は、なかなかよくできている概念だが、具体的な場面では、もとの定義では不十分なことも多い。だから、インスティチューションのいろいろな拡張や変形があってもいいと思う。

コンパクト空間と論理/モデル論」で述べたことは、インスティチューションの変形を意識している。インスティチューションのモデル圏ModΣは一般に(集合論的に)大きいが、ModΣから作った空間XΣは(集合論的に)小さいし、コンパクト空間でもある。論理式(文)の集合Senも、X上の関数と考えると同値関係で割り算するから小さくなる。つまり、空間Xと連続関数の環C(X, {0, 1})を作ると、インスティチューションをminifyできる。largeよりminiのほうが扱いやすい。

矛盾も抱擁する論理

もうひとつ、XとC(X, {0, 1})を考える動機は、論理を一般化したいから。通常、論理的な体系は矛盾がなくて一貫性(整合性)を持つことが要求される。だが、現実に、矛盾がないとか一貫しているなんてことはとても保証できない。だから僕は、矛盾有り/一貫性無しの体系でもいいだろうと思っている。ただし、そのような体系を矛盾無く一貫性をもって記述したい。これは、できるだろうとふんでいる。

小さな範囲では論理的推論がうまくいく。範囲を広くすると整合性を維持するのが難しい。つまり、局所的に矛盾のない(小さな)セオリーは容易につくれるけど、大域的になるほど矛盾を避けるのが難しくなる。幾何学では、局所的な関数はいくらでもあるのに、大域的関数は存在し得ない空間(多様体)がよく出てくる。小さな関数断片を大域的に繋ぎ合わせるのが難しいからだ。

通常の論理体系は局所的体系である。複数の局所論理(local logics)をうまく貼り合わせて繋げるかどうかが問題になる。うまくいくなら大域論理(global logic)ができる(が、たぶんうまくいかないケースが多いだろう)。「局所、大域、貼り合わせ」という話題なら、空間概念を使うのが一番だ。幾何学で扱う対象は、たいてい環付き空間(ringed space)になるが、古典論理に限定すれば、論理的対象は標数2の体を基礎体とする環付き空間と思える。非古典論理まで一般化するとしても、適当な代数系(環じゃないかもしれない)が付いた空間としてlogical varietyが定義できそうだ。

日常の素朴な推論とかも含めて、この世には小さな(大きいのもあるけど)論理系が無闇とたくさんあるだろう。それらはそれぞれにモデルの世界を持つ。「矛盾する」とか「妥当性がある」とかは、実はモデルに対して相対的なもんだ(純構文的な概念もあるにはあるが)。とあるモデルで矛盾(正確には非妥当)しても別なモデルでは矛盾しないかもしれない。2つの論理系が矛盾するとは、その2つを貼り合わせてより大きな体系が作れないことだ -- そんなことは全然珍しくない。ようするに、矛盾や一貫性も、ひどく相対的な概念なのだ。

矛盾の発生や一貫性の崩壊などの、よくある論理的現象(logical phenomena)が扱えないような体系では、仕様記述には使いものにならない気がするのだけど、まーそれは僕の偏見かも知れない。偏見であれどうであれ、僕としては、小さな論理系が無闇とたくさんあるような状況でもナニゴトかは言えるような、大域的枠組みが欲しいのだよね。で、インスティチューションをminifyしてみると、少しは何かが分かりそうだと思っている。