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

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

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

参照用 記事

インスティチューション の検索結果:

演繹系と閉包系

…13 演繹系と閉包系インスティチューション〈institution〉は、論理の意味論〈モデル論〉を抽象化した構造です。論理の構文論〈証明論〉を抽象化した構造としてπ-インスティチューションがあります。π-インスティチューションについては、例えば次の論文など: Title: Refinement by interpretation in π-institutions Authors: César Rodrigues, Manuel A. Martins, Alexandre M…

最近の型理論: 拡張包括構造を持ったインデックス付き圏

…tor〉と呼びます。インスティチューション理論ではリダクト関手〈reduct functor〉と言います。言いやすいという理由で、「リダクト関手」を使うことにします。リダクト関手は $`g^*`$ と略記されることがあります(もちろん、$`\cat{P}`$ は周知として)。トータル圏に埋め込まれた局所圏 $`\cat{P}[X]`$ は、ファイブレーション射影の逆像とみなせます。$`\quad P^{-1}(X) \cong \cat{P}[X] \In \dimU{\bf…

可換モナドとラックス・モノイド・モナド(動機も少し)

…ナド 構文モナド をインスティチューション理論の意味での指標の圏だとします。対象 は指標です*1。なにかしら「指標から項を生成するメカニズム」があるとします。そのメカニズムは文法/構文生成規則と言っていいかも知れません。指標 から生成された項の集合を とします。 は単なる集合ではなくて何らかの構造を持つかもしれません。その構造込みで だとしましょう。 は圏 の射(指標射)にも定義できて、 は圏 上の自己関手になるとします。つまり: が大きい圏である可能性も考えて (小さい圏達…

ローヴェア流セオリー論と統計モデル

…プログラム意味論(のインスティチューション理論)ではリダクト関手〈reduct functor〉、インデックス付き圏の文脈では再インデキシング関手〈reindexing functor〉とも呼ばれます。モデル移行関手を使えば、異なる統計セオリー上の統計モデルを比較することができます。パターソンは、モデル移行関手の実例も出しています。例えば、線形モデルが一般化線形モデルの特殊例であることは直感的には当たり前そうですが、厳密な記述と証明は出来るでしょうか? パターソンの動画でこの…

指標モジュールの話を(いつか)したい

…つも助けてくれるのはインスティチューション理論です。インスティチューション理論をベースに考えるのが良さそうです。少なくとも僕にとっては、インスティチューション理論が一番頼りになる足場です。インスティチューション理論の基礎概念に指標〈signature〉があります。指標をモジュールと考えることもできますが、規模が小さすぎるので、幾つかの指標をまとめたグループをモジュールと考えるのが良いでしょう。つまり、「モジュールとは何か?」に対しては「指標の集まりがモジュールだ」と答えること…

高次圏を考慮した指標の書き方

…性だけを要求します。インスティチューション理論(そういう理論がある)では、左単位律のような条件〈公理〉は指標とは切り離しますが、「何を条件として切り離すか?」の基準がハッキリしないので(「指標と仕様」参照)、ここでは条件〈公理〉も指標内に記述します*1。指標内のキーワードを変える「多相関数の「パラメトリック性 vs 満足性」」にて: 標準的なキーワードは、type, function ではなくて、sort, operation ですが、キーワードに違和感を持つ人が多いので t…

多相関数の「パラメトリック性 vs 満足性」

…。満足性の定義には、インスティチューション理論の道具立てを使います。が、インスティチューション理論を知っている必要はありません。Xさんは「lengthらしさ」を内心期待してましたが、3人に伝えてません。「lengthらしさ」を何個かの文として言語化しなくてはなりません。実際の関数fが、文sで記述された性質を実際に持つとき、次のように書きます。 f |= s 記号'|='(TeXだと \vDash '')は、満足関係〈充足関係 | satisfaction relation〉の…

等式的関手インスティチューションの作り方: 悩みどころ

…情です。「等式的関手インスティチューション(概要)」で述べたように、等式的関手インスティチューションでは、指標Σに対するモデル圏*1 Model[Σ] を、関手圏*2として具体的に構成するのでした。 Model[Σ] := [Σ◇, Set] 上記の右辺によりモデル圏が定義されますが、右辺に登場する (-)◇ と [-, -] の意味がハッキリしないと定義したことになりません。実際、これじゃ全然ハッキリしてません。モデル圏の定義をハッキリさせようとすると、圏論では常につきまと…

等式的関手インスティチューション(概要)

…Burstall〉のインスティチューション〈institution〉を少し具体的に考えたい、ってことでした。どのように具体化したいかと言うと: 使う論理を、等式的論理と一階述語論理に固定する。 指標Σに対するモデルの圏を、Model[Σ] := [FreeCat(Σ), Set]CAT と具体的に与える。 指標圏を固定する気はないのですが、当座の指標圏としては、有向グラフの圏を採用します。ただし、単に「有向グラフ」と言ってしまうと誤解をまねきそうです。通常の有向グラフGと、両…

任意の圏を等式により2-圏とみなす

…Burstall〉のインスティチューション〈institution〉は、論理やプログラムの構文論と意味論〈モデル論〉の抽象的枠組みを提供します。抽象度が高いゆえに、一般的で汎用性が高いのですが、ちょっと掴みどころがない感じもします。そこで、抽象的インスティチューションの一部を具体化します。 使う論理を固定する: 抽象的インスティチューションは論理非依存〈logic nutral | logic agnostic〉がウリなんですが、使う論理を等式的論理と一階述語論理に固定します…

モノイド対象と単体的対象

…指標とモデルの理論(インスティチューション理論含む)と、ローヴェア理論(ちゃんと言うと、「ローヴェア理論」の理論)と、形状圏を使ったホモロジー/コホモロジーが扱っているモノ達は、酷似しているのでしょう、おそらく。書き方に関する注意:ある言葉の同義語がある場合は、山形括弧('〈'と'〉')で囲んで示します。内容: モノイド対象 モノイドの指標 集合圏において具体化 順序集合の圏において具体化 ベクトル空間の圏において具体化 ローヴェア圏 モノイドの指標のローヴェア圏 ローヴェア…

指標と仕様

…〉と呼ぶ人もいます。インスティチューションの理論などでは、法則が入ってない指標と、法則を入れた仕様を区別したほうが確かに分かりやすいです。なんでもかんでも指標で済ませると、区別したいときに困るような気がします。多パート指標トム・レンスター〈Tom Leinster〉は(例えば https://arxiv.org/abs/math/9810017 で)、指標をデータ・パートと公理パートに分けて書いています(書き方はインフォーマルですが*1)。モノイドの指標をパート分けして書き直…

インスティチューションと忘却関手

…6-06(日曜))、インスティチューション理論についてほんの少しだけ説明しました(チアガールズの説明のほうが長かった気がする)。インスティチューションについては、「キマイラ飼育記」の初期の頃からチョコチョコ触れています。 「インスティチューション」の検索結果 インスティチューションに関する資料として、僕が最初に思い浮かべるのはゴグエン〈Joseph Goguen〉による次のページです。 https://cseweb.ucsd.edu/~goguen/projs/inst.ht…

ベイズ確率論、ジェイコブス達の新しい風

…Burstall〉のインスティチューション〈institutions〉や、ローヴェア〈William Lawvere〉のハイパードクトリン〈hyperdoctrine〉との関連もありそうです。インスティチューション/ハイパードクトリンからの知見を、ベイズ論理/ベイズ計算に活かせるかも知れません。例えば、「順序集合のカン拡張と特徴述語論理」の手法で限量子を定義できそうな気がします。ベイズ確率論の新しい風を感じたい人、従来の理論にモヤモヤを感じている人は、ジェイコブス・スタイル(…

クリーネ代数 再論

…理の圏論的な定式化 インスティチューションとホーア論理 というわけで、クリーネ代数/テスト付きクリーネ代数は、プログラムの振る舞いの分析、仕様記述の手法、テストフレームワークの作り方などに具体的な示唆を与えてくれます。これが、クリーネ代数/テスト付きクリーネ代数に興味を持つ(ひとつの、しかし大きな)動機です。クリーネ代数とは何かクリーネ代数を一言でいえば、アフィン線形不動点方程式を扱うための代数系です。となると、アフィン線形不動点方程式とは何か、から説明を始めるべきでしょう。…

高次圏: 無基底・無限階層の世界とn-圏

…scu〉のエッセイ「インスティチューション、中観派、一般モデル理論〈Institutions, Madhyamaka, and Universal Model Theory〉」を紹介しました。中観派〈ちゅうがんは〉は大乗仏教の学派です。ダイアコネスクは、中観派思想を熱心に勉強した上で、それがインスティチューション/一般モデル理論/圏論などと同じ発想だと言っています。でも僕は、仏教は何も知らない(勉強する気もない)ので、ほんとのところ「同じ発想」かどうかは分かりません。確信がな…

指数関手と構文論・意味論

…デルのスキーマの圏、インスティチューションの指標圏に相当します。二項関手 E:Quivop×Cat→Cat を次のように定義します。 E(X, C) := [X◇, C] ここで、[-, -]は圏Catの内部ホム、つまり関手圏です。Xは箙ですが、X◇は圏なので、関手圏[X◇, C]を作れます。Eは、s:X→Y in Quiv に対してはsの前結合で反変的に、H:C→D に対してはHの後結合で共変的になります。E(X, C)は、関手データモデルのデータベース状態〈データベース・…

なにゆえにカン拡張なのか

…そのテの知識がないと理解できないことが残念な点です。特定分野の予備知識を要求しない事例があるといいんですが … 何かあったら教えてください。 *1:とある圏の終対象または始対象の議論なのに、あえて「普遍」とか難しげな言葉を使う理由が分かりません。 *2:「ケンロニスト」はbonotakeさんによる造語 *3:"migration"の訳語は「転送」「移動」「移送」とかもあるでしょう。 *4:インスティチューション理論では、リダクト関手〈reduct functor〉と呼びます。

プログラム意味論の書き方サンプル: UMiToL

…と複雑な構造(たぶんインスティチューション)が現れます。また、条件分岐や繰り返しの制御構造を入れれば、それも複雑さにつながります。オモチャでない実用的プログラミング言語の意味論が随分と複雑そうなことは想像できるでしょう。しかし、その複雑さのなかに面白くて深い構造が潜んでいると期待もできるのです。 *1:0は自然数に含めます。 *2:valが何でもいいときは、違うリテラルが同じ値を指すことがあり、また、リテラルでは表現できない値も存在します。リテラルで表現できなくても、リテラル…

無料で入手できる本格的(紙なら高額)な理数系専門書15選 第2回(2017年春)

…いて書かれています。インスティチューションについての解説があります。例えば、大乗仏教中観派の話の予備知識が得られます。 Stochastic Integration with Jumps Stochastic Integration with Jumps (Encyclopedia of Mathematics and its Applications)作者: Klaus Bichteler出版社/メーカー: Cambridge University Press発売日: 20…

大乗仏教中観派と一般モデル理論

…クのエッセイの主題はインスティチューション(Institutions)と一般モデル理論(Universal Model Theory)です。ダイアコネスクはこの分野における第一人者なので、その主題的内容は完全に信用できるものです。となると、“欺瞞”かどうかの分かれ目は、この主題に対して仏教や中観派を持ち出すのが適切なのか? 仏教/中観派に関する理解が行き届いているのか? あたりでしょう。しかし、仏教がうんぬんなんて、僕には全く判断できません。とりあえず、仏教/中観派に関するダ…

Haskellの型クラスに関わるワークアラウンド

…on 2 3 のようにします。…… …… フエーッ、こんなん、僕の欲しいオーバーロードじゃない!*2 *1:Haskellでの標準的な方法は、型クラスNumを経由して足し算モノイドと掛け算モノイドを定義するものです。 *2:例えば、掛け算でも足し算でも通用する話をするとき、演算子記号を◇とかして、(◇) = (*) か (◇) = (+) かの区別は、「話の文脈」として与えるべきなんでしょう。ここらへんをキチンと分析するなら、インスティチューション理論を使うべきかと思います。

「関数型プログラミングはオブジェクト指向の正当な後継」なの?

…と置換原則 できればインスティチューションで分析したいところ。割と圏論バッキバキだったりするんだけど: 圏論とオブジェクト指向 インスティチューションと型階層 インスティチューションと Categories-as-Types インスティチューションとホーア論理 Haskellでは型同士の継承をサポートしていませんが、型クラスから型インスタンスへの継承はできるため、それを利用した多態性の実現が可能です。 「型クラスから型インスタンス」は文字通りインスタンス化であって継承とは言わ…

一般化されたマイヒル/ネロードの定理 1:準備と事例

…ure)と呼びます。インスティチューション理論では、指標をギリシャ文字大文字で表す習慣があるので、それに従ってギリシャ文字大文字を使ったのです。Φはグラフですが、圏と同様な記法を使って、頂点の集合を|Φ|、x, y∈|Φ| に対して2頂点のあいだの辺の集合をΦ(x, y)で表します。伝統的オートマトンAに対する指標グラフΦは次の通りです。 |Φ| = {0, 1, 2} Φ(0, 1) = {i} Φ(1, 1) = Γ Φ(1, 2) = {t} それ以外のΦ(n, m)は…

論理におけるさまざまな「矢印」達

… sentenceはインスティチューションの用語です。インスティチューションでは、|= をsatisfaction relationと呼びます。 動詞として、deduce, refine, infer, reasonなどもありますが、この表では使ってません。 |- を使ったjudgmentの左(premisesと書いた)はcontextということもあります。特に型理論ではcontextが多いです。 記号法/用語法だけでなく、内容的な補足をちょっとしておきます。|-, |=, …

関手データモデル/圏論データベース: その後の発展と現状 (2016)

…のベースとなっているインスティチューションと、FQLのベースとなっている関手データモデルは、事実上同じものです。そのことは次の記事に書きました。 一般関手モデル:インスティチューションとの関係 Alloyとの類似性に関して言えば、「Alloyを理屈っぽく考えてみようと思う」で次のように書いたことがあります。 関手データモデルとAlloyは、かなり親和性が高いんじゃないか、と感じるのです。[...snip...]また、関手データモデルを理解する道具としてAlloyが役に立つとも…

Coqの型クラスの使い方:バンドル方式とアンバンドル方式

…則を使うこの方式は、インスティチューションとの対応がハッキリしていて、個人的には使いやすく感じます。アンバンドル方式アンバンドル方式で何をバラすのかというと、指標に含まれる「台集合、二項演算、単位元」を別々なパラメータとして法則を表すクラスに渡すのです。 (* === アンバンドル方式 === *) Class MonoidUnbundle {A: Set} (op: A -> A -> A) (u: A) := { (* モノイドの法則 *) assoc'': forall…

Coqで定理を記述してみる、型クラスとか使って

…」に分けるやり方は、インスティチューションを意識しています。Σを指標とするとき、インスティチューションではモデル圏Mod[Σ]を定義しますが、Coqの型クラスとしてのΣマグマクラスは、モデル圏 Mod[Σ]の対象類 |Mod[Σ]| = Obj(Mod[Σ]) に対応します。指標Σの論理式の集合Sen[Σ]の部分集合Aを公理として特定したとき、Aを満たすモデルの全体は|Mod[Σ]|の部分類を定義します。公理系Aを記述したCoqの型クラスが、構造の法則クラスです。法則クラスは…

関手オートマトンを説明する記号法に大いに悩む

…すために使おう。Σはインスティチューション理論で指標(signature)を表すために使われる記号です。指標はアルファベットの拡張概念ですから関連はあるのです。グラフ理論からすると異例の記号法ですが、Σ, Γ などで有向グラフを表します。総和記号と紛らわしいことには目をつぶります。というわけで、オートマトン F:Σ→Set のように書くことにします。値を取る圏は具体的な圏を想定しているので、Set、PtSet、Rel などが登場します。有向グラフと指標に関する用語と記号法関手…

形式言語理論のための代数

…つからなかったので、インスティチューション理論の言葉を拝借しました。αB := αtBα と置くと、次の“指数法則”が成立します。δ = δT:T→T は単位行列だとします(遷移写像δと記号がかぶってますが、これも文脈で判断)。 α(βC) = αβC (α:S→T、β:T→U、C:U→U) δB = B B ≦ B' ならば、αB ≦ αB' これらの法則は、定義からすぐに出ます。インデックス付き圏 AutomH[-]基数条件χを固定して、MatχB を考えます。Bはブール…