…) in Set) 不動点オペレータ |C|×|C∋(X, A) (FixXA:C(AX, X) → C(A, X) in Set) デカルト微分コンビネータ |C|×|C|∋(A, B) (DA,B:C(A, B) → C(A×L(A), L(B)) in Set) （Lは線形化コンストラクタ） カリー化オペレーター |C|×|C|×|C|∋(A, B, C) (CurryA,B,C:C(A×B, C) → C(A, [B, C]) in Set) デカルト・ペアリング |…

…上の対蹠写像の唯一の不動点です。つまり、￢0 = 0 。NP0は、集合としてはZと区別が付きませんが、Zとは異なる順序を入れます。次の図で、線で繋がれていて上にある要素のほうが“大きい”とします。この順序は全順序にはなりません。NP0のこの順序構造を頭に焼き付けてください。NP0内で、μ以下の極性付き自然数達（ただし0は除く）は区間の形になります。この区間が〚μ〛です。 For μ∈NP0, 〚μ〛 := {a∈NP0 | 0＜ a ≦μ} 集合の定義のなかでラテン文字'a'…

… (-)* に対する不動点がレヴィ・チビタ接続になっています。期待多様体 再論期待多様体とは、統計的文脈で登場する情報多様体、つまり統計的情報幾何で扱う対象物です。「期待」という形容詞はニールセンによりますが、「期待値が絡んでいる」ことを示唆しています。期待値の値（実数値）より、期待値を対応させる作用素が問題になるので、この話を先にします。状況設定は次のよう： (X, ΣX, Λ) を測度空間とします。測度Λは確率測度とは限りません。記号の乱用で X = (X, ΣX, Λ)…

…があります。最小な前不動点は不動点になるクリーネ代数もコンウェイ半環も、最小不動点を扱う代数系だと言えます。最小不動点と最小前不動点に関して次のように書きました。 最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同じなので、次の2つの条件を満たすtは最小不動点となります。 「同じ」という言い方は誤解をまねくかな、と思って次のように修正しました。 最小不動点〈least fixed point〉…

…何か 順序構造と最小不動点 クリーネ代数の定義 可換性とベキ等性 コンウェイ半環 何に使えるのか／何に使いたいのか「クリーネ代数〈Kleene algebra〉とは何か」の前に、クリーネ代数は何に使えるのか？ 僕が何に使いたいと思っていた／いるのかを説明します。僕が想定している用途は主に2つで、 プログラム意味論 形式言語理論 です。今ここではプログラム意味論のほうだけ述べます。クリーネ代数は、非決定性プログラムの記述と分析に使えます。だいぶ古いですが、次の3つの記事を読むと…

…に対するアフィン線形不動点方程式 x = ax + b は、常に唯一の最小解を持つ。 b = 1 の場合の不動点方程式 x = ax + 1 の解を a* と定義することによりクリーネスターは後から導入できます。アフィン線形不動点方程式は1次方程式（の特殊形）なので、多次元化したくなります。連立の不動点方程式は次の形になります。 x1 = a1,1x1 + ... + a1,nxn + b1 ... xn = an,1x1 + ... + an,nxn + bn クリーネ代数…

…意味とは思いません。不動点や終対象は、そのような状況に意味を与えてくれることがあります。しかし、今考えている「Q(r) ⇔ 階数rの対象物にモノイド構造が定義できる」の文脈では、rを無限に大きくしていくことは（僕には）考えにくいです。有限な自然数Nに対してQ(N)を確定させて、逆帰納ステップを止めることを考えます。どうやって止めるか？ 考えられる候補は次のようなものでしょう（他にも在るかも知れないけど）。 Q(N)は、経験的・直観的*3に明らかだとする。 Q(N)を、より単純…

…2-は、Ψの対称面（不動点集合）に対して鏡映の関係にあります。当然に、O2+ = SO2 とO2-は図形として合同です。O2の形状とパラメータ表示O2 = O2+∪O2- の、R4内の図形としての位置・形状をハッキリさせましょう。もう一度O2の定義方程式を確認します。 1番目と3番目はどちらも円周の方程式ですが、1番目はx1-x2平面内の円周、3番目はx3-x4平面内の円周です。よって、1番目と3番目の方程式の連立方程式系の解集合はR4内のトーラスになります（以下の箇条書きと…

…あります。トレースや不動点オペレータは、関手・自然変換ではないけど重要な圏論的構成素です。非関手的対応、非自然な変換も積極的に使いましょう。内容： 圏論的コンストラクタと圏論的オペレータとは何か 関手・自然変換の一部を見ているとき トレース、不動点、微分 モナド、デカルト圏、コンパクト閉圏 モナド デカルト圏 コンパクト閉圏 おわりに 圏論的コンストラクタと圏論的オペレータとは何か最近、CADG（Categorical Abstract Differential Geomet…

…ランド、長谷川などが不動点理論を完成させています（「トレース付き対称モノイド圏とはこんなモノ」、「絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」」参照）。「フローチャートを復権させよう -- 2020年代のプログラミングへ」より： 1990年代以降、トレース付きモノイド圏／前モノイド圏の計算科学への応用は長足の進歩をしました。いまや、フローチャートは科学として扱えるのです。再びプログラミンミングの有効な道具としてフローチャートがカムバックする準備は出来てい…

…カルト圏では、再帰や不動点の議論ができます。この事実を明らかにしたのは長谷川真人さんです。長谷川さんの論文・スライドへの参照は「フローチャートをめぐる迷信と妄言と愚昧」の真ん中へん、「関数型言語では、フローチャートは書けない?!」のセクションにあります。長谷川（と先駆者達）の定理の簡単な紹介は「絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」」にあります。クリーネ代数を再現するには、トレース付きデカルト圏では構造が不足で、追加の仮定が必要です。その仮定とは；…

…X→Z） という領域不動点方程式を解かなくてはなりません。いや待て待て、領域不動点方程式なんて解きたくねーよ、となるでしょうね、ふつー。するとカタヅケ主義者は、「だったら、y = y(x) なんて書くんじゃねーよ」と文句をたれるわけです。こういう発想と反応は、一種のコミュニケーションの障害なのではないか、という気もします。コミュニケーション障害の症状のなかに次のようなものがあります（http://www.tsubasa.kitaq-src.jp/2/hatttatushoug…

…カラー）です。行列の不動点方程式（文法に相当する）の解が、適当なオートマトンによりφAA*ιAの形で書けることが、正規言語の理論の中核的事実でしょう。オートマトンは、言語の生成系であると同時に言語の認識系でもあります。与えられた語xが言語Xに所属するかどうかをオートマトンで判定できます。言語の生成と認識は、ある種の双対性（随伴性、共役性）があるようです。この双対性を理解するには、ゾゾウスキ導分を使うのが良いのではないかと思っています。 http://d.hatena.ne.j…

…イスター）から圏論的不動点演算子（コンウェイダガー）を作ることができます。f:A×X→X に f†:A→X を対応させる演算が不動点演算子＝コンウェイダガーですね。カザネスク／ステファネスク／ハイランド／長谷川の定理により、直積に対する不動点演算子からトレースを定義できるので、「エンドセットのスター演算→圏全体のトレース」という構成ができるのです。ここらの事は、昨日も引用した次の記事にだいたいは書いてあります。 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理…

…が、再帰、繰り返し、不動点、結び目などと関係することは次の記事で言及しています。 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 予定： クリーネスター・圏論・計算の離散力学 再考： クリーネスター・圏論・計算の離散力学 Testsはどうなるのかテスト付きクリーネ代数のテストとは、論理式、条件、命題、真偽値などと同じ意味です。なんらかの論理計算の体系です。テストの代数としては、通常はブール代数を仮定します。しかし、もっとゆるくハイティング代数がふさわしいと…

… に対して、fの最小不動点 p∈P、f(p) = p が存在する。 fの最小不動点は、⊥≦f(⊥)≦f(f(⊥))≦ ... の上限で与えられる。 もう少し一般化して、f:C×A→A に対して、c∈C を固定しての最小不動点p、f(c, p) = p を構成することができて、c|→p という対応もωCPO⊥の射となります。さて、ωICM⊆ωCPO⊥ なので、ωICMでもナスター／タルスキーの定理やその拡張が成立します。しかし、ωICMの射は最小元を保つので、f(⊥) = ⊥ …

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

…定義されるfに対して不動点方程式 x = f(t, x) を解きます。このxはパラメータtに依存するので、より正確には、 x(t) = f(t, x(t)) という形ですね。ちょっと計算すれば、x(t) = (1/(1 - a))・t だとわかります。ここで出てきたtの係数 1/(1 - a) がクリーネスターに相当する量で、実際 1/(1 - a) = 1 + a + a2 + ... = (aのクリーネスター) という無限級数展開を持ちます。収束とかは気にしないことにしま…

…コンウェイ圏（つまり不動点演算子を持つ） デカルト圏に余デカルト性を足して双デカルト圏（双積を持つ自己双対的な圏）の話にすると： Cはトレース付き双デカルト圏 ⇔ Cは双コンウェイ圏 双デカルト圏の典型例は（適当な係数半環上の）行列の圏なので、行列圏に特殊化すると： Cはトレース付き行列圏 ⇔ Cはコンウェイ行列圏 同値性（⇔）の半分だけにして、 Cはトレース付き行列圏 ⇒ Cはコンウェイ行列圏 とすれば予備知識は減らせるでしょう。でも、こうするとコンウェイ代数（コンウェイ半…

…f:X→X に対する不動点は、ミュー記号を使って μx.t のように書きます。ここでtは、関数ｆを表現する項（term）で、変数xは、変域Xを走ると想定しています。項tに自由変数aが含まれるなら、f:A×X→X のように考えて、μx.t はAでパラメータ付けされた不動点族 A→X を表すと考えます。letrecは、μx.t を使いやすくした形で、g:X→Y という後続する関数を一緒にして、g(μx.t) を letrec x = t in s と書くのです。sは関数gを表す項…

「不動点理論と対角自然性（dinaturality）」において次のように書きました。 「ほんとに対角自然変換なのか？」と疑わしくなってきました。ここからの話は、いちおう辻褄は合っていると思いますが、僕が何か勘違いをしている可能性もあります。なかなかうまく行かないので、変換の定義を少し変更してみる話です。αが満たすべき条件は六角形ではなくて五角形の可換図式となります。 fixed-point、dinaturality とかで検索していて、次の論文を見つけました。 Title: …

…のタイトニング公式と不動点に関するタイトニング類似の公式が、ある自然変換の自然性（naturality）の記述であることを示しました。不動点演算子の公理には、もうひとつ「対角自然性（dinaturality）」と呼ばれる等式があります。自然性が自然変換の定義であるのと同様に、対角自然性は対角自然変換（dinatural transformation）の定義となります。不動点演算子の対角自然性も、実際に対角自然変換が存在することを主張するのだろう、と思っていました。確認してみる…

…とするパラメータ付き不動点演算子は、FixAX:C(A×X, X)→C(A, X) というホムセットのあいだの写像として与えられます。不動点演算子Fixでも、タイトニングとよく似た等式が成立しますが、これも自然性です。問題の等式は、f:A×X→X、h:A'→A として、FixA'X((h×X);f) = h;FixAX(f) の形です。これは、φA = FixAX と置いて、(h×X)*;φA' = φA;h* と書けます。可換図式では： C(A×X, X) -(φA)-->…

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

…関数を定義するための不動点コンビネータを定義することもできず、（それが高階でなくても）再帰的に定義された関数を扱えません。再帰的な関数定義を許すための仕掛けがモジュールです。モジュールとは、名前を付けたラムダ項の集まりです。ここで名前とは変数記号のことです。uがアリティnの変数（u∈Vn）、tがアリティnのラムダ項として、ペア (u, t) が「名前を付けたラムダ項」ですが、(u, t) を def u t とか u := t とか書けばより馴染み深い記法となるでしょう。モジ…

…- いや、let式や不動点演算子などの議論はラムダ計算から拝借したいのです。というわけで、高階には登らないようなラムダ計算を定義してみます。記事のタイトルに「(1)」が付いてますが、実を言うと、この記事と類似の内容は何度も話題にしたことがあります。以下の記事などです。 樹形タプルの世界 高階関数を持たないが型の順序を持つラムダ計算 CatyScriptと総称ラムダ計算 これらの記事との連続性は無視して、仕切り直しに近いので「(1)」と番号を付けました。僕の感触では、アリティ付…

…定義される関数の最小不動点を表す μx.E も束縛子です。最大不動点なら νx.E ですね。これらは、ラムダ束縛を省略した書き方とみなせるので、本質的な束縛子はラムダ記号です； μx.E ≡ μ(λx.E)、νx.E ≡ν(λx.E)。積分記号∫、総和のΣ、総積のΠなども束縛子記号です。極限 limx→∞f(x) のlimも束縛子で、この例のxが束縛変数になります。「束縛子」という言葉を使うと、色々な構文的作用素の共通性を言い表すことができて便利です。 *1:正確に言えば、自…

…つかというと、それは不動点方程式の解を与えるからですね。「カザネスク／ステファネスク／ハイランド／長谷川の定理」によると、トレース付きデカルト圏では、不動点方程式の解はトレースを使って書き下すことができます*1。具体的には、f:A×X→X の不動点は、Tr(f;Δ):A→X で与えられます。ここで、Δは対角です。余単位!と対角Δを持つ対称モノイド圏がデカルト圏なのでした。特に、A = 1 なら、f:X→X とみなしてよく、f;Δ:X→X×X で Tr(f;Δ):1→X となり…

…許すletの意味論は不動点になります。このことから、fixpointなんて露骨なキーワードを使う例もありますがどうなんでしょう？ 分かりにくいと思いますね。不動点演算子はギリシャ文字μが使われるのでmuは？ もっと分かりにくい！「let 束縛 in 式」の順番を変えた書き方に「式 where 束縛」があります。どっちも同じ意味で書き方の違いだけです。それじゃwhereなんて要らないのか、というと、letよりwhereが便利な状況もあります。で、僕はよく知らないのですが（誰か教…

…再帰的定義の意味は、不動点で与えられます。モノイド積がデカルト積である対称モノイド圏では、不動点の存在とトレースの存在が同じことになります。そしてトレースは、図ではフィードバックサイクルになります。このことを厳密に示したのは長谷川さんご自身です。檜山による稚拙な解説なら： トレース付き対称モノイド圏とはこんなモノ 絵算で見る「カザネスク／ステファネスク／ハイランド／長谷川の定理」 羽生さんの講演で示されている典型的な次のフローチャート、これのフィードバックサイクル（繰り返しの…