代数系の種類という意味でドクトリンを使うとして、ドクトリンの事例には次のようなものがある。 mon モノイド grp 群 cat 圏 mon-cat モノイド圏 symm-mon-cat 対称モノイド圏 br-mon-cat ブレイド付きモノイド圏 str-2-cat 厳密2-圏 これらのドクトリン（…

型クラス相当機能は分かったが、 型クラスのインスタンス化の方法が分からない。 インスタンス化に証明が伴うが、書き方が分からない。is を使って、X is C と書いて、この命題を証明するのか？

ネーミングの選択が難しいのだが、 N値の1-形式＝1-コチェインが問題。一応C1(A, N)でN値の形式＝コチェインを表す。 三角ハイブ上で1-コサイクルを考えることが出来る。コバウンダリ作用素がないが、それでも等式で定義できる。コサイクルが許容状態（addmi…

次元 多角形格子 ストリング図 ベクトル空間 0 平面の点 - - 1 辺 ワイヤー ベクトル空間 1 折れ線 ワイヤーのn本束 テンソルn累乗 1 連接 横結合 併置 テンソル積 2 格子構造 ストリング図 線形写像 2 一点接合 横結合 併置 写像のテンソル積 2 折れ線接合 …

プログラムの同値性ではなくて、プログラミング方式と実行方式のあいだのマクロな同値性を考える。例えば、時分割方式とマルチCPU方式。時分割方式のプログラムの圏とマルチCPU方式のプログラムの圏がなんらかの意味で同値となる。「なんらかの意味」は、あ…

F = (F, μ, η, τ)が強モナドのとき、テンソル強度を使ってF(1)上のモノイド構造を入れることができる。このモノイドをFの先端モノイド（apex monoid）と呼ぶことにする。ApexMon:StrongMonad(C)→Monoid(C) という関手となる。例えば、Listモナドの先端モノイ…

というわけで、プログラミング言語としてのIsabelleを調べよう。1980, 90年代の資料とMLソースコードか。現在のシステムは大規模複雑だから、MLソースコードを読むのは辛い。Isabelle86のコードとか残っているといいのだが。[追記]あった。 https://www.repo…

Pureでどうやって証明する？ 自明に思えるが、やり方が分からない。 typedecl A axiomatization f:: "A ⇒ A" lemma uniq: "x == y ==> f x == f y"

場合分けによる関数定義はどうするのか？ funとかの高級な方法使わないで。 項の計算（単純化）はどうするのか？ これもvalueとか使わずPureのレベルで。 定義（宣言）した型に対するユーザー定義の等号はどうやって定義するのか？

論理屋が論理的な語りをしない／出来ない、という現実がある。諺に、「医者の不養生」「紺屋（こんや or こうや）の白袴」とかあるけど、ちょっと違うな。他人のために尽くしていて自分には手が回らない、ってのとは違う。「儒者の不身持（じゅしゃのふみも…

基本は、滅茶苦茶、恣意的、行き当たりばったり、気分次第、その場限り、思い付きで、イイカゲン、ルール無し、である。が、たまに区別を要求するからタチが悪い！多用されて多義性が強い（オーバーロードが激しい）用語は、その意味を列挙した辞書を作るし…

「これはひどい」としか言いようがない。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]他の参考記事： 「ならば」記号の部分 - 檜山正幸のキマイラ飼育記 メモ編 論理の用語、日本語-英語 - 檜山正幸のキマイラ飼育記 メモ編…

この話題については、コボルディズム、TQFT、オペラッドとか - 檜山正幸のキマイラ飼育記 メモ編にまとめてある。上記の記事と、ルビンの壺と意味論 - 檜山正幸のキマイラ飼育記 メモ編から参照していたジョーンズ（Vaughan Jones）のスライドがドメイン（qq…

なにがミソかというと、係数（可換）半環Kが総和完備なこと。これによって、K値関数の引き戻しだけではなくて前送りが定義できる。つまり、反変関手だけでなく共変関手も定義できる。反変と共変が同時に定義できると内積と共軛（随伴）っぽい概念が使えるよ…

表現と加群は同じことだが、それを考えるために： アンビエント・ドクトリン： 世界となる圏の圏、2-圏構造を使うこともある 単対象サブドクトリン：アンビエント・ドクトリンのなかで、単対象のものだけの集まり。圏になる。 表現サブドクトリン：表現の舞…

マンダラの構造を解明するのは、生きているうちには無理だ。分からないままに死んでしまう。簡単な対象物を探ることにする。とりあえず、オートマトンの圏の基本的な構造だけに注目する。それも（たぶん）有限オートマトン。並列実行も脇に置く。難しそうな…

%.exe : %.cpp g++ -o $@ $< %.exe : %.c gcc -o $@ $

圏の指数のための中置演算子記号 - 檜山正幸のキマイラ飼育記 指数の中置演算子には随分と苦労している。 [ , ] → ⊃ ^- --o --○ ●--○ 左右の指数を区別をするときは、それぞの逆向き。指数を使ってアブラムスキーのネームとコネームを表すには4種類の記号が…

ある意味驚いた。なんとなく、コンパクト閉圏をベースにした線形代数は古典テンソル計算に翻訳できると思っていたが、表現力が足りなくて無理だった。多圏におけるストリング図をスパイダー図と呼ぶことにする。コンパクト閉圏の図では極性が必要になるので…

2009-05-01 バートレット・フリップとヤンキング - 檜山正幸のキマイラ飼育記 メモ編 ブルース・バートレットは、次の主張をしている。 双対概念は、大域的な割当として考えるべきではない。 すなわち、双対が存在するのは圏の性質であって構造ではない。 性…

2007-03-31 右ケリー双対と左ケリー双対が一致する圏：等方的剛性 - 檜山正幸のキマイラ飼育記 メモ編 任意のAに対してケリー双対系(A, R, η, ε)、(L, A, δ, γ)が存在するような圏は堅い圏と呼ぶ。 2007-04-03 平面的フィードバック - 檜山正幸のキマイラ飼…

2009-03-05 詳細は後で（バートレット、計算の世界、XML） - 檜山正幸のキマイラ飼育記 メモ編 バートレットの学位論文 "On unitary 2-representations of finite groups and topological quantum field theory" 5章を読んだ。 2009-03-05 ブルース・バート…

ワークスペース管理：これは深刻、せめてセーブ時刻を表示してほしい。 パレット内のサムネイルの順序の並べ替え。これも深刻。 パレットの内容をテキストとしてダンプ 今見てるセルのsourceやtargetを取りたい。Resrictだけでは取れないことがある。 穴あき…

双対的に反転してコピーする機能 方向の切り替え。やっぱり、上から下がいい。 描画次元が0のセルを有限な大きさ（矩形、方体）で表示する。 交替律の適用の自動的な最適化 より一般的なペースティング可能箇所の検出 プレースホルダを含むテンプレート図形…

「globular, 課題」というタグの組み合わせで、あると良さそうな機能を書く。具体的にどうするかは分からなくても、とにかくメモしていく。 ラベル以外に何らかのコメント、ドキュメンテーション 記録したワークスペースのソート、特に日付順。今、日付がよ…

モナドにおける「拡張」の補遺：アンクライスリ化かな - 檜山正幸のキマイラ飼育記 例外モナドのクライスリ圏の話。tryブロックが埋め込みJの随伴であること。これ、アイレンベルク／ムーア圏だとどうなる？ 例外モナドのアイレンベルク／ムーア代数は付点集…

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

パッケージ所属関数の親スコープは通常のパッケージの名前空間。名前空間からのサーチパスはグローバル環境に向かっている。グローバル環境より先のサーチパスは、パッケージの関数には無意味、あるいは有害だと思える。スコープチェーンは、グローバル環境…

使っている時はいいけど、使わないと忘れるのでマトメが必要だ。パッケージマネージャ的な使い方 CRANリポジトリの設定と変更 CRANのパッケージリスト CRANの検索、特定パッケージ、パターン インストールされているパッケージの一覧 特定のパッケージがイン…

過去に自分で書いた練習用のソースを読んでみる。 アットマークを多用しているが、これはなんだっけ？ Class定義で、波括弧ナシとアリでどう違う？ クラスパラメータで、中括弧はなんだ？ たしか自動的に補完するとかだったか。 アンダースコアは特殊な名前…