2016-02-01から1ヶ月間の記事一覧
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 インデントの際…