このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ステファネスク, 長谷川 の検索結果:

型理論が気持ちよく出来る圏とは

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

マイクロコスモ原理とクリーネ構造

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

圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却

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

「フローチャート」騒ぎ、もう少し頭使って考えてみようよ

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

絵算のススメ 2015 年末版

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

クリーネ代数への批判と賞賛: プログラムのモデル色々

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

クリーネ代数の「テスト」を圏論的に定義できるだろうか?

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

クリーニ代数と圏論

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

ωCPO(可算完備順序集合)で考える形式言語理論

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

トレースを使ってクリーネスター(またはクリーネプラス)を計算する方法の概略

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

予定: クリーネスター・圏論・計算の離散力学

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

letrecと不動点方程式とトレース付き圏

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

フローチャートを復権させよう -- 2020年代のプログラミングへ

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

goto、大域変数、例外、双対性

…で見る「カザネスク/ステファネスク/ハイランド/長谷川の定理」 データ・コード双対性、エルゴット繰り返し、ツインコードスタック抽象機械 あんまりタチの良くない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…