…するのがカザネスク／ステファネスク／ハイランド／長谷川〈Cazanescu-Stefanescu-Hyland-Hasegawa〉の定理です。これについては以下の過去記事で触れています。 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 トレース付き対称モノイド圏とはこんなモノ アフィン型不動点方程式圏 $`\cat{C}`$ の対象 $`X`$ は、順序だけでなくて足し算も備えているとします。つまり $`\quad (+):X\times X \to X …

…圏です。カザネスク／ステファネスク／ハイランド／長谷川の定理によると、不動点方程式が解けるデカルト圏はトレース付きデカルト圏〈traced cartesian category〉と同じことになります。このことについては、以下の記事を参照してください。 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 トレース付き対称モノイド圏とはこんなモノ letrecと不動点方程式とトレース付き圏 その他 ステファネスク, 長谷川 の検索結果 デカルト圏 が圏論的トレース…

…圏なら、カザネスク／ステファネスク／ハイランド／長谷川の定理より、不動点オペレーターはトレースと同じことになります。ここいらのことは： トレース付き対称モノイド圏とはこんなモノ トレース付きモノイド圏の新しい定義 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 不動点理論と対角自然性（dinaturality） 不動点の対角自然性（dinaturality）はやっぱり五角形可換らしい 半加法構造（双積）とデカルト構造はうまく両立しない（たぶん）ので、カザネ…

…で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 トレース付きモノイド圏の新しい定義 こんな簡単なトレース付きモノイド圏があったなんて トレースのタイトニングが自然変換であること 不動点理論と対角自然性（dinaturality） 不動点の対角自然性（dinaturality）はやっぱり五角形可換らしい CADGの微分オペレータ（微分コンビネータ）については、いずれまた述べる機会があるでしょう。モナド、デカルト圏、コンパクト閉圏 モナド モナドの定義には、クライ…

…年代にはカザネスクとステファネスクが精力的にフローチャート（フローノミアル→ネットワーク代数と名前を変えて）理論を整備しています。トレース付きモノイド圏（traced monoidal category）としては、90年代にハイランド、長谷川などが不動点理論を完成させています（「トレース付き対称モノイド圏とはこんなモノ」、「絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」」参照）。「フローチャートを復権させよう -- 2020年代のプログラミングへ」より： …

…で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 最後に、最近見た壮絶な絵算（サーフェイス図による証明）の例：この絵は、次の論文から取ったものです。こういった絵が山のように載っています。こりゃ、ついてけない。 Gray categories with duals and their diagrams John W. Barrett, Catherine Meusburger, Gregor Schaumann URL: http://arxiv.org/abs/…

…で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」」にあります。クリーネ代数を再現するには、トレース付きデカルト圏では構造が不足で、追加の仮定が必要です。その仮定とは； デカルト積が双積になっており、始対象と終対象が一致する（零対象が存在する）ことです。零対象と双積を持つ圏を半加法圏と呼ぶので、この仮定があると、トレース付きデカルト半加法圏を考えることになります。トレース付きデカルト半加法圏でクリーネ代数が再現できることは、「トレースを使ってクリーネスター（または…

…ですね。カザネスク／ステファネスク／ハイランド／長谷川の定理により、直積に対する不動点演算子からトレースを定義できるので、「エンドセットのスター演算→圏全体のトレース」という構成ができるのです。ここらの事は、昨日も引用した次の記事にだいたいは書いてあります。 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 予定： クリーネスター・圏論・計算の離散力学 再考： クリーネスター・圏論・計算の離散力学 テストの代数は絞り出せない？前節で仮定したような圏 (C, …

…で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 予定： クリーネスター・圏論・計算の離散力学 再考： クリーネスター・圏論・計算の離散力学 Testsはどうなるのかテスト付きクリーネ代数のテストとは、論理式、条件、命題、真偽値などと同じ意味です。なんらかの論理計算の体系です。テストの代数としては、通常はブール代数を仮定します。しかし、もっとゆるくハイティング代数がふさわしいときもあるでしょう。テストの代数を外側の圏から導くのはけっこう難しい気がします。エンドセ…

…SHH（カザネスク／ステファネスク／ハイランド／長谷川）定理によりトレースを構成可能です。つまり、ωCPO⊥はトレース付きデカルト圏、ωICMはトレース付き双デカルト圏です。「ゾゾウスキ導分とゾゾウスキ共役」で出した、言語に対する左連接オペレーターLαやゾゾウスキ導分Dαは、ωICM内の射として解釈可能です。ゾゾウスキ共役（随伴）の議論をするには、ホムセットに順序構造が必要ですが、ωICMのホムセットは標準的な順序構造を持ちます。LαとDαは共役（随伴）対なので、 Lα(Dα…

…SHH（カザネスク／ステファネスク／ハイランド／長谷川）定理です。行列圏を典型とする双デカルト圏という設定のなかでは、トレース、不動点オペレーター、クリーネスター（コンウェイ代数）という構造が同じものであり、なにかの量を計算したいときに、どれを使ってもいいことになります。その一例がクリーネスター／クリーネプラスをトレースを使って計算することです。そしてそれから1/(1 - a) = 1 + a + a2 + ... という“等式”は、僕にとってはもの凄く不思議で、なんとか解釈…

…圏です。カザネスク／ステファネスク／ハイランド／長谷川の定理（KSHH定理）により、トレースと不動点演算子の構造が同値であることが分かるので、「不動点演算子を持つデカルト圏 ＝ トレースを持つデカルト圏 ＝ コンウェイ圏」となります。 参考： 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 双対的に、余不動点演算子を持つ余デカルト圏を考えると、これはトレースを持つ余デカルト圏と同じことになります。トレースは自己双対的な概念なので、余トレースとトレースを区別…

…すね。「カザネスク／ステファネスク／ハイランド／長谷川の定理」によると、トレース付きデカルト圏では、不動点方程式の解はトレースを使って書き下すことができます*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付きラムダ式はトレース付きモノイド圏の射としての解釈を持つので、フローチャートで図示できます。…

…中盤でもエルゴットやステファネスクのように積極的にフローチャートを研究した人もいますが、基本的な道具であるトレース付きモノイド圏／前モノイド圏（traced monoidal category/premonoidal category）が一般化したのは1990年代から今世紀に入ってからです。トレース付きモノイド圏に関連することは次の記事と、そこからのリンク先で触れています。 トレース付き対称モノイド圏とはこんなモノ Webサービスの設計：リンク集＋お絵描きWeb設計 フローチ…

…で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 データ・コード双対性、エルゴット繰り返し、ツインコードスタック抽象機械 あんまりタチの良くないgoto文もCPS（継続渡し方式）変換でだいたいは説明が付きます。 CPS（継続渡し方式）変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ CPS（継続渡し方式）変換で裏返る理由 マイク・ステイ（Mike Stay）が指摘しているように、CPS変換は米田埋込みです。この解釈を採用するなら、goto…

…で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」」にて： トレースについて今は説明しませんが、次のような公理で特徴付けられます。 バニッシング（アクション性） タイトニング（自然性） スライディング スーパーポージング（強度性*1） ヤンキング たまたま次の論文で、トレース付き対称モノイド圏の絵を見つけたので、少し説明します。 Title: Diagrammatic Representations in Domain Specific Languages (20…

…年代末にカザネスク／ステファネスク（Cazanescu, Stefanescu）により認識されていました。ハイランド（Hyland）も同じことを述べているようです。一般的かつ完全な記述は、長谷川真人（はせがわ・まさひと）さんにより与えられました。絵算f† := [∇;f]← と f*>0 := [f;Δ]† に対して、逆向きの公式を絵で与えます。 定義：f† := [∇;f]← 逆向き：f← := (A+iX);[(f+iA);(B+σX,A)]† 定義：f*>0 := [f…

…ャート研究の第一人者ステファネスク師匠の半環圏（semiringal category）と同じ概念なのでした。不思議な因縁を感じます。 僕がエフイチにハマる打算的理由（と、ステファネスク師匠） コンヌとマニン僕がエフイチを知ったキッカケはコンヌ／コンサニ（Alain Connes and Caterina Consani）の論文Characteristic 1, entropy and the absolute point でした。そのコンヌと、（コンヌと親交がある）マニンは…

…た人が、ルーマニアのステファネスク*2（Gheorghe Stefanescu）です。「プログラムの算術的計算法 (続き＆完結）」の最後「計算法と図解法」に、ステファネスクの名前が出ていたりもします。ちなみに、ステファネスクさんは、九州大学に客員教授でいたことがあるそうです。 Gh. Stefanescu. On Flowchart theories I: The determinisitc case. Journal of Computer and System Scien…