グラフ上に半環の値を付与して最適問題を解くのは、行列計算とお絵描きをつなぐ良い例題だ。係数をmax-plus代数にすると、時間的／空間的移動に伴い累積する値を大小比較で判定される（少ないと負け）状況を表現できる。実数区間[0, 1]のmax-times代数の場合…

なんでこんなにだるいんだ？それはともかく： 自然演繹 ラムダ計算 デカルト閉圏 ∧導入 タプリング 直積 ∧消去 射影 射影 ⊃導入 ラムダ抽象 Λと指数 ⊃消去 適用 eval T（真） ユニット型 終対象

トレースを TrA,BX:C(A×X, B×X)→C(A, B)と書くことにして、Xを固定して、A, Bを動かす。すると、Trが、C(-×X, -×X)⇒C(-, -):Cop×C→Setという自然変換になっている。この事実を書き下すと、両側タイトニング公式となる。同じようにラムダ抽象 ΛA,BX:C(A×X, B)…

本編「デカルト閉圏における絵算 詳細編」に対する等式的計算。 ○○○ = (ba×outa);eval;inb△△△ = Λa'[○○○] = Λa'[(ba×outa);eval;inb]とする。 (Λa'[(ba×outa);eval;inb]×a);[(b'a'×ina);eval;outb] = // Step1 △△△の導入と括弧の付け替え (△△△×a);(b'a'×ina)…

ちょっと考えてわかったこと： フロイド／ウォーシャル法は半環係数で考えても非常に一般的な方法だ。境界付きグラフ（リグラフ）の始境界であたえられた初期値が無限の未来に終境界にどのような影響を与えるかを計算する。ダイクストラのアルゴリズムは、始…

混乱を招くこともあるが、Haskellのセクション記法が便利なこと気付いた。 (△b) = λx.(x△b) (a△) = λx.(a△x) 特に、関数結合;に対して使うと： (;f)(u) = u;f 後結合＝前送り (f;)(u) = f;u 前結合＝引き戻し

Turaevゲームのために、参考：ラフォンは次の形をレイヤーと呼んでいる。αは基本記号で、レイヤーは最小なスライスと同じこと。 リージョンwをw'を入れ替える操作は次の図： この操作は可逆で等式に対応。一方、LLT（ランカスター／ラーソン／タウバー）のフ…

これって、メモしておいたっけ？ Title: QPL 2006 : From reversible to irreversible computations Authors: Alexander S. Green, Thorsten Altenkirch URL: http://www.mscs.dal.ca/~selinger/qpl2006/PDFS/05-Green-Altenkirch.pdf URL (2): http://sneez…

対称、または組紐が作用する圏で、ブレイディング（クロッシング、トランスポジション）と結合性（associativity）との一貫性は六角等式で示せるが、これは、ABC→CAB、ABC→BCA という左右のローテーションに関する手順独立性だとみなせる。 右ローテーション…

古典テンソル計算って、かなり綱渡りだなー。アインシュタイン規約、添字の上げ下げ、縮約は、トリッキーだがよく出来たマシナリーだなー、と感心する。が、合理化は面倒。昔、トレース付き圏の計算をそれと知らずにやっていたが、変数の扱いで散々に混乱し…

インフルエンザで高熱（39.5度）を出して脳細胞は大量死滅したであろう。まーた、よりバカになった。とりあえずリハビリしておくか（無駄だろうけど）。うーんと、諸般の事情でコレ： URL: http://academics.hamilton.edu/physics/smajor/Papers/AJP00972.pd…

「モナドと上江州拡張」にて： モナドのKleisli圏と上江州拡張はなんらかの関係があるってことだな。 項(Term)モナドと上江州拡張の関係をハッキリさせる -- これ課題。方針としては、まず、項モナド（実際は、モナドのKleisli圏）を、[0]={}, [1]={1}, [n]=…

あれれっ、あれ？ 型付き変数集合の圏の上で項モナドや項集合モナドを考えると、[x1, ..., xn]→[y1, ..., xm]のような射がKleisli射として得られる。ところが、上江州拡張でも同じ射が得られる。ということは、モナドのKleisli圏と上江州拡張はなんらかの関…

なんでXMLに上江州計算を使わなかったんだろう。ばかだなー。アンビエント・モデル圏がωCPOなんだから、使い放題なのに。式（正規表現とか）はfrom-v射だし、非再帰方程式系はfrom-v to-v射だし、トレース・オペレータτのスコープとかもλと同じだし、上江州…

Cが対称モノイド圏なら、ある程度上江州計算ができる。Xが全順序が入った型付き変数集合＝型環境（型宣言の順序リスト）なら、上江州拡張C⊆C[X]が作れるから、 from-v射（上江州さんのv→射）としての変数を含む式 式のタプル to-v射（上江州さんのv←射）とし…

「カリーをもっと -- ラムダで考えるカリー化」（http://d.hatena.ne.jp/m-hiyama/20051215/1134614762）って面白いな。自分のエントリーだけど。

Nick Benton他 A Term calculus for Intuitionistic Linear Logic →http://research.microsoft.com/~nick/tlca93.ps Masahito Hasegawa, Logical Predicates for Intuitionistic Linear Type Theories (1999) → http://citeseer.ist.psu.edu/hasegawa99logic…

変数xと型記号（ソート）Aに対して、x::A （普通はx:A）を変数の型宣言と呼ぶことにする。型宣言の集合を型環境と呼びΔ、Γなどで表す。型環境には、同じ変数の宣言が2回以上は登場しないとする。型環境に登場する変数の集合をVar(Δ)と書く。Var(Δ)とΔは同じ…

本編に次のエントリーを書いた。 モノイド圏、豊饒圏、閉圏と内部ホム - 檜山正幸のキマイラ飼育記 (はてなBlog) 閉圏、弱いラムダ計算、弱い論理 - 檜山正幸のキマイラ飼育記 (はてなBlog) で、上江州＜うえす＞流ラムダ計算ならモノイド閉圏でも定式化でき…

“古典論理＝可換環論”の計算と種明かし - 檜山正幸のキマイラ飼育記 (はてなBlog)をコピー。 MICR（乗法的ベキ等可換環）からBL（ブール束）がちゃんと作れること BLからMICRがちゃんと作れること MICR→BL→MICRでもとに戻ること BL→MICR→BLでもとに戻ること …

箱を囲んで回り込んでいるワイヤーをほどいて真っ直ぐにする操作は割と出てくる。 見た感じから、ヤンキングを使うことは予想できるが、手順は次のようにする。 クロス（対称ブレイディング）のスワップ公式で、箱をループから外に出す。 右タイトニングを使…

絵算のコツ（ダミーワイヤー） - 檜山正幸のキマイラ飼育記 メモ編の件：まず、余デカルト圏のElgot反復と、デカルト圏のConway不動点から、トレース・オペレータをもう一度作り出す絵。 律儀に、θ、σ、+（または、!、σ、×）を組み合わせて準備をしている。…

射影と入射は確かに双対だ。絵算の観点からは、どちらもダミーワイヤーを導入するときに使う。ダミーワイヤーは繋がってない（通電してない）ワイヤーで、捨てても同じ。配線の帳尻を合わせるために適宜挿入する。絵算でダミーワイヤーは必須だけど、どうせ…

ストリング図を使った絵算が少しできるようになった。Beckの分配律の公理に出てくる五角形（つうより5点四角形）2つから、スワップ結合律を示して、結合モナドの結合律が示せる。この程度なら、ストリング図で簡単。で、絵算の計算は何をしているかというと…

composite monadのassociativityをやってみた。 ストリング図のほうが描きやすく、計算しやすい。 コツは、グラフを部屋（chamber）にわけて、部屋の内部を規則でそっくり置き換える。 書き換えるべき部屋と規則を見つけるところが発見的。 分配律のBeck公理…

α:A→B :: Γ→Σ のような記法を使ったが、コロンの個数を逆にして、α:: A→B : Γ→Σ にしよう。2セルに関しては、⇒を使ったり、上に点が付いた→を使う例があるが、コロンの数＝セルの次元にすればわかりやすい。圏Catでいえば、自然変換αは、α::F→G:C→D となる。…

上江州さんは、略記、記号の乱用（オーバーロード）を多用するので、僕も真似してしまうのだが、X, Yが変数列のとき： x∈X -- 変数xが列Xに出現する。 X⊆Y -- Xに出現する変数はYにも出現する。ただし、順序はどうでもいい。 X≒Y -- Xに置換をほどこすとYに…

上江州さんは、彼の計算（それを僕が「ウエス計算」と名付けた）を、トポスを扱うときのチョッとした道具くらいにしか考えてなかったのだろう。ていねいに作ってないし、まじめに説明もしてない。でも僕は、ウエス計算はそれなりに使えると思うから、再構成…

とりあえず、はじめよう。Cは有限積を持つ圏。Vが（集合とは限らない）変数の集まり。#:V→|C|が、割り当て。#(x)∈|C|を「xの変域」（もちろん、#を仮定して）と呼ぶ。Cの適当な拡張圏C'（C=C'でもよい）があって、Vの重複を持たない有限列Xに対して、#:USeq(…

うーん、多引数・多値が全然スッキリしない。上江州（忠弘）先生が若い頃に構成した計算法があるんだが、あれを整理してみようか。ご本人も忘れているかもしれないから（1981; 25年前）、大幅に変更しても文句もでまい。2006年版上江州計算(Uesu calculus 20…