…]）ストリング図は、トレース付きモノイド圏、コンパクト閉圏、デカルト閉圏などの計算でよく使われますが、ここでは「圏、関手、自然変換」の計算にストリング図を使う場合を扱います。「圏、関手、自然変換」をセルと呼び、それぞれ、0次元セル、1次元セル、2次元セルといいます。n次元（n = 0, 1, 2）セルを絵に描くときは、(2 - n)次元の図形を使います。n←→(2 - n) の対応はポアンカレ双対と呼ばれます。 セル セルの次元 双対次元 図示すると 圏 0 2 面、領域、エ…

…数では表せない現象 トレース付きデカルト圏とデカルト半加法圏 並列実行と同期通信 条件付き実行はどこに行った？ 時分割実行と待ち合わせ クリーネ代数は足りないけど素晴らしい プログラムの代数としてのクリーネ代数クリーネ代数が素晴らしいのは、プログラムの代数的取り扱いを可能としたことです。プログラムの組み合わせや制御方法には次のものがあります。 順次実行 選択的実行 繰り返し実行 条件付き実行 クリーネ代数による定式化では、これらの実行制御を代数演算で表します。 プログラム ク…

…, μA) に対してトレース付きの可換環を対応させるだけでなく、トレース付き可換環を最初に与えて、そこから通常の確率空間を構成することが主眼です。そこまで抽象化しないまでも、確率空間には「確率変数の代数」が付随するという発想はけっこう使われているのでしょう。L(A)の要素としての確率変数は、系の観測量（observable）とか座標に近いものです。この意味の確率変数は足したり掛けたり平均したりすることができます。 確率変数の意味その3： 適当な条件を満たす実数値可測関数であり…

…のひとつです。また、トレース付き圏、コンパクト閉圏、テンソル半加法圏などをベースに、形式言語やプログラムの意味論を展開するのも代数化のあり得る方向性です。使える方法があまりに多様過ぎて、相互の関係が掴み切れなかったり、方向が定まらないのが問題です。断片的でも面白いトピックを拾っていくのも健全なやり方かも知れません。正値TQFT（Positive TQFT）というヒントを手に入れたとはいえ、僕が使える時間も気力もごく僅かです。滞っているブログがアクティブに復活するとも思えません…

…半加法圏、テンソル・トレース付き半加法圏、対角付き対称テンソル・トレース付き半加法圏とか、形容詞が付いてダラダラした長い名前になってしまう、ウーン、しょうがないか。今日は名前が付いて良かった、ってだけ。テンソル半加法圏がプログラムとどう対応するかだけ書いておくと： 圏の対象 データ型 圏の射 プログラム 恒等射 各データ型上のnop 射の結合 プログラムの順次実行 零対象 クラッシュや無限ループ 双積の対角 非決定性の分岐（ロードバランシング） 双積の余対角 結果のマージ 双…

…さらに思いつくまま。トレース付き圏とクリーネ代数復習： 零対象と双積を持っていて、ベキ等律 Δ;∇ = id が成立し、双積に関してトレースを持つ圏Cがあれば、各エンドセットC(A, A)にクリーネ代数の構造を入れることができます。今言った条件を満たす圏になにか名前があればいいのですが、合意された名前はないようです。「クリーネ圏」という言葉はあるのですが、この条件とは違う、つうか人によって違った意味で使っていたりして安定した用語法じゃないみたい。「圏全体の構造→エンドセットの…

…どで述べています。 トレース付き対称モノイド圏とはこんなモノ トレース付きモノイド圏の新しい定義 モノイド積が双積で与えられるときは、f:A→A のクリーネスターf*を次のように定義できます。 f+ = Tr(Δ;f;∇) Tr(∇;f;Δ) f* = idA + f+ = Δ;(idA×f+);∇ このf*はクリーネスターとして期待される性質を持っています。f*は等式的（equational）に定義されています。伝統的なクリーネスター、クリーネ代数は不等式（順序）を使って定…

…つまり、ωCPO⊥はトレース付きデカルト圏、ωICMはトレース付き双デカルト圏です。「ゾゾウスキ導分とゾゾウスキ共役」で出した、言語に対する左連接オペレーターLαやゾゾウスキ導分Dαは、ωICM内の射として解釈可能です。ゾゾウスキ共役（随伴）の議論をするには、ホムセットに順序構造が必要ですが、ωICMのホムセットは標準的な順序構造を持ちます。LαとDαは共役（随伴）対なので、 Lα(Dα(x))≦x x≦Dα(Lα(x)) は成立するのですが、ゾゾウスキ共役はより強い条件にな…

…言語理論の枠組となるトレース付き圏の対合オペレーター（involution）にまで拡張すると面白そうだと思っています。より具体的に言うと、線形文法と（有限）オートマトンが同じであることは、トレース付き圏上のゾゾウスキ共役で説明できるはずです。具体的な行列計算ではそうなっているので、そのうち（忘れる前に）書きたいとは思っています。 [追記 date="当日"] そのうち（忘れる前に）書きたいとは思っています。 すぐに忘れそうだから以下に一部をメモ。トレース付き圏にいく前に、ベキ…

…ivative）を、トレース付き（あるいは不動点オペレーター付き）行列圏でキッチリと定式化できれば、1/(1 - a) に近いナニカを構成できるんじゃないかなー … とか。 Brzozowskiってどう発音するんだろう？ と、昨日Forvoの発音待ちにしておきました。「発音サイトForvoの反応が早い」にも書いたように、反応早いです。今朝には発音が登録されていました。→ http://ja.forvo.com/word/brzozowski/Brの音は聞こえないで、「ゾゾウス…

…桂さんによるご指摘。トレース付きブレイド圏で、基本ブレイド X+（下の絵の正の交差）を3つ重ねて2本の紐（全部）のトレースを取ると三つ葉結び目（trefoil knot）になると言って、絵も描きました。（http://upload.wikimedia.org/wikipedia/commons/thumb/b/b3/Blue_Trefoil_Knot.png/176px-Blue_Trefoil_Knot.png より）このとき、交差の上下（手前と奥）が逆だったようです。三つ…

…一般的な形は、 Cはトレース付きデカルト圏（つまり紐の計算ができる） ⇔ Cはコンウェイ圏（つまり不動点演算子を持つ） デカルト圏に余デカルト性を足して双デカルト圏（双積を持つ自己双対的な圏）の話にすると： Cはトレース付き双デカルト圏 ⇔ Cは双コンウェイ圏 双デカルト圏の典型例は（適当な係数半環上の）行列の圏なので、行列圏に特殊化すると： Cはトレース付き行列圏 ⇔ Cはコンウェイ行列圏 同値性（⇔）の半分だけにして、 Cはトレース付き行列圏 ⇒ Cはコンウェイ行列圏 と…

…ecと不動点方程式とトレース付き圏 letrecといえば、まさに「不動点方程式とトレース付き圏」を具現している構文なんですが、そこらへんのことは、長谷川真人さんの素晴らしいスライドで見事に解説されています。 「再帰プログラムの幾何」 http://www.kurims.kyoto-u.ac.jp/~hassei/slides15sep06s.pdf 長谷川さんのスライドの絵は「これはひどい誤解だ -- フローチャートは手続き型…だってぇー?!」でも引用しています。上のほうの …

…は、新しいスタイルのトレース付き圏（トレース付きバランス圏とその特殊化）の公理を表しています。（長谷川真人さんの "On Traced Monoidal Closed Categories", 28 November 2007 より、「トレース付きモノイド圏の新しい定義」から再掲。）ここで、タイトニング（Tightening）が自然性（Naturality）とも呼ばれています。これは、トレースが自然変換の性質を持つことですが、毎回「どこが自然なんだっけ？」と忘れてしまいます。…

…す。 行列線形代数 トレース付き圏論 力学 幾何 これら4つの観点を、それぞれノート1枚にメモしたので、ここでそれを紹介します。メモ・ノートはないのですが、このエントリーの最後に、アルゴリズムの話を補足します。登録はアテンドで： http://atnd.org/events/42643 行列線形代数 線形（線型）代数とは言っても、ベクトル空間や線形写像のような抽象的な枠組は使わないで、行列の計算を露骨（explicit）にします。足し算と掛け算だけを使う行列計算です。でも、係…

…まで格上げされると、必要な計算は縦結合「;」と横結合「*」だけです。縦結合と横結合の組み合わせのバラエティは膨大になることがあり、それが複雑さにつながっています。しかし、この組み合わせのあいだの同値性は、エレベーター規則（交替律）で統制されています。エレベーター配置の同値性は、絵の目視で比較的容易に判断できます -- それが絵算の大きなメリットです。 *1:絵算がものすごく有効だと感じるのはコンパクト閉圏のケースです。トレース付きモノイド圏、デカルト閉圏でも絵算が活躍します。

…圏 Mat[X]C が定義できます。記号の簡略化のためにこの圏をMとすると： |M| := Labeled(X, |C|) a, b∈|M| に対して、ホムセットは M(a, b) := Mat[X]C(a, b) 射の結合は行列の積 恒等射は単位行列 今日定義したMat[X]Cは単なる圏ですが、XやCに条件をつけることにより、モノイド圏や半環圏やトレース付き圏にすることが出来ます。また、ホムセットの足し算を他の構造から導き出すこともあります。行列計算はなかなか楽しいですね。

…川の定理」によると、トレース付きデカルト圏では、不動点方程式の解はトレースを使って書き下すことができます*1。具体的には、f:A×X→X の不動点は、Tr(f;Δ):A→X で与えられます。ここで、Δは対角です。余単位!と対角Δを持つ対称モノイド圏がデカルト圏なのでした。特に、A = 1 なら、f:X→X とみなしてよく、f;Δ:X→X×X で Tr(f;Δ):1→X となり単一の不動点を与えます。letrec R in E という形が、トレース付きデカルト圏でどう解釈される…

…る稚拙な解説なら： トレース付き対称モノイド圏とはこんなモノ 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 羽生さんの講演で示されている典型的な次のフローチャート、これのフィードバックサイクル（繰り返しのために戻る線）はトレースです*5。この図は（他のフローチャートも）トレース付きモノイド圏で解釈できます。ということは（直積-直和の双対で移りあうのを許して）、letrec付きラムダ式としても表現できます。逆も真で、letrec付きラムダ式はトレース付きモ…

…部分圏（ホムセットがクリーネ代数）に限定しているからでしょう。トレース付きモノイド圏やメイヤー加群の圏を使うと、より自然で柔軟な定式化ができるだろうと思います。実は、メイヤー加群をベースにしてテスト付きクリーネ代数を定義する方法を試してみたんですが、これは面白いですよ。テスト付きクリーネ代数は、プリミティブな概念じゃなくて、述語やガード条件に関する性質から構成可能な代数系のようです。 *1:正規表現の代数構造と捉えることも多いですが、こここでは非決定性プログラムの話をします。

…うに思えます。特に、トレース付きモノイド圏やコンパクト閉圏における計算では、シーケント計算を使うとラクチンです。かけ算九九をおぼえた後、二桁以上の掛け算のために筆算を習いますよね。筆算のおかげで、大きな数の掛け算も遂行できるようになります。シーケント計算は、論理と圏論における筆算のようなもんだと考えることができるでしょう。内容： シーケントとその意味 推論規則 自然演繹風の推論も一緒に使う シーケントとその意味シーケントの定義は、先日の記事「古典論理のシーケントとコマンド： …

…た、フローチャート、トレース付きモノイド圏、goto文、継続などの記事はあんまりウケなかったのに、なぜか昨日の記事はブックマークもアクセスも集めたようです。不思議だ。「正規表現」のときみたいに誰かが言及したのかな？それはそうと、ブックマーク・コメントのひとつに： フローチャートは手続き型しか記述できない。同時性や格納形式の相手が出来ない これって、3,40年前の評価ですよね*1。 時代は変わったのに、「フローチャートってダメなんだよね」とか根拠もなく盲信しているのって、なんな…

…、基本的な道具であるトレース付きモノイド圏／前モノイド圏（traced monoidal category/premonoidal category）が一般化したのは1990年代から今世紀に入ってからです。トレース付きモノイド圏に関連することは次の記事と、そこからのリンク先で触れています。 トレース付き対称モノイド圏とはこんなモノ Webサービスの設計：リンク集＋お絵描きWeb設計 フローチャートと結び目理論フローチャートは絡んだ糸のような図形です。ですから、それを扱うには結…

…ルト閉圏はもちろん、トレース付き対称モノイド圏とかコンパクト閉圏とかはよく登場するのですが、アーベル圏にはなってないのですよ。アーベル圏の特徴というと、たぶん次の2つでしょう。 足し算ができる 完全列（という概念）が定義できる 「足し算ができる」という概念は加法圏（additive category）として定式化されています。一方で、列や関手の完全性という概念が意味を持つ圏として正則圏（regular category）があります。圏のアーベル性を加法性と正則性に分解すること…

…る話は「こんな簡単なトレース付きモノイド圏があったなんて」に書いています。さて、このモノイド圏がモノイド閉構造を持つには足し算の随伴となる指数が必要です。次の同値性が欲しいわけ。 (n + m ≦ k) ⇔ (n ≦ km) ここで、km と指数の形に書いてますが、ほんとの指数（累乗）を意味しているわけじゃないですから気をつけてください。混乱を防ぐために、km の代わりに [k <- m] と書くことにすると： (n + m ≦ k) ⇔ (n ≦ [k <- m]) この同…

…は次の記事を参照。 トレース付き対称モノイド圏とはこんなモノ 単純平面タングルの圏のデモに関しては次の記事に書いてあります。 田辺さんの圏論デモ、こりゃオモロー 田辺さんの単純平面タングル（SPT）圏デモの画面ショット 代入の圏置換の圏Permをブレイドとは別な方向で一般化してみます。次の図は、Perm(3, 3) の射（3次の置換）の例を3つ挙げたものです。Perm(3, 2) は空集合（3→2 の射が存在しない）ですが、線が切れたり枝分かれするのを認めると、3→2 の射を…

…tapdf.pdf トレース付きデカルト圏におけるコンウェイ演算子の具体的表示は、f† := Tr(f;Δ) となります。Trはトレース演算子、Δは対角射です。余デカルト圏、つまり直和に関するモノイド圏を考えて、Tr'を直和に関するトレース、∇は余対角だとすると、Tr(f;Δ) の双対として Tr'(∇;f) という表示が得られます。不動点演算子の記号としては、f† のように“右肩のスターやダガー”がよく使われます。不動点演算子の双対は、左肩のダガーを使うことにしましょう。（…

…、と。使った枠組みはトレース付きモノイド圏です。コンパクト閉圏は、随分と以前から「使ってやろう」と思っていた概念です。デスクトップアプリケーションや業務システムのコンポネントの記述に使えるだろうと思っていたのです。コンパクト閉圏がWebの記述にも使えることがハッキリとしたのは割と最近。COMET（逆HTTP）がコンパクト閉圏の双対（随伴）を与えるのです。ごく最近、MongoDBの問い合わせ言語をコンパイルターゲットにすることを考えたんですが、普通の古典論理が無闇と役立ったので…

「トレース付き対称モノイド圏とはこんなモノ」で、長谷川真人さんの "Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi (1997)" http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.52.31 からコピーした絵を載せました。 法則（公理）はバニッシング、タイトニング、スライディ…

…たまたま次の論文で、トレース付き対称モノイド圏の絵を見つけたので、少し説明します。 Title: Diagrammatic Representations in Domain Specific Languages (2001) Author: Konstantinos Tourlas URL: http​://www.lfcs.inf.ed.ac.uk/reports/02/ECS-LFCS-02-426/ECS-LFCS-02-426.ps pages: 158 僕が常々面…