「ストリング図とストリンググラフ、何が違う？」で触れたストリンググラフを、もう少し詳しく説明します。内容： アンチ反射的単純有向グラフ ストリンググラフとラベリング ストリンググラフの描画＝ストリング図 描画の例 その他の話題 アンチ反射的単純…

インターネットで資料探しをしていると、出版されている書籍と同じ内容のPDFがゴロンと置いてあってビックリすることがあります。以下に挙げるのは、そのような、“出版物と同等な内容”が無料公開されている理数系専門書のリストです。紙の本とまったく同じも…

JavaScriptのSVGライブラリを探していたら、bonsaiというライブラリが見つかりました。 https://bonsaijs.org/ ロゴもこんな(↓)ですから、これは「盆栽」ですね。Kendo UIというUIライブラリもあるようです。 http://www.telerik.com/kendo-ui Kendo UIのオ…

Isabelleをいじっているあいだ（＝飽きるまで ^^;）は、ダイアリーにIsabelleの話が入るでしょう。今日は小ネタ。「ハイコンテキストな定数・記号の解釈」とかで話題にしたmin-plus半環をIsabelleで書いてみました。あの記事では、通常の演算子記号「+」「*…

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelle…

以前、証明支援系Coqの記事を書いたことがあります。今日話題にしたいIsabelle（イザベル）は、Coqのライバルと目される証明支援系です。最初のリリースが1986年ですから、実に30年間に渡って開発が続けられています（Coqもほぼ同時期にスタートしています）…

絵算（お絵描き計算、pictorial/graphical/diagrammatic calculation）で使われる絵はストリング図（string diagram）と呼ばれます。とある文書でストリンググラフ（string graph）という言葉を見たんですよね。ストリング図の同意語だろう、と思ってました…

歌詞で何やら騒動になったこの曲（2016年4月13日発売） http://www.uta-net.com/song/206311/ ディアナ・アグロンばっかり話題になりましたが、対比されているのは何故かアインシュタイン。少し後の2016年4月27日発売のこっちはシュレディンガー。 http://ww…

「関手データモデル／圏論データベース： その後の発展と現状 (2016)」 にて： FQL IDEがサポートする4つの言語のなかで、位置付けがハッキリしないカワイソウなFQL++ですが、「圏論の学習にはとても有用」という特徴があります。これだけを切り出して圏論学…

これ、中国語だし、「もと動画から許可とってる？」とか思ったりもするのですが、「猫と赤ちゃん」の可愛さは無敵ですね。この動画(↑)では、みんな（猫たち）赤ちゃんに気を使ってますね、爪を立てないようにしたり。でも、いつでも子供にやさしいとは限らな…

いらすとやさんの「水素水のイラスト」これは笑えます。けど、笑ってくれない人もいそうで、それがちょっと怖いです。このイラストのページの広告には（たぶん、ほとんどの場合）水素水の広告が出ます。それがまた可笑しかったりします。「スポンサードリン…

C/C++のとんだ落とし穴（ハマっちまったよ） 上記の記事で、Shift_JIS（CP932）のコメントにまつわるトラブルを紹介しました。あまり時をおかずして、C/C++でまたハマりました。コメント事件ほどの意外性はないにしろ、事情を知らないと対処しにくいトラブル…

2013年の初頭に、デイヴィッド・スピヴァックの関手データモデル（functorial data model）について紹介しました。 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル 衝撃的なデータベース理論・関手的データモデル 入門 あれか…

最近、「律子」という言葉を使っています。「りつこ」じゃなくて「りつし」です。英語の接尾辞「-or」の訳語のつもり。では、その「-or」とは何でしょうか。M = (M, ×, i) をモノイドとすると、次の法則が成立します。 (a×b)×c = a×(b×c) ― 結合律（associat…

「モノイド自然変換としての積分： 大雑把に」にて： 勘違いや抜けがあるかも知れませんが、修正をしても大筋はたぶん維持できるでしょう。もう少し確認して、“時間と気力があるときに”具体的な構成法を書くつもりです。 この件は書くつもりでいますが、一度…

「モノイド圏上の加群圏の実例」にて： 僕が加群圏にちょっと興味をいだいたのは、変則的なラムダ計算のモデルとして加群圏が使えないかな？ と思ったからです。思っただけで、よく分かってません。 これ、分かりました。何が分かったのか？ を大雑把に記し…

アレックスの花が今でも咲いています。しかし、花にしては寿命が長すぎる気がするし、緑色になってきてるんだけど。これって実は葉っぱ？

試供品でもらったシャンプー＆リンスだけど、間違っているよね、これ。と思ったんですが、こういうデザインのようです（コメント欄参照）。

とあるC++コードがコンパイルエラーするんですが、原因がまったく分からなかったんですよ。「そんなバカな?!」という感じ。しばらくハマってしまいましたよ。結局、C++でもCでも同じことが起きることが分かりました。次は、僕が遭遇したのと同じ現象が起きる…

昨日の記事に実例がなかったのでそれを追加します。いくつかの準備から：FinSetを有限集合の圏とします。×は普通の直積、1 = {0} として、(FinSet, ×, 1, α, λ, ρ) はモノイド圏になります。α, λ, ρを具体的に書くと： αA,B,Cは、((a, b) c) |→ (a, (b, c)) …

Cがモノイド圏でDが圏のとき、二項関手（双関手） H:C×D→D が結合律と単位律を満たすならば、(D, H)をC上の加群圏（module category）と呼びます。（加群の圏（category of modules）とは違いますから注意。）モノイド圏C上の加群圏(D, H)と、モノイド関手 Φ…

「目黒川がきらい 」： 目黒川の桜って何であんな人気なの。コンクリで護岸がちがちに固められた川だよ？桜っていう「自然」とコンクリっていう「構造物」はそもそも矛盾してるし。 目黒川の近くに20年以上住んでます。コンクリで固められた川なのは、そのと…

「モノイド関手／ラックス・モノイド関手とその実例」 今日の話はここまでにしておきますが、モノイド関手／ラックス・モノイド関手の定義からすぐ出るようなことでもけっこう面白い話題があるので、補足を書くかも。 補足を書きます。内容： ラックス・モノ…

かなりたくさんのファイルがあって、それらの先頭の数行を眺めたい -- そんなときは、headコマンドとlessコマンドを繋げばいいでしょう； head * | less 。眺めるだけじゃなくて編集もしたいときは、エディタ内からheadコマンドを実行したいですね。僕はEmac…

今でもあるんですよね、レトロなページが。出会ってしまうと、微笑ましいような、懐かしいような、気恥ずかしいような。 あなたは[nnnnnnn]番目の訪問者です。 文字が流れる（マーキーっていうんだっけ）。 キリ番踏んだら掲示板で報告してください。 Sorry,…

乙武洋匡さんのハナシがやたらに多いな―。僕は良い悪いとかよりも、乙武さんの能力に圧倒されてしまいますね*1。強靭なメンタル（今回は凹んでいるらしいが）、知的能力にも極めて優れ、体力・運動神経も抜群なのでしょう。無神論者なんだけど、こんなときは…

競馬の馬の名前ってなんでもありのようですが、昨日24日浦和で勝った馬はアスキーコード。注目されているのはアスキーコードに騎乗していた藤田菜七子騎手ですけどね。 藤田菜七子騎手がデビュー36戦目初勝利/競馬・レース/デイリースポーツ online 36戦目で…

モノイド圏のあいだの関手で、モノイド構造を考慮したものとしてモノイド関手（monoidal functor）やラックス・モノイド関手（lax monoidal functor）があります。その定義と幾つかの実例を挙げます。この記事のもともとの動機は、“直積をモノイド積とした集…

アレックスは僕が飼っている(？)植物です。去年の6月末（2015年6月29日）に「アレックスが花を咲かせた！」という記事で、十数年間一度も花を付けたことがないアレックスが花を咲かせたことを書きました。それから1年たってないのですが、 何故かまた花を付…

resp-lawvさんが、矢印のひっくり返し方が分からないので夜も眠れないそうです。残念ながら、僕は適切なアドバイスが出来ません。でも、夜は眠りましょう。ご飯も食べましょう。resp-lawvさんが想定しているセッティングでは扱いが難しいのですが、うんと単…