自分で参照する都合で小さなリンク集を作った； 僕の興味はたぶん次のようなキーワードで示せるのでしょう。 メイヤー 「本文」「目次」 ホーア「本文」「目次」 型理論 「本文」「目次」 インスティチューション 「本文」「目次」 シーケント 「本文」「目次」 仕様記述 「本文」「目次」 次の2つの語は一般的過ぎるかも。ヒットが多すぎる。 論理 「本文」「目次」 ラムダ 「本文」「目次」

…れることがあります。インスティチューションでは、指標と指標射からなるベース圏の上にモデル圏が森の木のように“生えた”構造を考えます。メイヤー代数もメイヤー指標で定義可能です。集合圏で考えることにすれば、メイヤー指標は、1つの隠蔽ソート（hidden sort）を持つ隠蔽指標（hidden signature）です。次のものから構成されます。 Commandを表す記号の集合C Queryを表す記号の集合Q、各記号qには値のソートVqが割り当てられている CもQも無限集合でもかま…

…だいぶ違うでしょう。インスティチューション・ベースならCategories-as-Typesと考えるべきかもしれません。とりあえずここでは、Sets-as-Types（型とは集合なり）に限定することにします。「型とはなにか？」を固定してもまだ問題があります。型に関する議論には、プログラミング言語の概念、論理の概念、集合論の概念（Sets-as-Typesのとき）、そして型理論固有の概念が登場します。同じ、またはほとんど同じ概念にたくさんの用語が対応しています。同義語なのか、微…

…性の関数とは関係（relation）と言っても同じです。そして、関数や関係の背後にはSetやRelのような圏があります。圏Setや圏Relと、伴意順序のような順序を一緒に扱えないでしょうか？ そのひとつの候補が順序付き関係の圏ORelです。もちろん、インスティチューションやインデックス付き圏や構文生成モナドなどの他の方法もありますが、ホーアセオリーと順序付きの圏は割と相性が良さそうです。 *1:セオリーは、ホーア論理に特有のものではなくて、論理一般に関して定義できる概念です。

「インスティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。 ホーア論理の圏論的な定式化 真偽構造が付いた圏 -- ホーア論理のために 「インデックス付き圏のフビニ／グロタンディーク同値」では、入れ子になったインデックス付き圏を持ち出しました。入れ子のインデックス付き圏の動機は「大量のモナド類似物（monad-like entities）を一挙に扱う方法」だと書きました。実は、「インスティチュ…

…様技術への道 -- インスティチューションを縮めてみる」とか、「古典論理は可換環論なんだよ」なんかがあります。これらも、マジメに書いてあるみたい。そういえば、「古典論理は可換環論なんだよ」には、「当方記事には過ぎた続編」をtri_iroさんに書いていただきました。「イデアルと論理 番外の補足：ベキ等元と連結性」と「“古典論理＝可換環論”の計算と種明かし」も関連記事です。以上に挙げた記事は、「論理は位相や代数とも関係するんだぜー」みたいなハナシ。そして、「論理も位相も代数も計算…

…な定式化」において、インスティチューションとホーア論理を一緒にしたようなナニカができないかなぁ、とか言ったので、もう少し考えてみることにします。ただし、最初のステップだけで、インスティチューションを使う段階には至ってません。僕がやりたいことは、「拡張されたホーア論理」の意味論を構成することですが、とりあえず意味論の舞台となる構造を作ることにします。真偽値という概念を圏論的に扱いやすい形にしたモノです。内容： 圏の上に真偽値を乗せる 真偽構造のあいだの準同型 具体的な真偽構造付…

…ーバーライドなしの）継承 MethodS→MethodT となっています。それから以上の定式化は、状態空間とメソッドのモデルとしては直接的・直感的なものだと思います。多くの現実の実装が採用している方式と同じで、メソッドはthisとかselfとかの暗黙の引数を持つことにより実現されます。大域関数はthisの値がvoidであるメソッドとみなされます。この定式化と、インスティチューション、ホーアトリプル、余代数などの関係を考えてみると面白いかも（あるいは面白くないかも）しれません。

インスティチューションは重要だと思っているのですが、このブログでまとまった記述をしたことはありません。じゃ、まとまったものを書くのか -- 書きません(苦笑)。まとまりのない断片的なことを書きます。インスティチューションはインデックス付き圏です。ベースの圏（インデックスの圏）は指標圏（category of signatures）と呼ばれ、標準的な記法では Sig と書きます。指標 Σ∈|Sig| ごとにモデル圏 Mod[Σ] が対応して、Σ |→ Mod[Σ] がインデック…

インスティチューションは、さまざまな型理論を統一的に扱うための便利な枠組みになります。与えられたインスティチューションをインデックス付き圏（indexed category）とみなして、グロタンディーク構成を行うことは有効なテクニックです。このテクニックの簡単な応用例を紹介します。この方法は、オブジェクト指向のクラス、抽象クラス、インターフェースなどを全部ひっくるめた型階層（type hierarchy）を作りたいときなどに使えます。Σを指標だとして、M[Σ]をモデル圏としま…

…インデックス付き圏 インスティチューション 仕様構造圏C上の仕様構造の定義は簡単です。 圏Cの対象Aごとに P(A) という集合が対応している。 圏Cの対象A, Bごとに P(A)×C(A, B)×P(B) の部分集合 H(A, B) が対応している。 P(A)は、A上のプロパティ（properties over A）の集合と呼びます。H(A, B) はホーアトリプルの集合と呼びましょう。P(-) と H(-, -) に関して次の条件を要求します。 (p, idA, p)∈H…

…ットに他ならない。 インスティチューション理論では、指標をΣと書く習慣がある。基本オペレーションの集合は指標と解釈できる。 実例を出しましょう。単純な整数変数をオブジェクトに仕立てたものをvとします。vは整数値を蓄えることができるのでストレージです。ただしvは、値がバインドされてない状態と、壊れてしまった状態を持つとします。vへの値の代入には、v.set(2) のようなsetメソッドを使い、値を未定義にするには v.unset() とします。vを壊す操作は v.destroy…

…い枠組みは？ そりゃインスティチューションでしょう。 圏論とオブジェクト指向 圏論とオブジェクト指向：資料編 自己改変コードについてはたまに考えてみるんですが、よくワカリマセン。状態空間が変化していく状況をモデル化したいなら、クリーネ圏を使えばよさそうなんですが …不純な計算や概念、多くの人が避けたり嫌ったりする計算や概念は魅力的。ただのへそ曲がりかもしんないけど、面白いんだからしょうがない。 *1:[追記]これは日本語が不正確。ほぼ書き間違っていますね。goto文を継続で解…

…category）、インスティチューション（institution）、ファイバー圏（fibred/fibered category）あたり。ステファネスク師のデカルト半環圏（Cartesian Semiringal Category）も、古典圏論の範囲では扱いがたいシロモノです。それで、何日か前からインデックス付き圏の話をはじめたのですが、毎度のことながら、定訳のない用語をどう表記するかで悩んでいます。古典圏を超える概念を扱うので、「超」とか「モドキ」の意味を持つ形容詞・副詞…

…のなかで、図式の例とインスティチューションの例は、具体例とは言いながら完全に圏を1つ固定した話ではなくて、圏の類を話題にしているので後回し。ベクトル空間の例に対してグロタンディーク構成（平坦化）を具体的に作ってみます。以下では、グロタンディーク構成で作った圏を「平坦化（した／された）圏」と呼ぶことにします。正確に言えば、インデックス付き圏（indexed category）のグロタンディーク構成からファイブレーションを忘れた圏（ファイバーバンドルで言えば全空間）が平坦化圏です…

…限倍とは限りません。インスティチューションインスティチューションがあるとして、Signを指標圏、Modをモデル関手とします。σ:Σ→Σ' を指標圏Sign内の射（指標射）だとします。インスティチューションの定義から、指標射σに対応するモデル圏のあいだの関手 σ*:Mod(Σ')→Mod(Σ) が誘導されます。この関手σ*はリダクト関手（reduct functor）と呼ばれるものです。つまり、インスティチューション構造のModは、指標圏Signをベース圏とするインデックス付き…

…とします。この記法はインスティチューションに倣いましたが、インスティチューションは出てきません。「|- A」という書き方のAを変数だと思うと、次の集合Provableが定義でます。 Provable = {A∈Sen(S) | |-S A} 左側がカラッポの「|-」の意味は、Sen(S)の部分集合だと言っていいでしょう。しかし、「A |- B」のような書き方もあります。これは、Aを仮定すればBが証明できる、という相対的証明可能性です。「A |- B」のA, Bを変数だと思うと…

…式化として、現状ではインスティチューションが一番包括的だと思います。ですが、インスティチューションの定義は「圏の圏」（あるいは圏のタバ）の形をしていて、インスティチューションのあいだの準同型を考えると「圏の圏の圏」を扱うことになります。それに、インスティチューションの準同型って概念はあんまりハッキリしてないし。僕の個人的な印象（錯覚や誤解かもしれません）では、インスティチューションは論理の双対性をうまくキャプチャできてない気がします。この感覚は、「当方記事には過ぎた続編、よみ…

…て、代数／余代数とかインスティチューションとかもあるのですが、知名度(?)から言ってモナドかな、結局。と、まーそういうことです。最初は、モナドの具体例を丁寧に紹介するつもりです。僕の感覚では、リストモナドが典型的モナドなので、リストから入るかもしれません。「圏論やモナドが、どうして文書処理やXMLと関係するのですか？」で紹介したテンプレートモナドも具体的で面白いですね。「世界で一番か二番くらいにやさしい「モナド入門」」で扱った大域変数への代入とか、ファイル入出力とか例外とかも…

…することにします。「インスティチューション」という言葉を表だっては出しませんが、僕の気持ちとしては、インスティチューション入門も意図しています。「もっと型理論」の続きみたいな感じかな。内容： 言葉と記法の準備 インターフェースの実例 リネーム 指標射 モデル（＝実装クラス）のリダクト操作 セオリーでプログラマの気持ちを表す もう一回くらいは続くでしょう ●言葉と記法の準備毎度毎度愚痴っていることですが、用語法がいっぱいありすぎてやんなる。おおざっぱな対応表↓ オブジェクト指向…

… 僕がたまに口にするインスティチューションや余代数の説明も、いつかJavaScriptを使ってするかもしれません（無保証言明）。 これの準備のつもりなんですが、それは置いといて、単に「できるだけ小さな言語仕様」ってことなら、いくらでも案はあると思います。「通常のプログラミング言語に類似の構文」という制限も別に意識しなくてもいいでしょう。そういう自由に決めていい「極小プログラミング言語」って、個人の好みや経験や価値観をけっこう反映することになりそうだな。僕自身は、なんだかんだ言…

…れないな（背後にあるインスティチューションが好きなんだろうが）。続き物にする気はなかったのだけど、また型理論の話を少し。昨日のエントリー「もっと型理論」で： "types as specifications/theories"の立場では、サブタイプ／スーパータイプの定義は複雑になります。問題は、サブタイプ／スーパータイプ概念が、extendsだけで尽きているわけではないことです。まだ説明すべきことが残っているのです。 と書いたけど、extendsだけも分かること／説明できるこ…

…す。しかし、T extends Sが成立しているなら、確かに「TがSのサブタイプ」だとは言えます。問題は、サブタイプ／スーパータイプ概念が、extendsだけで尽きているわけではないことです。まだ説明すべきことが残っているのです。残っている肝心なことはまた次の機会にします。[追記]インスティチューションとの関係に興味があれば、http://d.hatena.ne.jp/m-hiyama-memo/20060302/1141280252 にちょっとした補足があります。[/追記]

…：多重継承万歳！ 多重継承死ね！）を声を荒げて言いつのっても、どうせ何の結論も出ませんよ（少なくとも、ロジカルに意味のある結論が出る見込みはない）。まーもっとも、形式化が僕の趣味嗜好に合致しているのであり、それゆえ、「可能なら形式化すべき」との主義主張に至り、「形式化が明晰性をもたらす」という信仰を抱いているわけだから、天に唾を吐いているのは僕ですけどね。 *1:GoguenとBurstallがインスティチューションを導入したのは1984ですから、実は20年以上もたってます。

…では、日本語の本で「インスティチューション」に言及しているのはこれだけです。まー、それはともかく、講義の改善ポイントは何であったかというと、実装寄りの説明を採用したこと以外に、「型とクラスの違いを明確にしたこと」、「値の集合としての「型」から、代数としての「型」に飛躍が起こっていることを時間をとって説明したこと」となるでしょう。型概念を、値の集合から代数（代数系、代数構造）にまで引き上げることは大賛成です。値の集合としての型（types as sets）で理解できるのは、ごく…

…vaScriptで十分な気がしてます。僕がたまに口にするインスティチューションや余代数の説明も、いつかJavaScriptを使ってするかもしれません（無保証言明）。実を言えば、このあいだまでJavaScriptは「なんかトンデモない言語仕様の、ひどく貧弱な言語」-- みにくいアヒルの子と捉えていたのですが、りっぱな白鳥に、でも灰色の斑点が少し残った白鳥に成長しそうですね。いくらりっぱになっても、最適化コンパイラがEXEやDLLを吐く、とかはやって欲しくないな、可愛くなくなる。

…だけ記しておきます。インスティチューションの中心人物はGoguen（http://www.cs.ucsd.edu/users/goguen/）です。彼のインスティチューション・ページ（http://www.cs.ucsd.edu/~goguen/projs/inst.html）をハブに使えます。抽象モデル論という発想はバーワイズ（Barwise）が先のようですが、文（sentence、命題、制約）の集合を天下りに“単なる集合SenΣ”にしてしまったところが、Goguen/Bu…

…。枠組み大枠としてはインスティチューションでしょう、やっぱり。ただし、インスティチューションは何にでも使えるので、オブジェクト指向に特有な現象を説明できるわけではないですね。もっと狭くて強い枠組みには余代数があります。単一のクラスを説明するには余代数はけっこういいですよ。（いまいち中途半端な入門だけど→http://www.chimaira.org/docs/AlgebrasCoalgebras.htm）複数のクラスが絡んだシステムは、代数／余代数だけでは定式化が辛い。ここは…

…ちょっとイメージ落ちた。著者にも印税が入るのだろうが、CiteSeer, arXiv.org, 自分のWebサイトなどに論文を置いたほうが、より「文化と学術に貢献する」ような気がします。それはそうと、しゃくにさわる感情を横に置いて"Institutions:"を眺めて、まー、インスティチューションの例が載っている（当たり前だ）のがいいか、と。（$30の価値があったかといえば、、、いやっ、それは言うまい。）僕としては、当面、インスティチューションのいろんな具体例を知りたいから。

…、余代数／隠蔽代数、インスティチューション、トレース付きモノイド圏、コンパクト閉圏、デカルト閉圏あたりが使えそうな気がしている。各種モナド、トポス、テンソル圏、インデックス圏／ファイバー圏（indexed categories/fibred categories）あたりも道具にはなりそうだが、あんまりよくわかってない。 キマイラ・サイトの圏論コーナーは、http://www.chimaira.org/docs/indexCategoryTheory.htm 圏論に関係しそうな…