プログラム意味論
基本的な概念と用語： まだ曖昧な所があるが、 区分〈くぶん | division | ディヴィジョン〉： 特定の圏Cと次元数kのペア。Cのk-射の集合を意味する。 区分ラベル： 区分に付ける人間可読なテキスト。 区分け〈くわけ | divisioning | ディヴィジョニング〉 …
ハイパーインスティチューションは、3×3のマトリックスで整理できる。縦横どう書くかは自由だが、3ロール×3レイヤーと呼ぶ。 ロール： ベース（Base）ロール、論理（Logi）ロール、モデル（Mode）ロール レイヤー： アンビエント（Ambi）レイヤー、計算（Com…
圏論的な世界〈world〉を次のようなものだとする。 世界の構成素を領地〈dominion〉と呼ぶ。 領地は、高次の圏、複圏、多圏のいずれかである。 領地は有限個である。 それぞれの領地は小さいn-圏, n-複圏, n-多圏である。 領地の次元は有限で、最高次元nが領…
指標（"インデキシング・ベース圏”の対象）と命題（{インデキシング垂直圏 | ファイブレーションのファイバーである圏}の対象）のペアを仕様と呼ぶ。仕様はグロタンディーク／エルブラン圏＝ハイパーベース圏の対象であると同時に、ハイパーインスティチュー…
重要なのはグロタンディーク／エルブラン圏である。 MLの概念 グロタンディーク／エルブラン圏 別な言い方 シグニチャー 仕様 セオリー ストラクチャ 絶対セオリー インスタンス ファンクタ 相対セオリー トランスフォーマー シグニチャに属するストラクチャ…
素材： 名前の集合 Name アンビエントドクトリン アンビエント圏C： アンビエントドクトリンから1つ選ぶ 論理ドクトリンL 以上から、指標圏と指標射が作れて、指標圏を定義できる。この指標圏をベース圏として、論理ドクトリンLに値をとるインデックス付き圏…
Aがテスト付き半環で、test(A)がそのテスト元の集合だとする。δ:A→test(A) がプレドメイン作用素だとは、 ∀a∈A.∀p∈test(A).( δ(a) ≦ p ⇔ a ≦ pa ) のこと。次でも同値。 ∀a∈A.∀p∈test(A).(1. a ≦ δ(a)a, 2. δ(pa) ≦ p) プレドメイン作用素は次を満たす。 (i)…
Linear Logic, Domain Theory and Semi-Functors / Hoofman http://www.cs.uu.nl/research/techreps/repo/CS-1990/1990-34.pdf フーフマン（Hoofman）の線形圏 - 檜山正幸のキマイラ飼育記 メモ編も見よ。
新→旧 の順 計算科学における半加法圏の位置付け テンソル半加法圏とプログラム意味論 個体と世界の関係：圏から論理半環を絞り出す クリーネ代数の「テスト」を圏論的に定義できるだろうか？ クリーニ代数と圏論 トレースを使ってクリーネスター（またはク…
インスティチューションでは、指標Φに対してモデル圏Mod[Φ]が決まる。まーこれはいいのだが、指標圏が何であるか、Mod[Φ]をどう作るかは言及しない。公理的フレームワークだから、まー、そんなもんだ。しかし実際に出現するインスティチューションではもっと…
型クラスのパラメータ問題（トラブルっぽい話）が出てくるのは、指標とモデルの相対性の考察が不足しているせいだと思う。グロタンディーク平坦化を“積分”とみなしてのフビニに定理だと思う。繰り返し積分と同時多重積分の同値性。直積領域の積分ではなくて…
MLのモジュールシステムは禁欲的で、必要最小限の機能だけだが、スッキリしていて好きだ。だが： signatureにパラメータを付けられない。functorは当然にパラメータ（引数）を持つが、functorの値はstructureであってsignatureを値には取れない。 これは当然…
http://arxiv.org/pdf/0904.3848.pdf の3ページ目にconsolidationの定義が書いてある。 A consolidation for C is a function p: Co×Co → C, p(e, f) = pe,f, where pe,f is an arrow from f to e and pe,e = e.
昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはい…
Standard MLが圧倒的に良くできているな。オーバーロードを意図してない、型システムじゃない、という問題点はあるが、許せる、許せる。Haskellは「悪いお薬」をキメている。当座はとても元気が出るが、いずれは心身を蝕むアレ。型名に対するコアージョンを…
Scalaの書き方がけっこう良い。 trait Functor[F[_]] { def map[A,B](fa: F[A])(f: A => B) : F[B] }
関数型プログラミングとオブジェクト指向について、何か書く、かも - 檜山正幸のキマイラ飼育記 関連で少し調べてみたら、ウワーッ、随分とひどいことになってるんだな。 型述語解釈 http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf : axio…
型クラスの意味論がイイカゲンなわけだが、それはそうとして、型クラスの現実的に厳しい問題は： 型システムとモジュールシステムの役割分担、相互関係 名前の管理 特に名前の管理が滅茶苦茶に大変なのだが、あまり指摘されない。裸の名前・記号をどう解釈し…
Title: Categorical Programming for Data Types with Restricted Parametricity Authors: Dominic Orchard and Alan Mycroft URL: https://www.doc.ic.ac.uk/~dorchard/drafts/tfp-structures-orchard12.pdf 誤解しているとしか思えない。型クラスのスーパ…
公理付きか公理なしか： 公理付きならセオリー、なしなら指標。 パラメータが1つか複数か： 単パラメータ型クラス（単一の型パラメータを持つ型クラス）と複パラメータ型クラス（複数の型パラメータを持つ型クラス） パラメータを使うかレコードフィールドを…
a, b ：グラフの辺 a, b ：アルファベットのレター b : 振る舞い d ： 識別頂点 e ： 分離対象の分離射（予定） f, g, h ： 指標圏の射 i ： 始状態指定 i ： 添字 k ： コンストラクタ射、コンストラクタ-コマンド射 k ： 体 n, m ： 整数 p ： 余分離対象…
一般関手モデル：どこを一般化？ - 檜山正幸のキマイラ飼育記 一般関手モデル：インスティチューションとの関係 - 檜山正幸のキマイラ飼育記 一般関手モデル：「圏の表示」の圏 - 檜山正幸のキマイラ飼育記 一般関手モデル：相対スキーマと相対インスタンス …
とりあえず表。説明はその下。 関手オートマトン 可達性 可識性 圏論 相対分離性 相対余分離性 部分圏 余反映的部分圏 反映的部分圏 エルブラン構成 単純エルブラン構成 二重双対エルブラン構成 分離性は圏に分離対象（separator）または分離対象族（family …
この話題については、コボルディズム、TQFT、オペラッドとか - 檜山正幸のキマイラ飼育記 メモ編にまとめてある。上記の記事と、ルビンの壺と意味論 - 檜山正幸のキマイラ飼育記 メモ編から参照していたジョーンズ（Vaughan Jones）のスライドがドメイン（qq…
メイヤー流のCommandのさらなる分類 リソース獲得 -- 増進的状態変容で、戻り値はないか、成功・失敗を告げる。 リソース解放 -- 減退的状態変容で、戻り値はないか、成功・失敗を告げる。 リソース生成 -- 増進的状態変容だが、自分で所有権を持たず、生成…
メイヤー先生のCommand-Query分離の原則はいつだって役に立つ。ただ、若干の拡張や補足は必要になる。コマンドとして、“状態空間のendomorphismである状態遷移（transition）”以外に、“異なる状態空間のあいだの写像である状態変容（mutation）”が必要だ。tr…
単一のオブジェクトではなくて、複数のオブジェクトが連携するとき、編成された連合体を何と呼ぶか？ あまり適切な呼び名がないような気がする。フェデレーションという言い方もあるが、大げさな気がする。2002年頃、僕はオブジェクトフォーメーションと呼ん…
次の3者の関係が問題 仕様と仕様の記述方法 仕様に基づいて実装する“実装者” 実装が仕様に合致しているかどうかを確認する“テスター” 次のように考える。 仕様は、モノイド生成元と関係で与えられる。関係には観測演算子が使われる。 テストには、テスト式と…
なにがミソかというと、係数（可換）半環Kが総和完備なこと。これによって、K値関数の引き戻しだけではなくて前送りが定義できる。つまり、反変関手だけでなく共変関手も定義できる。反変と共変が同時に定義できると内積と共軛（随伴）っぽい概念が使えるよ…
まず、可換モノイド上の総和構造 Aは可換モノイド x:I→A の形の写像の“集まり” Summable(A) がある。集合とは限らない。 Σ:Summable(A)→A がある。総和をとる作用素。 x:I→A のIが有限集合（空集合も含める）のとき、Σx は有限和に一致。 部分和の存在：φ:J→…
