まず、今までのステパノフへの言及： ステパノフ理論：正則型 - 檜山正幸のキマイラ飼育記 メモ編 ステパノフ理論：コンセプト - 檜山正幸のキマイラ飼育記 メモ編 プロトキン／パワー風の状態とRDBとポインター - 檜山正幸のキマイラ飼育記 メモ編 ステパノ…

既存ソースの修正で感じたこと - 檜山正幸のキマイラ飼育記 メモ編 ： もとのソースはよくテストされて枯れたソースなので、無闇に変更はしたくない。イジらなくてよいところはそのまま使いたい。構造を変えるようなリファクタリングもリスキーだからしたく…

次を読めば参考になるはず。 Title: Quasistrict symmetric monoidal 2-categories via wire diagrams Author: Bruce Bartlett URL: http://arxiv.org/abs/1409.2148 Pages: 18p. Title: Polycategories via pseudo-distributive laws Author: Richard Garne…

計算科学 -- 型付きラムダ計算とデカルト閉圏 論理 -- 自然演繹とシーケント計算 それらを結ぶのが多圏の絵算。どうやって結ぶのか： デカルト閉圏（一般には非対称モノイド閉圏）と厳密多圏の対応を作る。 自然演繹は絵算と同一視する。つまり、自然演繹の…

今日は画像だけ。いずれ本編で説明する機会があるかも。

20070416 直積と射影がらみの高階関数たちの相関図 - 檜山正幸のキマイラ飼育記 20090325 演繹系とお絵描き圏論 - 檜山正幸のキマイラ飼育記 今、けっこう真面目に考えている。多圏の導入と使い方。[追記]だいたい出来た→ http://d.hatena.ne.jp/m-hiyama-me…

クラスプ（clasp; 留め金）の絵。モノイド閉圏、オダンゴ、留め金、池袋 - 檜山正幸のキマイラ飼育記の図： 方向の取り方： カリー化： 左右のカリー化： この絵法を最初に見たオリジナル論文： Title: Computation and the Periodic Table (ATMCS 2008) Aut…

終対象またはモノイド圏の単位対象からの射を「要素」とみなすのは割と自然な発想。デカルト圏なら終対象＝単位対象なので、Cをデカルト圏として、Elt(C) = {e∈Mor(C) | dom(e) = 1 } としてElt(C)を定義する。Elt(C)は単に射の集合で構造を持たない。Cはデ…

γアノテーションは、束縛子や限量子と似た構文で、γ記号の後に変数を伴いスコープを持つ。γにくっついている変数をγ変数と呼ぶことにする。γアノテーションに変数の束縛作用はなくて、γアノテートされた項（スコープ内部）でγ変数は自由のままである。したが…

CCC計算 - 檜山正幸のキマイラ飼育記 メモ編 で出したγ導入の件。γアノテーションという記法をラムダ計算に追加して、γアノテーションの導入規則も加える。γアノテーションの「γ」には何の意味もない。ギリシャ文字を適当に選んだだけ。ガンマ計算とかガンマ…

本編： 感動か効率性か - 檜山正幸のキマイラ飼育記 オカシイと文句を垂れるなら、修正案を提示しないとね。シーケントの左辺が型宣言の集まり、右辺が型付き代入文の集まりとなる形を仮にCCCシーケントと呼ぶ。CCCシーケントの意味はデカルト閉圏の射だが、…

双代数と双モノイド - 檜山正幸のキマイラ飼育記 両モナドのアイレンベルク／ムーア構成 - 檜山正幸のキマイラ飼育記

x, yがレコード、n, mが名前のとき、 x >>+ y は、左優先のマージ x + x +++ y は、排他的公平なマージ、エラーの可能性あり !x は、xのレイフィケーション、結果はインスタンスである。フィールドの型が値ロールで解釈される。 x.n でフィールドを参照でき…

名前管理の単位をモジュールとパッケージと呼ぶ。 名前空間が単一のファイルに対応するとき、モジュールと呼ぶ。 名前空間が単一のディレクトリに対応するとき、パッケージと呼ぶ。 パッケージはレコードインスタンスであり、フィールド名はファイル名で、フ…

オミクロン・ラムダ計算というものを考える。目的は、 名前管理をちゃんとする。 名前や項の解釈に柔軟性を持たせる。 十分な表現力を持ち、かつ出来るだけ単純なデータ構造を導入する。 いくらでも高階の存在物を扱えるようにする。 そのためには、 例外を…

型ヒントという概念を導入する。型ヒントは Hint{name1: typeList1, ..., nameN: typeListN} という形。 型ヒントを使って、termの型を推論する。 ここのtermは、「レコードterm＝レコードインスタンス」であってよい。 型コンテキストは、型ヒントの特殊な…

基本概念はレコード型とレコードインスタンスとレコードのアプライだけでなんとかなるのでは？ レコード型は、{name1 : type1; ..., nameN : typeN; } の形 レコードインスタンスは、{name1 := val1; ...; nameN := valN; } の形 未割り当て型宣言と値割り当…

集合圏、部分写像の圏、関係圏は一緒に考えて互いに比較するといいようだ。今の焦点は部分写像の圏。まずは、モナド、つうか随伴関手対と共に考える。Set上のモナドAugを考える。Augはaugmentation（増加、増強、増大、添加物、拡大）のことで、付点モナドと…

カリー／ハワード対応は、まさにアナロジーの勝利。マーク・ホプキンスの観測もアナロジーだし、バエズ／ステイのロゼッタストーンにしろアナロジーだ。表のまとめ： 2015年10月、11月、12月ほんの少し - 檜山正幸のキマイラ飼育記 メモ編 の表の多くはアナ…

主に2015年10月と11月、12月少し（昨日・今日とか）でブログに出現した表を集めてみる。全部一度に眺めると、なにか思いつくかもしれない、と期待して。まとめる作業がイイカゲンだから、順不同で網羅的かどうかも分からない。 豊饒プロ関手は豊饒な世界を提…

ローヴェルの一般化距離空間では、一般化距離（≒コスト）を測るのに非負実数（∞含める）を使っている。豊饒圏の枠組みで考えれば、別な圏（ベナボウコスモス）でいいはずだ。ベクトル空間Vを次のようにしてモノイド圏Cだと考える。 |C| = V 対象＝ベクトルに…

ホムセット（ホモセット）ならぬヘテロセット H(X, A) |C|×|D|→Set を考えると、CのHへの左作用、DのHへの右作用を考えた双加群は、プロ関手 H:Cop×D→Set, H:C-/→D になる。特に、C = D のとき、自己プロ関手は、左C-右C-双加群となる。以上はよく知られた事…

タスクというわけが分からない概念がある。ひとまとまりの仕事という意味だが、それじゃ国語辞典の項目としての説明なだけで「定義」になってない。仕事に対してその仕事をする主体をエージェントと呼ぶことにする。「やること」と「やる主体」の違いしかな…

プロトキン／パワーの定式化自体は分かんなかったが、背景の一般概念のほうは利用価値がある。スピヴァックのスキーマ理論とも関係する。アドレスとは区別してロケーションというものを考える。アドレスがアドレス空間の“点”であるのに対して、ロケーション…

Gordon Plotkin and John Power "Notions of Computation Determine Monads" を眺めたが、これは分かりにくい。なんでこんな定式化するのかの意図が読めない。なんか別な定式化があるはずだ。

Global State（ストレージ）を特徴付ける7つの公理 - 檜山正幸のキマイラ飼育記 メモ編 プロトキン／パワーのストレージ代数 - 檜山正幸のキマイラ飼育記 メモ編 フロベニウス半群 - 檜山正幸のキマイラ飼育記 メモ編 フロベニウス加群族 - 檜山正幸のキマイ…

Global State（ストレージ）を特徴付ける7つの公理 - 檜山正幸のキマイラ飼育記 メモ編 プロトキン／パワーのストレージ代数 - 檜山正幸のキマイラ飼育記 メモ編 フロベニウス半群 - 檜山正幸のキマイラ飼育記 メモ編 の続き。Global State（ストレージ）を…

プロトキン／パワーのストレージ代数 - 檜山正幸のキマイラ飼育記 メモ編の続き。まず、フロベニウス代数と特殊フロベニウス代数（special Frobenius algebras）については、 http://ncatlab.org/nlab/show/Frobenius+algebra http://ncatlab.org/nlab/show/…

ストレージ代数の公理は次の記事で引用している。 Global State（ストレージ）を特徴付ける7つの公理 - 檜山正幸のキマイラ飼育記 メモ編 モノイド、コモノイド、双モノイド、加群、余加群、双加群と入れ替え（スワッパー）の文脈で考える必要がある。これは…

「オートマトンの圏」は色々に定義できる。色々有り過ぎて困る。優劣を論じるより、使い分けるという話だ。オートマトンを対象、トランスデューサーを射とみなすのは、模倣／双模倣の解釈に役立つ気がする。この解釈では、射が単なる状態空間の対応ではなく…