Cが非対称（対称とは限らないという意味）厳密モノイド圏だとして、対応する多圏Poly(C)を定義する。S = |C|*（クリーネスター）として、Sは連接で厳密なモノイドになるとする。α = (A1, ..., An), β = (B1, ..., Bm) をSの要素として、PolyHom(α→β) := C(<α…

「本棚 右の壁から10面目、11面目」のなかに、なんか変な論理本。 「本棚 右の壁から6面目、7面目」のなかに『論理学をつくる』 「本棚 右の壁から4面目」にも変な論理本。隣の本がタイトル見えないが、なんだ？ 「本棚 右の壁から4面目」のなかに『ゲーデル…

セルの次元は描画時にbump upしているので、描画キャンバス次元は1次元上がっている。 高次圏 シーケント ムービー 0-セル 命題 絵の一部（ワイヤー） 1-セル シーケント スチル 2-セル 推論、証明 トランジション、ムービー 3-セル 証明の変形 ムービームー…

竹内／八杉のあの『証明論』が見つからない。カット消去がちゃんと載っているのはアレくらいだろう。

20070416 直積と射影がらみの高階関数たちの相関図 - 檜山正幸のキマイラ飼育記 20090325 演繹系とお絵描き圏論 - 檜山正幸のキマイラ飼育記 今、けっこう真面目に考えている。多圏の導入と使い方。[追記]だいたい出来た→ http://d.hatena.ne.jp/m-hiyama-me…

「ならば」記号があると、左右または上下がある。その部分は何と呼ぶのだろう。まったく確信がないが、 A⊃B で、Aが前件（antecedent）でBが後件（consequent）だったか？ 前件／後件は条件法（conditional; 条件表現、条件文）に対して使われる言葉だと思う…

⊃ implies |- provable（probableじゃない、注意） ⇒（シーケント） entailsかな |= valid, satisfies A |- B に対して、B is provable from A のようになる。|= A も A is valid。A |- B を A proves B と読むとおかしいのかな？ proveする主語はAじゃなく…

当然ながら、いきなり専門用語は避けたほうがいい。 代替の言葉 論理の専門用語 文 命題、論理式 接続詞 論理結合子 主語変数 個体変数、束縛変数 固有名詞 個体定数 主語変数を持つ文 命題関数、単項述語 当てはめ、置き換え 変数置換、具体化 Pが単項述語…

絵算の描画方向を示すために旗を使うことにした - 檜山正幸のキマイラ飼育記 で紹介した方向を示す旗 バエズの指数クラスプ、絵記号とテキスト記法 - 檜山正幸のキマイラ飼育記 メモ編 のバエズのクラスプ（clasp; 留め金） クックのケット、クックの絵算解…

指数の中置演算子 - 檜山正幸のキマイラ飼育記 メモ編 の続き。指数を「A●--○B」はいかにもうるさいので、「A--(B)」とする。正式には「[A]--(B)」だとする。つまり、()--[] という2つの場所と6文字からなる演算子記号。絵では、○と□を使う。A○--□B が、(A)-…

string streamを使うために、 #include <sstream> // std::ostringstream とする。これで文字列の構築を出力ストリームへの書き出しとして扱えて便利。ところが、なんかエラーする。エラーの箇所は次のようなコードのなか。c:/Installed/MinGW/lib/gcc/mingw32/4.6.2/</sstream>…

elocute【自動】弁じ立てる elocution【名】雄弁術、演説法／演説口調 erotic【形】性愛の、肉体関係の性欲を起こさせる［かき立てる］／〔人が〕淫乱な、欲情にとらわれた

Contacting host: www.emacswiki.org:80 gnutls.c: [1] (Emacs) GnuTLS library not found Opening TLS connection to `www.emacswiki.org'... Opening TLS connection with `gnutls-cli --insecure -p 443 www.emacswiki.org'...failed Opening TLS connect…

タブの問題は意外に頭がいたい。どうすべきか悩む。とりあえずは、タブが使われているかを見るために、http://keisanbutsuriya.hateblo.jp/entry/2015/02/03/153149 にあったスニペットを貼り付けて実行してみた。 (require 'whitespace) (setq whitespace-s…

まず、メイト対応のもとになる単位の構造 ベクトル空間の双対空間 K→V*V 関数計算（インフォーマルなラムダ計算とか）の恒等射のネーム 1→[A, A]（指数） 関手の随伴対 η::Id⇒G*F 米田埋め込み id::1⇒A*A^（A^は対象Aの米田埋め込み） ベクトル空間の双対と…

andLinuxなんてのがあったんだよな。 andLinux - 檜山正幸のキマイラ飼育記 メモ編 BSD on Windowsなんてのもあった。今じゃ仮想環境で本物のOSが動かせるからな。

http://blog.10rane.com/2014/09/17/to-reading-comprehension-of-the-source-code-by-introducing-the-helm-gtags-mode/ 先ほどphp-modeとruby-modeにhelm-gtags-modeをホークしたので、Rubyファイルを開くと自動でhelm-gtags-modeが起動します。 http://yo…

めちゃくちゃ昔からあったような気がするが、使う機会がなかった。モードのフックでセットするようだ。 (defun my-c-c++-mode-init () (setq c-basic-offset 4) (setq indent-tabs-mode nil) (hide-ifdef-mode t) (hide-ifdefs) ) (add-hook 'c-mode-hook 'm…

とある処理部分をgithubにあるソースを使おうと思ったのだけど、古めのコンパイラだとダメな所があった。古めのコンパイラだと、 final, noexcept, overrideなどのキーワードを知らない。 右辺値参照 && を知らない。 右辺値参照に関わる std:move などを知…

圏の指数のための中置演算子記号 - 檜山正幸のキマイラ飼育記 指数の中置演算子には随分と苦労している。 [ , ] → ⊃ ^- --o --○ ●--○ 左右の指数を区別をするときは、それぞの逆向き。指数を使ってアブラムスキーのネームとコネームを表すには4種類の記号が…

ここの、Category theory as CCLTとRelations in Categoriesが気になる。

本棚 右の壁から10面目に『Scalaプログラミング入門』てのがある。記憶にないので、買っただけだったらしい。

クックの三角形＝ディラックのブラケットの採用 バエズのクラスプを積極的に利用 クラスプと極性と線形含意記号（指数の記法）の統合 evを台形にした。 描画方向を示す旗記号 極性の印はプラスが○、マイナスが●で、マイナスからプラスが矢印の方向。だから、…

A×(B + C) = (A×B) + C これは分合律（dissociative law, linearly distributive law）。 A×(B×C) = (A×B)×C なら通常の結合律。別な演算*があって、 A * (B×C) = (A * B) * C ならなんと呼ぶか？ * を含意＝指数だと思うと、これはカリー同型。分合律やカリ…

https://www.cs.cmu.edu/~fp/courses/linear/handouts/lnd.pdf からの引用（画像としてコピー）線形含意の記号は 。ラムダ絵算で使おうと思っている。

gtagsに関しては→GNU Global - 檜山正幸のキマイラ飼育記 メモ編タグファイルを作ったり更新したりは、helm-gtags-create-tags, helm-gtags-update-tags。キーバインドは次のように覚える。 入力されたタグの定義元へジャンプ(kbd "C-c C-t") 'helm-gtags-fi…

クラスプ（clasp; 留め金）の絵。モノイド閉圏、オダンゴ、留め金、池袋 - 檜山正幸のキマイラ飼育記の図： 方向の取り方： カリー化： 左右のカリー化： この絵法を最初に見たオリジナル論文： Title: Computation and the Periodic Table (ATMCS 2008) Aut…

関数オブジェクト - 檜山正幸のキマイラ飼育記 メモ編 もうひとつ、関数オブジェクトってのがある。operator() を持つオブジェクト。 例を出す。まー、クロージャですね。 #include <stdio.h> struct CountedHello { int counter; CountedHello() : counter(0){} void</stdio.h>…

コンピュータはメンドクセー - 檜山正幸のキマイラ飼育記 メモ編 やっぱりコンピュータはメンドクセー！！ - 檜山正幸のキマイラ飼育記 メモ編 コンピュータって、インストールだの設定だのトラブルだの、それで半日潰すとかしょっちゅう。あー、やだやだ。…

いつも忘れてしまうのだが、 タブコードを使う／使わないは、バッファローカルな indent-tabs-mode 変数。 タブキーによる効果を設定するのは、グローバルな c-tab-always-indent 変数。 バッファローカル indent-tabs-mode 変数 値 動作 nil インデントの際…