演繹系（証明系）を、技術者の言葉で語ることが課題。まだ、いろいろと思案中だがね。まず、基本的な態度あるいは視点としては； 演繹系も計算システムであるので、通常のコンピュータシステムやプログラミング言語システム（言語処理系と実行環境）と同じだ…

Bruce Bartlett の "Categorical Aspect of TQFTs"(TQFTはフルスペル) より： Theorem (Reshetikhin and Turaev [89]).Let (C,×, 1, σ, θ) be a ribbon category. Then the evaluation of a ribbon diagram into a morphism in C is invariant under 3d isot…

表題の言葉がいきなり頭に浮かんだ。その状況と理由は … それは後日にする。ニュートンとライプニッツのどっちが先に微積分を発見したのか？ という話があるが、歴史的に早い遅いはどうでもいい（差があっても僅差だろう）として、記号法の便利さは圧倒的に…

1次元ベクトル空間の圏に、零空間を入れても圏になる。0と1に掛け算を入れた代数系の圏化／線型化かな？零空間は1個しかないと思ってもいいし、無限にあると思ってもいい。射は同型か零写像しかない。

ボブクックが本を編集しているらしい。 http://golem.ph.utexas.edu/category/2008/09/new_structures_for_physics_ii.html バエズ／ステイの論文がリバイスされている。 http://math.ucr.edu/home/baez/rosetta/rose4.pdf 50ページからが「計算」の章。P.50…

林晋さんの論理の本（オーム社だったか）に、カリー／ハワード対応が載っていたような気がする。この本ないなー。どこだ？

"A diagrammatic approach to Hopf monads"が見つかったので読んでいる。著者はウィラートン（Simon Willerton）。ウィラートンも用語法では悩んでいるらしい。ベクトル空間の圏で使われる用語を標準と考えるのがいいのかも知れない。モノイドとモノイドの作…

高階関数をさまざまな側面から理解することが重要なのだ、と思う。 関数のパラメータ付けられた族（関数族） パラメータを、もう1つのの変数と思う たくさんの関数達の値をまとめて表示すると、2次元の表（マトリクス）になる これはすなわち2変数関数だろ …

「信じられなーい！ 3」見つかった。コンビニ袋に、SPA! と一緒に"A diagrammatic approach to Hopf monads"が入っていた。ナルホド。紛れ込むパターンが多いのだな。特に、雑誌、書籍、他の書類のなかに紛れ込むことが多いようだ。

「配列内から特定の値を探す」課題に対して： // Eチャンのコード // 配列arは、具体的に与えられていて ar.length = 5 var i = 0; while (i if (x == ar[i]) { print("found"); } else { print("not found"); } i = i + 1; }ナールホド。これはこれでいいん…

「ホップモナド、左右の随伴」に挙げた"A diagrammatic approach to Hopf monads"を印刷したんだけど、なくなった。いや、ほんとに信じられない。ウーン、、、研究の価値があるほどに謎の現象だ。

適当な係数（スカラー）体上の1次元ベクトル空間だけを集めた圏Vec1を考える。そんなものつまんねー、と思うだろうが、いいやっ、十分に面白い。テンソル積に関してモノイド圏になる。モノイド単位はスカラー体だが、実はどの対象を選んでも単位になる。単位…

ピノキオを人間にする ： /C/(A, B) = C(I, [A, B]) = C(A, B) は、Cが閉圏なら自明に成立する。 まー、自明なんだけど、それは閉圏の定義が自明になるように作られているからだよね。 http://golem.ph.utexas.edu/category/2009/02/monoidal_closed_categor…

「なんでもプロパティ」のようなことを最初から出すのは得策ではない。 「変数がない」、「変数が未定義」は箱で説明できる。 undefined値とかtypeof演算子、in演算子とかは最初から出してもいいようだ。 ifの例題に時刻により文言を変える挨拶。 絶対値とか…

「XMLを圏論的に」というスローガンがあったわけだ。関係の圏Relが集合の直和を直積としてデカルト圏になるとか、エルゴットオートマトンの圏とかを横目で睨むと、XMLの圏の様相も見えてくる。とりあえず、LSL = Linear String Languageの圏を定義しよう。Σ…

[紛失物]に書いてなかったヤツだが、なくした書類が出てきた。紙はステープラで閉じて、その紙束をクリップで閉じる。で、紛失物は他のクリップ閉じのなかに紛れ込んでいた。と、そうこうこともある。オリンパスのマニュアルもバラバラの紙束のなかにはさま…

あー 心残り もったいない せっかくだから もう少し あこもせも。

Xが集合でVが対称モノイド圏、[-, -]:X×X→V がV-圏の構造を与えているV値ホムだとする。モノイド単位を I∈V として、C(A, B) = V(I, [A, B]) とすると、X×X上の集合値ホムC(-, -)が通常の圏を定義するはず。これがピノキオから人間を作る標準的な方法。Cが閉…

Title: COHERENCE OF PROOF-NET CATEGORIES Authors: Kosta Dosen and Zoran Petric URL: http://www.emis.de/journals/PIMB/092/n092p001.pdf Pages: 33 Title: LogicWithout Syntax Author: DOMINIC HUGHES URL: http://boole.stanford.edu/~dominic/paper…

Title: A diagrammatic approach to Hopf monads (Submitted on 3 Jul 2008) Authors: Simon Willerton URL: http://arxiv.org/abs/0807.0658 Pages: 26 最近の絵算もの、面白そうなので印刷した。 Title: Isomorphisms between left and right adjoints (Su…

Title: Jump from parallel to sequential proofs Author: Paolo Di Giamberardino URL: http://www.cirm.univ-mrs.fr/videos/2008/exposes/323/Giambera.pdf Pages: 42 オーバーレイあり

Berger は ベルジュ Hughes は ヒューズ

『計算理論と論理プログラミング』という、どこで手に入れたか分かんない本が出てきた。スマリアンのEFSがべースという変わった内容。

バカ、キリ ランベック、スコット カウフマン コック（Kock）

強い興味を持ったにしても、いずれは忘れてしまう。 メールじゃなくて電話で確認。

日付と曜日の関係が同じ。

もらった書類やプリンタで印刷した紙束の紛失が尋常じゃない。おかしい!? うちにはシュレッダーもブラックホールもないはずだが。

物理現象 f = <t|ut - (1/2)gt^2> とかの例を出してもよかったかな プロファイルの説明がゴッソリ抜けてた 僕は最近、X, Y→Z のような書き方をする（カンマを使う）、その理由も説明するといいかもな。 ×（かける）はX（エックス）と紛らわしい。 テンソル積は難しげな印象を与</t|ut>…

「言い忘れ」つうか、時間内に言い切ることに無理があった項目： 機械語と高級言語の境界線はない コンパイラとインタプリタの境界線はない テキストとバイナリの境界線はない 式と値の境界線はない（値としての式、値も一種の式） 世界は相対的、連続的 境…

絵を上下反転（鏡映）、左右反転させて描く 算術式のパースツリーをいろいろな方式で描いてみる 中間ノードに演算を描く方式と、末端ノードに演算を描く方式とか