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

Luigi Santocanale "From Parity Games to Circular Proofs (2002)"→http://citeseer.ist.psu.edu/santocanale02from.html (12P) にμ項の絵が在るのだが、これがまた、僕がカリー／ハワード対応をでっちあげるために描いたλ項の絵と同じなんだわ。どういうこ…

テンパリー／リーブ代数のように、図式（diagram）の同値類を基底（生成系）にして、図形の演算（境界結合、直和など）と係数の演算（主に足し算とスカラー乗法）を組み合わせてできる代数を図式代数（diagram/diagrammatic algebras）と呼ぼう。特に次元が1…

ジョーンズ関係式による定義では、恒等I:1→1、「上に∪、下に∩」であるX:2→2、ループ◇:0→0の3つが生成元になる。それに対して、恒等I:1→1、Λ:0→2、V:2→0を生成元にする方法もある。X=V;Λ、◇=Λ;V。これを逆に解こうとすると係数が必要になりそう。ん？ どうな…

テンパリー／リーブ圏のスカラーのことを書いておく。TL(0, 0)を、アブラムスキーは（抽象）スカラーと呼んでいる。スカラーは可換モノイド（可換性はケリーによる）になる。もし、圏がAb-豊饒なら可換環になることがわかる。係数なしの純幾何学的には、TL(0…

テンパリー／リーブ圏で遊ぶのは、もう単なる趣味だわな。なんか僕は、針金細工（ワイヤークラフト、ワイヤーワーク、ワイヤーアート）みたいんが好きなんだよね（http://www.d1.dion.ne.jp/~phantaz/frhow.htm 面白い）。カウフマンのブラケット関係式（一…

白旗さんのアレ（例えば、http://www.fbc.keio.ac.jp/~sirahata/Research/cmll.pdf）から推論規則を抜き出しておこう。公理は、コンパクト閉圏C（モデルの圏）から適当に選んだ射達、ただしidは全部入れる。それと、|- I（Iは単位）。CがΣから生成されている…

アブラムスキーの"Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics"（http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/tambook.pdf）をチラチラと眺めて思ったことを記す。The TLTLは固有名詞で、the Temp…

アブラムスキーの示唆は面白い。The n-Category Cafe'（http://golem.ph.utexas.edu/category/）の記事 http://golem.ph.utexas.edu/category/2007/03/computer_science_and_physics.html に、次の参照があった。 What are the fundamental structures of co…

アブラムスキーがテンパリー／リーブ代数を語る - 檜山正幸のキマイラ飼育記 メモ編 ウギャギャギャギャ、すっげー、テンパリー／リーブ圏（Temperley-Lieb categories）、モノイド閉圏だー！ しかも可換環Rに関してR加群でenrichだしぃ。こっ、これは遊べる…

線型論理とエコ経済 - 檜山正幸のキマイラ飼育記 メモ編 コピーもゴミ捨ても有料 -- 我ながらじつにまったく実感がこもった言葉だ。いずれは対称（置換）もコストがかかるのかも。こうして、コスト意識から非可換線形論理に導かれるのかもしれない。

The n-Category Cafe'（http://golem.ph.utexas.edu/category/）の記事 http://golem.ph.utexas.edu/category/2007/03/computer_science_and_physics.html 経由で知った：Abramsky "Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via …

観測子とは何であるか - 檜山正幸のキマイラ飼育記 メモ編は少し変だった。次のように考えるべき。実験観測をする側に、刺激（または信号）の履歴（または記憶）を蓄積しているデータHと、観測量または観測命題Pがある。新しい刺激・アクションaを投入すると…

避けて通っていた線形論理をほんの少しいじってみた。で、線形論理がresource sensitive/awareだって意味がなんとなくわかった。縮約規則は対角＝コピーだし、水増し規則は射影＝要るほうを抽出＝要らないほうを破棄すること。コピーもゴミ捨ても有料なのだ…

ベクトル空間の直和（むしろ、双積と呼びたいが）は、1次元空間に制限しようとしても無理だ。1 + 1 = 2 だから。しかし、テンソル積は1次元空間だけに制限できる（0次元空間を入れても大丈夫）。考えてみると、テンソル積は小学校から出てくるんだよな。速さ…

モノイド圏で、×、1とかの記号を使っていると、ついつい1を終対象だと思ってしまうことがある。そんときは、K-ベクトル空間とK-テンソル積の圏を思い出してみる。Kは終対象じゃない！ A→Kはイッパイあって、双対空間ができるよ。

ヤコブ・ルーリエは、「神様は才能を公平に分けない、極端な偏りがある」証拠となる人物だな。亜細亜の片隅のあなぐらから応援しよう、っと。田舎のオッサンが、「北島サブちゃんも凄いけど、氷川きよしね、アイツも演歌の天才だね、いいよー、きよし君」と…

高次圏まで含めた圏とは、“なんらかの意味で「きれい」な”多面体分割を与えられた図形（CW複体とか）じゃなかろうか。その図形に代数演算がたくさん含まれている。代数的な法則は up-to-homotopy、または up-to-isotopy でしか成立しない。up-to-homo/iso-to…

証明は自然演繹とする。 仮定と結論を持つ証明図（ペトリネット風グラフ） グラフ書き換え規則としての推論規則、書き換え過程としての証明行為 仮定を除く（含意導入）規則 公理は仮定と考えない 特殊ケースとしての仮定のない証明図 非形式的なシーケント…

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(Δ)とΔは同じ…

面白いことに気が付いた。Σをアルファベット（アトミック・アクションのラベル集合）とする遷移系Tがあったとする。それに、観測子（オブザーバー）φが付いているとする。φは|S|→V という写像。ここで、|T|はTの内部状態空間、Vは観測値（量）の空間である。…

うーん、随伴相方（adjoint mate）の解釈が間違っていたかも。F:C→D, G:D→Cで、D(F(A), Y)≒C(A, G(Y)) のとき、(f:F(A)→Y in D) と (g:A→G(Y) in C)が対応しているとして、fとgを相方（mate）と呼んでいるようだ。つまり、関手のあいだの関係ではなくて、圏D…

F -| G が随伴対のとき、Fに対するG（＝Fの右随伴）、Gに対するF（＝Gの左随伴）を、随伴相方（adjoint mate）と呼ぶことがあるようだ。これはいい！ が、「あいかた」って訳語はどうかな。相棒、連れ -- よけいマズイ。配偶者 -- 関係が強すぎ。カタカナ語…

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