圏上のチェーンの畳み込み積 - 檜山正幸のキマイラ飼育記 (はてなBlog) モノイドと圏はやっぱり似ているね - 檜山正幸のキマイラ飼育記 (はてなBlog) もう一度ちゃんと考える価値がある。

総称ラムダとかを参考にすると、次のようになる。ただし、これは厳密結合の推論で、型制約が出てこない。残念ながら、これでは実用にならないが、キレイにまとまる感じはある。S, Tなどは型項（または型表現）、f, gなどはコマンド項、M, Nなどは式（formula…

ベックの法則の定式化がけっこう分かってきた。これはさすがに書いておかないとな。忘れるからな。基本的に（メンタルに）想定しているのは多元環Rと加群Mなんだが、モノイドとモノイド作用なら何でも同じこと。ここでは、モノイド構造さえ考えないでマグマ…

http://www.cs.cornell.edu/~kozen/papers/papers_collapsed.htm ここからいろいろな論文が取れる。set expressionはtype expressionで、set constraintsはtype constraintsだから、そのまま型推論に使える。しかし、termset代数が、エルブラン方式理論であ…

左←→右 は、同じ圏のなかでの双対性、ただし、右は非決定性（ND）な圏なので、決定性の圏を非決定性の圏に埋め込んで双対を考える。上←→下 は、直積・直和の双対性から導かれる対応。異なるモノイド圏のあいだの対応関係（関手ではない）。 ＼ 自明な構造 非…

ステファネスクに従って、用語法をデカルト分配圏からデカルト半環圏（cartesian semiringal category）に変える。記号の説明： θ -- 空集合を域とする唯一の射 ι -- 標準入射 ∇ -- 直和のフォールド＝余対角 λ -- 左unitor自然同型 ρ -- 右unitor自然同型 α…

注意：distributorは用語的に問題があって、distributivityとか言うほうが望ましいだろう。が、-er, -or って語尾はコンピュータ／ソフトウェア屋さんは好きだから、distributor使う。まず普通の足し算に関して： associator自然同型 (A+B)+C ⇒ A+(B+C) 左un…

モニャドセミナー4 資料 抜粋 ＋ 追加 - 檜山正幸のキマイラ飼育記 メモ編も参照。 足し算ぽい：ブーリアンのOR演算 -- 足し算ぽいね、うんうん 足し算ぽい：集合の合併 -- 以下同様 足し算ぽい：max, min 足し算ぽい：特に平坦束、この圏の線形写像はなにか…

「勝たす異論」じゃねーよ。型推論とかいうとつっこまれそうだから、型解析にする。問題はパイプ結合だけ。 型ユニフィケーションをして、SIL命題のセットを出力する SIL命題セットを整理、計算（簡約）する。 SIL命題セットから代入を取り出して、再帰的に…

式Eの計算が、すべての部分式の計算も含めて安全に行われる（と予測できる）とき、《E》 と書く。式Eのすべての部分式とパイプ記号には、番号（一意的ならなんでもいい）が振ってあるとする。異なる番号が同じ場所を指す可能性がある。（[追記]そんなにイッ…

これは、あくまで構文的であり、決して意味的ではないことに注意。意味的な議論は解釈を決めないとできないし、解釈は色々あり、解釈ごとに定義は変わる。基底：コマンド呼び出しと定数 Dom(f::S -> T) = S Dom(c) = null Cod(f::S -> T) = T Cod(c) = sing(…

「文字列（名前）の集合と非負整数値」の組をシグニチャと呼ぶ。次の形で書く； {"foo", "bar"; 2}, {; 3}, {"baz"; 0}, {;0}。シグニチャパターンはオプションシグニチャパターンと引数シグニチャパターンの組である。オプションシグニチャパターンは： 文…

カロウビ展開圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)のコピー与えられた圏Cに対して、新しい圏Kを作ります。その作り方を順に述べます。まず、Kの対象は、Cのベキ等射とします； a∈|K| ⇔ aはCのベキ等射 ⇔ a;a = a inc C。Kの射 f:(A,a)→(B, b) は次の…

モノ（値）かコト（事態、動作）か モノとコトの相互変換 soft-nothing と hard-nothing ⊥の追加、厳密射、リフト 結局は、バンドルと層を使うことになるな。 集合圏の始対象／終対象の非対称性 関数と関数型（べき、指数） 特異値と非特異台 外延的記法によ…

代数幾何の枠組みを他分野に応用するには、ガブリエル／ローゼンバーグ（Gabriel Rosenberg）の再現定理（reconstruction theorem）というのがどうも鍵らしい。可換環からなにやらかにやらして作ったアーベル圏から、もとの環を再構成できる、ということらし…

http://d.hatena.ne.jp/m-hiyama/20061115/1163573135