「型推論に関わる論理の概念と用語 その1」で、「『型推論』て言葉が何を意味するかはそれほど明らかじゃない」と言いました。その2では、「同義語／類義語が無闇に多くて、人によって言葉の使い方が違う」と注意しました。僕の目論見としては、何種類かの文…

話が前後しますが、なんで僕がこんなエントリー（のシリーズかな？）を書こうと思ったかを述べます。その後、高階述語論理に少し触れます。 前回のエントリー：型推論に関わる論理の概念と用語 その1 シリーズ目次： その1 その2 その3 その4 その5 その6 番…

寒いのがホントに苦手。寒いと活動レベルが下がって、なんもやる気が出ないわ。これ、一回のエントリーで書こうとした内容なんだけど、途中までなので「その1」を付けました。中途半端なところでブチッと終りますが、続きをたぶん書きます。[追記 date="2012…

長男は、昔のアイドルとか古い歌謡曲をよく知ってます。長男：「東山って、少年隊のメンバーだったんだよね」父親：「うん、今でも少年隊なんじゃないの」長男：「それと、ニシコリっていう人も少年隊だよね」テニスのニシコリ選手が大活躍ですからね。少年…

ラベル付き有向グラフは関手とみなせます。有向グラフの基本的概念Gを有向グラフとします。Gには特に制限を設けず、多重辺もループ（同じ頂点に戻る有向辺）も許しましょう。Gの頂点の集合をNode(G)、辺の集合をEdge(G)とします。e∈Edge(G) に対して、辺eの…

雑感を記すだけですが：1年ほど前に、「なぜ僕は操作的意味論に傾いたか」という記事を書いたことがあります。もともと、ナントカ意味論という分類には拘ってはいないのですが、できることなら表示的（denotational）にやりたいな、という希望はあります。で…

bashでは、定義した変数はコマンドライン上でも二重引用符の文字列内でも展開されます。 $ format='+%Y-%m-%d'; date $format 2012-01-17 $ whom='Hanako'; echo "Hello, $whom" Hello, Hanako 入れ子もできます。 $ whom='Hanako'; greeting="Hello, $whom"…

[追記]このエントリー、間違って消してしまったから、再現。[/追記]長男から電話がかかってきて、質問をされた。 防衛相退任が決まった一川保夫氏と、俳優の蟹江敬三さんは似てると思うか？ 元画像：http://img.blogs.yahoo.co.jp/ybi/1/f3/c6/yoshimizushri…

うううう、今日も寒い。昨日、シーケント計算の話をしました。ここ最近、プログラムの解析にシーケント計算が使えるんじゃないかと思っているんですよ。シーケント計算の背景には、単なる圏よりはむしろ複圏／多圏（multicategory/polycateogry）があるので…

うううう、寒い。寒いのダメ。それはともかく：シーケント計算について初めて知ったのは、竹内さん（a.k.a ガイシ）の論理の本だったと思います。が、最近は、論理とあまり関係ないところでもシーケント計算を使ってますね。「シーケント計算は論理で使うも…

“筆跡が総書記そっくり”と称賛 [1月5日 16時47分] 北朝鮮の新聞は、軍の最高司令官に就任したキム・ジョンウン氏の筆跡が父親のキム・ジョンイル総書記のものにそっくりだと称賛し、[...snip...] キム・ジョンウン氏が先月末に工場の労働者らから寄せられた…

僕は、「抽象的」と「具体的」という言葉を必ずしも反対語として使っていません。意図的にそうしているわけじゃないのですが、気がつくとそうなんです。どういう事かというと、僕の個人的な言葉使いでは： 抽象的の否定や反対語が具体的（具象的）ではない。…

「フローチャートを復権させよう -- 2020年代のプログラミングへ」において、プログラムに関係する絵・図の話をしたのですが、僕がフローチャートを使いたい理由（いくつかある）のひとつは、一種のカリー／ハワード対応を利用したいからです。カリー／ハワ…