通常集合論 レイヤー 選択されたインスタンス アンビエント レイヤー 3 I3 = s2-圏 CAT A3 = s3-圏 s2- レイヤー 2 I2 = 圏 Set A2 = s2-圏 CAT レイヤー 1 I1 = 集合 A A1 = 圏 Set レイヤー 0 I0 = 要素 a A0 = 集合 A 線形代数的モノイド論 レイヤー 選択…

予備知識／能力として、原始組み合わせ幾何〈primitive combinatrial geometry〉を仮定する。有限点や有向線分などを理解している、とする。n-箙、特に有限n-箙は原始組み合わせ幾何の概念で直観で理解可能だとする。参照→ マテリアル計算 - 檜山正幸のキマ…

やった、n-セオリーから自然にインスティチューションが出てくる。n-セオリーまず、n-セオリーのk-段階（k-階層、次元k）の定義： (At dimension k): Σk∈0k-Spef[Σk+1], Ak∈0k-Mod[Σk+1](Σk, Ak+1) Ck := k-Mod[Σk+1](Σk, Ak+1) k-Mod[Σk+1]:k-Spef[Σk+1]×Ck…

マイクロコスモ原理は、原理ではあるが困難として立ちはだかる。逆帰納ステップをどうやって止めるか？ がシビアな問題になる。次の方針はひとつの解決策となる。 圏論的世界（いちおう、グロタンディーク宇宙とは区別して世界）に最初から組み込みで存在す…

Title: The category of 3-computads is not cartesian closed Authors: Mihaly Makkai, Marek Zawadowski Pages: 6p URL: https://arxiv.org/abs/0710.5202 マレク・ザワドウスキイはスタニスワフ・スザウィールの先生。この論文で、生成系の要素である者を…

For γ in 3-Th, C in 2-Cat. For β in 2-Th, B in 2-Modγ(β, C). For α in 1-Th. 1-Modβ(α, B) in 2-Modγ(β, C)一般的には、 For γ in n-Th, C in (n-1)-Cat. For β in (n-1)-Th, B in (n-1)-Modγ(β, C). For α in (n-2)-Th. (n-2)-Modβ(α, B) in (n-1)-Modγ…

まずは記号法、事例とルールがごちゃ混ぜだけど。 1-Cmptdα -- ドクトリン〈2-セオリー〉がαである1-コンピュータッドの圏 1-Cmptdsmc -- ドクトリンが「対称モノイド圏」である1-コンピュータッドの圏 2-Mod(smc, Cat) -- 小さい対称モノイド圏の2-圏 Σ in …

最近、マンダラの精神を忘れていたかも知れない。「この世はマンダラだ」 マンダラ→ http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B%A5%DE%A5%F3%A5%C0%A5%E9%5D ミニマンダラ→ http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B…

defintion and example - 檜山正幸のキマイラ飼育記 メモ編 同義語・多義語の例 - 檜山正幸のキマイラ飼育記 メモ編 指標とモデルと意味論 - 檜山正幸のキマイラ飼育記 メモ編 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 決める側…

{definition (form)? | specification | signature | (type)? class | interface | concept} {example | model | (type)? instance | structure | implementation | class | algebra}

昨日 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編、次の用語を導入した。当たり前で自己説明的な言葉だと思う。 (n-)?代数(的)?定義(形式)? (n-)?定義(形式)? 同義語が： (n-)?指標 (n-)?仕様 (n-)?セオリー (n-)?型クラス (n-)?イ…

演繹付きインスティチューション〈institution with deduction〉を定義する。普通のインスティチューションに、指標Σごとの演繹性判断〈deducibility judgement〉|-Σが付いている。 |-Σは、Pow(Sen[Σ])とSen[Σ]のあいだの（二項）関係 演繹性判断は、次の公…

インスティチューションでは、指標Φに対してモデル圏Mod[Φ]が決まる。まーこれはいいのだが、指標圏が何であるか、Mod[Φ]をどう作るかは言及しない。公理的フレームワークだから、まー、そんなもんだ。しかし実際に出現するインスティチューションではもっと…

インスティチューションの指標の圏があって、Σ, Φが指標として、基本指標射 σ:Σ→Φ だけでんなくて、モナドFが働いた FΦ を考えて、クライスリ射 Σ→FΦ を使うことは非常に多い。つまり、最初の指標圏をクライスリ圏に拡張して使う。一方で、柱体とホモトピー…

C = V + H と直和分解されている圏が隠蔽指標。射を次のように呼ぶ。 dom(f) cod(f) fの呼び名 H H transition H V observer V H constructor V V calculation 通常、calculationはないとする。M:C→Set が集合論的なモデル。Vの要素（対象）だけで定義された…

多ソートメイヤー指標（many-sorted Meyer signature）とは： 状態指標の集合Σ 値指標の集合Φ s∈Σ ごとに、通常のメイヤー指標 (Cσ, Qσ)。クエリーの値はΦから取られる。 s, t∈Σ ごとに T(s, t) という記号の集合。状態のあいだの変換を表す記号。空でもよい…

「インスティチューションだのプロ関手だのなんだの」の「何が必要か」に書いたこと、だいたいの見当は付いたと思う。厳密性がないハナシで、その意味ではマダマダだけど。目的は多段階の設計実装プロセスをきちんと定式化すること。インスティチューション…

クリスマスで連休で、その後は正月で、ってなわけで、こういうときは、普通どおりに仕事するのもナンだし、最近は子供と遊ぶことも少ないしで、なんだかボーッとしている。すると、ボーッとしたことを思いつく。はたして意味があることかどうかわからないが…

Command-Queryが分離した指標をメイヤー指標と呼ぶことにしよう。メイヤー指標のモデル（理論的な実装）をメイヤーオートマトンと呼ぶ。もちろん、インスティチューションになる。いつだか忘れたが、昔、IDLの構文に、when accept xxx とか issues Event, re…

インスティチューションは概念を整理する枠組みとしては便利だが、中身がまったくないので、インスティチューションから出発してもラチがあかない。なんか実際のモノを作って、後から見たらそれはインスティチューションでした、ってことじゃないとダメだな…

インスティチューションは、構文とモデルを区別する。もともとがモデル論だから当たり前だ。が、コンピュータでは、その構文領域もデータ領域としてモデルの世界に入り込む。ここが問題。インスティチューションの構造を残しながらも、構文（項）がモデルの…

帰納的に自由な集合の件だが、有限な代数指標Σを決めて、Σの自由代数＝始対象のことだわな。Σを決めるごとに再帰関数（帰納関数）論ができるから、全体としてはインスティチューション。

パリク・ベクトルを一般化して、正規集合に関するパリクの定理（本来は文脈自由文法に関する定理）を示したいものだ。まず、Pow(Nn)に、足し算∪と掛け算+で半環構造（cup-plus代数とでも呼ぶべきか）を入れる。クリーネ級数は収束するから、クリーネ連続半環…

本編 なんで多重継承はそんなに嫌われるのか？ ちょっくら分析してみるか - 檜山正幸のキマイラ飼育記 (はてなBlog) の補足：簡易インスティチューションで定式化してみる。実は簡易インスティチューションにさえなってない略式インスティチューション。どの…

これも後で書く - 檜山正幸のキマイラ飼育記 メモ編 形式言語系の定義 - 檜山正幸のキマイラ飼育記 メモ編 この話。ラベル付き遷移系と多項式の例を出す。（多項式インスティチューションについては、多項式インスティチューション - 檜山正幸のキマイラ飼育…

指標の圏はだいたいこれでOKだろう - 檜山正幸のキマイラ飼育記 メモ編 昔から言っていたことだった - 檜山正幸のキマイラ飼育記 メモ編 形式言語系の定義 - 檜山正幸のキマイラ飼育記 メモ編 指標について色々 - 檜山正幸のキマイラ飼育記 メモ編 観測可能…

本編「レコードの型階層を合理的に説明できるか」の設定でインスティチューションを作ってみる。用語や記号は本編記事に従う。指標圏フィールド名として許されるすべての名前の集合をName（無限集合と仮定）とする。Nameの有限部分集合を指標と呼ぶ。例えば…

余完備性をKleisli圏に持ち上げたい open programs open programs 再び 2005年の夏、えー、こんな昔からTermモナドがプログラムだって知っていたの、僕？ Cospan構成にも言及しているし。以上をふまえて書いた記事： ソースコードの形式化 これ↑で、「コンポ…

protecting 演算（記号）も法則（等式）も追加できない。 extending 演算は追加できるが法則は追加できない。 using 自由

プレ圏（グラフ上に部分的な圏構造）の圏をPrecatとする。さらに、プレ圏に同値関係（一般化合同）が与えられたものを(P, E)として、その全体をEPrecatとする。EPrecatは有限余完備だと期待している。EPrecatが有限余完備ならその上の余スパンの圏が作れる。…