長男：「橋下さんは、大阪維新の会で大阪都を目指すのか」父親：「…」長男：「んじゃ、俺は、東京維新の会を作って東京都を目指すぞ」父親：「あのさ、目指さなくても東京は都だから」

ホモトピーをヘビーに使う型理論が登場したりして、コンピュータ屋さんでも「ホモトピーなんて無関係」とも言ってられないようです。とか言いながら、僕はろくに知りませんけど(苦笑)。まー、用語くらいは調べておこうかな。トム・レンスター（Tom Leinster…

Cがデカルト圏だとは次のことです。 Cには終対象がある。 Cには二項の直積がある。 この2つのことから、すべての有限離散図式の極限の存在は保証できます。上記のデカルト圏の定義を言い換えてみましょう。この言い換えは、次の概念を確認するために良い練習…

先週、「Alloyの矢印記法と、モノイド閉圏としての関係圏」で、「Alloyで直積を表す矢印記号は、関係圏で解釈するとツジツマがあう」という話をしました。より一般に、Alloyの意味論を関係圏Rel上で展開してみるのは面白そうです。とはいっても、Alloyがカテ…

Alloyでは、タプルを矢印記号「->」で書くんですよね。最初は「なにこれ？」と思いました。例えば、aとbのタプル（この場合はペア）である (a, b) を、a->b と書くのです。集合の直積も同じ記法で、「集合Aと集合Bの直積」を A->B で表します*1。最初は違和…

長男：「ちょっと小遣い足りないから、おとうさん、肩揉んであげるよ」父親：「はっ、どういうこと？」長男：「肩揉んであげるからお金ちょうだい」父親：「君はマッサージへたでしょ、ほんとに気持よかったらお金出してもいいけど」長男：「うまかったらい…

Catyでユースケース図もどきの絵が描けるようになったことを紹介。ついでに、昨日「悟りやヒラメキがほんとに大キライだ」とか騒いでいた前後の経緯というか、文脈をちょっと説明しておきます。いくつかの理由があって、Catyにユーザーロール（user role）と…

ソフトウェアの設計は僕の仕事の一部なんだけど、モデリングとか高水準の設計手法とかに興味がない。いや、正確に言うと、そのテの手法とか流儀とかには、僕を苛立たせるものがあって、精神衛生のために避けている傾向があるってことです。参照の必要があっ…

見た目も大事だよね、と思ってCatyにビジュアライズ機能を入れ始めたのですが、以下のような図に比べると、Catyが描いた図はどうも分かりにくい感じがします。（以下の図は、http://terasoluna.sourceforge.jp/tutorial/server-web/Document/WebTutorial_2.h…

GMailの操作中に間違って広告をクリックしてしまい、とあるWebページが表示されました。以下がスクリーンショットです。原寸大画像よく目を凝らして見ると、背景になにやらプログラミング言語のソースコードのようなものが散りばめられています。おそらくWeb…

「インスティチューションとホーア論理を一緒にしたようなナニカ」は、僕にとっての一つの課題です。この課題については、次のエントリーで述べています。 ホーア論理の圏論的な定式化 真偽構造が付いた圏 -- ホーア論理のために 「インデックス付き圏のフビ…

以前、セミナーでの説明のために、「大きなラムダ式／小さなラムダ式」という記法を使いました。その後も使ってますが、けっこう具合がいいです。紹介しておきます。大きなラムダ式は圏の射をそのまま表し、小さなラムダ式は指数対象への射を表します。次の…

「WebアプリケーションフレームワークCatyの現状と今後」と似たような題名の記事、まー続きのようなものです。Catyのプロモーション的なことをしてないので、少し宣伝風に書いてみようかと。「Catyプロジェクト／ソフトウェアについて」（2009年8月）あたり…

「インデックス付き圏のフビニ／グロタンディーク同値」より： ここ2,3日考えていたことがあります。その動機とか背景とかを説明すると「けっこう面白い」かと思うのですが、長くなるので結論（になるはずのこと）だけをザッと述べます。一言だけいっておく…

ここ2,3日考えていたことがあります。その動機とか背景とかを説明すると「けっこう面白い」かと思うのですが、長くなるので結論（になるはずのこと）だけをザッと述べます。一言だけいっておくと、大量のモナド類似物（monad-like entities*1）を一挙に扱う…

僕は、ほぼ毎日、だいたい決まった時間にスターバックスに行くので、店員さんと顔なじみになる。だけど、「お早うございます」と挨拶くらいはしても軽口を叩いたりはしない。事務的にコーヒーを注文するだけ（参照）今日は、男性の店員さんが、事務的やり取…