有向グラフで、in-degreeが0のノードを湧き出しノード（source node）、out-degreeが0のノードを吸引ノード（sink node）と呼ぶ。sourceがチトまずい言葉だと思うが、日本語なら問題ない。湧き出しでも吸引でもないノードを流動ノード（fluent node）と呼ぶ…

ケーニヒスベルクの橋の問題は、だいたいポアンカレ双対。

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

どうにもならないなーー(溜め息)「除去規則の適用」のレゾリューションアルゴリズムの圏的意味論を考えてみたが、これは複雑。なのに、Isabelleのなかでは天下り。これでは納得出来るわけがない！それはそうと、ポールソンは、メインゴールとサブゴールズと…

自然演繹の正規形定理は、直和を持つデカルト閉圏の等式的な公理系から出てしまう。つまり、直和を持つデカルト閉圏を計算するシステムのなかに自然演繹は埋め込めて、正規形定理は埋め込み先では自明になってしまう。自明になってしまうのだけど、そこまで…

1994年のGentle Introductionとか読むと、処理系の発展・進化はいいとして、説明や教育に関しては、退行した感がある。かつては強調されていた諸点が今は触れられなくなったのは、そのことがコミュニティの内部で常識化したせいだろう。が、新参者にとっては…

IsabelleやCoqだけを責めることは出来ないな。論理学の用語や概念が曖昧だったんだよな。ものごとをハッキリさせるはずの学問が曖昧な記述で済ませていた。だから、ソフトウェア実装でも曖昧な概念と用語法が引き継がれ、混乱がより悪化した、という事情だろ…

propositin, fact, goal と並べて書いてあるのを見て、ひょっとして、と思った。 propositionとは、真偽の判定を伴わない単なるexpression、つまり論理式のこと factとは、propositionに |- のマークが付いたもの。つまり、判断主張文。 goalとは、propositi…

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

モノイド圏上の加群圏の実例 - 檜山正幸のキマイラ飼育記 僕が加群圏にちょっと興味をいだいたのは、変則的なラムダ計算のモデルとして加群圏が使えないかな？ と思ったからです。思っただけで、よく分かってません。 よく分かったぞ。少なくとも「積分を入…

総和完備な半環上の加群の圏を考えて、加群も和に関して完備、写像は総和連続だとする。そのような圏では、クリーネスターが自動的にクリーネスターに移るので、クリーネスターを意識する必要がない。意識する必要がないので忘れていたが、単に半環／多元環…

いまだに植木算で間違う。印刷指定の多くは、印刷開始ページと終了ページを指定する。「14ページから10枚印刷する」と頭で考えて、「開始：14, 終了：24」とやってしまった。14 -- 24 だと11枚印刷される。区間の両端は、a≦ x ＜ b が自然なのかも知れない。

Seq(C)とPoly(C)はアルファベット（または指標）で相対化する。アルファベットの構成要素は、 |C| の有限部分集合V Mor(C| の有限部分集合E dom, codをE上に制限したときに、(V, E)が有向グラフになることが条件。さらに関係の有限性を入れる。 Cにおいて(V,…

記法を変える。PolyFull(C)じゃなくて、Seq(C)にする。 Seq(C)は単なる圏。その対象を列（シーケンス）、その射をシーケントと呼ぶ。 Seq(C)のモノイド積（連接）は、# と書く（++, ##の略記）。 |Seq(C)| = |C|* Seq(C)(Γ, Δ) C(Prod(Γ), Prod(Δ)) シングル…

やたっ、これでうまくいきそう。Poly(C)の構成の方針 - 檜山正幸のキマイラ飼育記 メモ編の続き。地獄のHerculean taskを回避できそう。Poly(C)の構成の要点は： Cに部分対称構造（partially symmetric structure/system）を導入する。 Poly(C)とCの中間にPo…

A×(B + C) = (A×B) + C これは分合律（dissociative law, linearly distributive law）。 A×(B×C) = (A×B)×C なら通常の結合律。別な演算*があって、 A * (B×C) = (A * B) * C ならなんと呼ぶか？ * を含意＝指数だと思うと、これはカリー同型。分合律やカリ…

絵素： お絵描きの基本素材 絵図的操作： 絵素の組み合わせ方や絵素の変形加工法、構成的・作業的 部品： 与えられた基本の絵素から絵図的な操作で作ったモノ。後で使うためにストックする。 神託： 絵図的な操作で作れないものを作ってくれる神様がいるので…

Xを平面内でX軸に対する鏡映、XをY軸に対する鏡映とする。 平面に置かれたカードに対して、FはX軸中心の裏返し（フリップ）、Rは180度の回転とする。 Sをスター関手、Dをダガー関手とする。 いずれも、生成元が2つで同じ関係を持つ4元の群となる。 XX = X, Y…

箱入りのタングルを考える。箱は例えば3次元として、上下の矩形内にn個の点をバラまいてタングルの境界とする。タングルの境界点（マーク点）に圏Cの対象、ストランドに圏Cの射を対応させて、iCラベル付きタングルと呼ぶ。Cラベル付きタングルは、構文的な存…

*は任意のマルチインデックス、x, yは極性の符号、**は任意の極性付きマルチインデックス 射 ポリ行列 圏の射 極性なし、1→1 シェイプ 複圏の射 極性なし、*→1 シェイプ 多圏の射 極性なし、*→* シェイプ 双対付き圏の射 極性あり、1x→1y シェイプ 双対付き…

http://d.hatena.ne.jp/m-hiyama-memo/20160209/1454977682に書いたように、伝統的古典テンソル計算（古式テンソル計算）では、コンパクト閉圏の表現が出来ないことが分かった。ポリ行列という概念を導入する。 極性なしポリ行列 ←→ 極性なしスパイダー 極性…

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

内積付きの線形代数の定式化として、対称半リボン圏がいいような気がした。いや、いいよ、これはいいよ、非常にいいよ。まずリボン圏に関しては、 https://en.wikipedia.org/wiki/Ribbon_category https://ncatlab.org/nlab/show/ribbon+category nLabの説明…

冗談ではないよ、マジ、マジ。絵算の起源（のひとつ）は、ペンローズがテンソル計算の代替に使っていたペンローズ・ヒエログリフなのだから、古典テンソル計算が絵算で出来るのは当然なのだ。絵算の電卓ソフトとしてGlobularを使う。問題点は、Globularがラ…

本編で次の記事を書いた。 Globularのサンプルを追加： 随伴関手対と双対ベクトル空間対 - 檜山正幸のキマイラ飼育記 このての話のベースは、メイト定理だ。 https://ncatlab.org/nlab/show/mate nLabのこの記述は分かりにくいが、2-セルに関する絵を描けば…

結合律、フロベニウス律、特殊性（no-hole条件）からパヒナー（Pachner）移動が出てくることは、このダイアリーのどこかに書いておいたと思う。[追記]三角形を細分しても計算結果は同じにできる - 檜山正幸のキマイラ飼育記 メモ編 だった。[/追記]結合律の…

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

アフィン空間も一般化距離空間、指数は引き算 - 檜山正幸のキマイラ飼育記 メモ編 では、ベクトル空間を圏とみなしたが、すべてのベクトルを対象と思って、離散圏としている。モノイドMがあるとき、Mを圏とみなすために、対象類として単元集合を想定して、M…

ローヴェルの一般化距離空間では、一般化距離（≒コスト）を測るのに非負実数（∞含める）を使っている。豊饒圏の枠組みで考えれば、別な圏（ベナボウコスモス）でいいはずだ。ベクトル空間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-双加群となる。以上はよく知られた事…