内容 レイフィケーション 形式化された証明と算術プログラミング メタプログラミングと妖精さん達 レイフィケーション2006年の正月に、「ゲーデルの不完全性定理」に関する記事を何本か続けて書きました。 最初の記事： プログラマのための「ゲーデルの不完…

僕は小さい頃は甘えん坊だったと聞かされたが、母親と特に親密だったおぼえがない。むしろ、小学生／中学生くらいのとき、何度か母親にひどく腹を立てた記憶のほうが残っている。小学生の頃、理科実験器具のタグイが好きだった僕は、ガラス製温度計を持って…

BNF（バッカス／ナウア記法）は、構文を正確に記述するためにとても便利です。僕はよく使ってますし、このダイアリーでもけっこう言及してますね。 http://d.hatena.ne.jp/m-hiyama/archive?word=BNF BNFでは区切り記号や予約語なんかも具体的に記述しますが…

ツリーに関する用語ですが： 木構造 根ノード 葉ノード この「木」「根」「葉」って、訓読みしますか、音読みしますか？ きこうぞう／もくこうぞう ねのーど／こんのーど はのーど／ようのーど 僕は「き」「ね」「は」だけど、音読みの人もいるみたい。

2010年3月に3D映画『アバター』を観に行ってエライことになりました。次男が頭痛と吐き気をもよおしてしまったのです。そのことは、「「アバター」は危ない」に書きました。それから案の定3D映画が増えて、次男は映画館には行きたがらなくなり、長男と二人で…

Webサイトの構造を設計するとき、多くの人は画面とそのあいだの関係（遷移、ハイパーリンク）から考えるでしょう。僕は、このやり方は正しいと思っています。画面（ページ）という概念がないWeb APIの場合でも、画面をクライアント状態に代えて、クライアン…

先ほど書いた記事を受けて、Catyに関する情報不足をナントカする試み。技術的な背景や設計判断に関して述べることはいくらでもあるのですが、それ以前に、「それはなに？」「なにがうれしい？」さえも説明してない／できてないですね。「それはなに？」「な…

[追記]この記事の続き(?)として、「Catyの特徴と機能をイメージできるようなオハナシ」という記事を書きました。「Catyの特徴と機能をイメージできるようなオハナシ」をオンラインで書き始めた状態で間違ってサブミットしてしまい、結果として、この記事「Ca…

ラムダ計算の強力さの理由（のひとつ）は、任意の高階関数が定義可能なことでしょう。しかし、1階の関数があれば高階関数は必要ない状況もあります。α、βがデータ型だとして、関数の型 α->β は必要だが、(α->β)->γ なんてのは要らない、って設定です。これか…

僕は、ソフトウェアシステムの構造や処理の流れを絵で描くのが大好きです。つうと、「UML図か」とか思われそうですが、UML図には気力が湧きません。 理由1：ナントカ図、カントカ図といっぱいありすぎる。 理由2：オブジェクト指向設計の影響が強すぎる。 UM…

直積と直和を持つ圏Cで、対象Aを固定して、λX∈Obj(C).(A×X)、λf∈Mor(C).(A×f) とするとCの自己関手を定義できます。A×f と書いたときのAはidAの意味だとしています。対象も射も表す変数xを導入して、λx∈C.(A×x) とすると簡略に書けます。M = (M, m, e) が（…

とある論文にあったパズル（一人ゲーム）です。（後日、ネタはばらします。）これは、点と線からなる図形、つまりグラフですね。このグラフの辺に、0, 1, 2 の3つの数のどれかをラベル付けします。このとき、次の条件を満たすようにします。 すべての点で、…

中丸薫さんて方は、2012年にアセンション（なんだかわからん現象）が起きるとおっしゃっていましたよね；「2012年 地球は5次元に移行する」とか。そもそも意味不明ですが、いまのところ、次元が変わった気がしない。闇の権力とＵＦＯと２０１２年作者: 中丸 …

昨日は変な時計の紹介とかしてしまったのですが、ネタ元は、マイク・ステイ（Michael A. Stay）の次の記事です。 "Compact Closed Bicategories" guest post by Mike Stay (http://golem.ph.utexas.edu/category/2012/06/compact_closed_bicategories.html) …

The n-Category Cafe のマイク・ステイの記事から、なぜか面白い時計を紹介したサイトへのリンクがありました。25 Cool And Unusual Clocks 25個の、斬新なデザインで、ちょっと変わった時計が紹介されています。そのうちの4つを引用します。他の時計たちも…

以前、、ローカルホストの綴り字を間違えましたが、リンクをたどってアクセスできました。今回はローカルホストのサーバーをあげるのを忘れていました。お節介な親切な Google Chrome さん： Google Chrome では localhost に接続できませんでした もしかし…

次男：「ぼく、家出するなら行くとこ決めてるんだ」*1長男：「ふーん」次男：「小さい頃よく行っていた××公園」長男：「あそこは夜でも暗くないから、いいよな」次男：「あとブックオフ」長男：「漫画とかあるから退屈しないな。図書館もいいんじゃない」次…

今週（2012-06-04からの週）は、圏TotPtRelの話をしてましたね。 月曜： 役に立ちそうだが奇妙な圏 火曜： 続報・役に立ちそうだが奇妙な圏： コレ、使えそう 木曜： 奇妙じゃなかった、これは役に立つ圏 月曜日は「変なものを見つけちゃったよ」という感じ…

忘却関手とは何であるか？ を、一般的に定義するのはけっこう難しいことです。 さまざまな忘却関手 ですが、構造を忘れる忘却関手なら定義できなくもないようです。P. V. Golubtsov, S. S. Moskaliuk "Method of Additional Structures on the Objects of a …

奇妙だと思っていたのは僕の誤った印象だったようです。 役に立ちそうだが奇妙な圏 続報・役に立ちそうだが奇妙な圏： コレ、使えそう 基点付き集合（pinted set）を対象として、基点を基点に移す全域（total）な関係を射とする圏TotPtRelは、どうやら、良い…

昨日、「役に立ちそうだが奇妙な圏」という記事を書きました。基点付き集合（pinted set）を対象として、基点を基点に移すような関係を射とする圏PtRelを考え、さらに全域な関係だけを選んだ広い部分圏TotPtRelを作ります。この圏TotPtRelが役に立ちそうなん…

Relを関係圏（the category of relations）とします。R:A→B in Rel のとき、RはAとBのあいだの関係なので R⊆A×B ですね。(x, y)∈R であることを xRy とも書くことにします。また、x∈A に対して R(x) := {y∈B | xRy} と定義します。Aが基点付き集合（pointed …

2011年12月20日の記事で： [フローチャートについて書くのは] 僕にとっては定期ポストみたいなものです。年に一,二度はこのことを言っておきたい、みたいな。 と書きました。それから半年たってないのですが、なんかまたフローチャート・ネタをやりたくなり…