今朝、「ピタゴラスイッチ」見ていて気付いたのだけど、「いつもここから」の山田一成、すごく太ったんではないか。もともと菊地秀規よりは少し太めだったが、今はだいぶ太い。

夕刊紙の見出し： 全米でサイバーテロ!! よく見ると小さく、ダイ・ハード4.0 あすから公開。こんなことするのは東スポだな、と思ったら夕刊フジだった。

「圏論勉強会 復習」の続きみたいなハナシ。話題はレトラクション。レトラクション対（retraction pair）とは、r:X→Yとi:Y→Xの対(r, i)で、i;r = X（idXを単にXと書く）を満たすもの。rのほうを（狭い意味で）レトラクションと呼んで、iを埋め込み（embeddin…

レトラクション図形的イメージは「レトラクションの起源（かな？）」に描きました。計算論（再帰関数論）よくわからんにょ。デカルト圏の等式的計算僕は絵を描いて（pictorial calculation）済ませてしまうことが多いのだけど、等式的計算（equational calcu…

サーバーお引っ越しでバタバタしているってことかな。

レトラクション（retraction）やベキ等自己射（idempotent endomorphism）の典型例つうか起源は、図形の引き込み変形のような気がします。いやっ、気がするだけでほんとのところは知らないけど。まーとにかく、絵を描いておきます。平面をPとして、普通の座…

ErlangによるWebサーバーといえば、YAWSというのが有名らしいです。が、もっと原始的な付属ライブラリ・モジュールhttpdを使ってみました。解説文書が（あるかも知れないけど）見つからなかったので、manページとソースを拾い読み。 man httpd -- http://www…

前回（その2）から引用： “未定義の定義”ごとに、型や型階層の概念が少しずつ違ってきます。それらは並列に存在する異なった定式化であり、優劣を論じても生産的ではありません。無理に優劣を付けようとすると、不毛な議論になるわけです。 というわけで、「…

梅雨時の天候としてはこれが正常なのだろうが、湿度は苦手だ。あー、ダメ。

900円の胡麻だれ蕎麦を食べてお勘定しようと、ポケットからサイフを出した瞬間には100円玉のおつりを手渡してくれる。僕は、千円札を探し出して差し出すことになる。

前回（初回）わかったことは、レコードデータによって構成される型の階層は、データ（インスタンス）集合の包含関係ではうまく説明できないことです。実際のところ、データ集合の包含関係では型階層を表現できません。型階層を定義する正統派（と僕が思う）…

レコードデータの型階層（type hierarchy）は、ときおり考えてみる問題なのです。毎回考えた結果を忘れている(苦笑)ような気がするので書き留めておくことにしよう、っと。JavaScriptを事例に考えます。ただし、現状のJavaScriptの型システムは奇妙で不格好…

次男（未就学児）：「それでは、お父さんにコレをあげよう。」父：「これ、なに？」次男：「俺が17年前にオジイチャンからもらった御守りだ。」「17年前」って？

長男：「お父さん、今日は父の日なんだからプール連れてって。」次男：「じゃ僕にはポケモンの本買って。」なんか違うんじゃねーか、それは。

長男：「女子サッカーでは、なんで試合が終わった後、ユニフォームの交換をしないの？」だいたいの事情は察しがつくんだけど、うまく説明できない。

まー、お風呂とか温泉で使えるのは便利(?)かも。でも、僕は防水より防コーヒーのほうが切実な要求だな。

以前にここで提出したアミダのクイズをErlangプログラムにより解いてみました。「解いた」とは言っても、プログラムが解の候補を全部列挙するシラミツブシ方式ですけどね。でも、これで遊んだり実験してみると、なかなか楽しいですよ。内容： アミダのクイズ…

最近たて続けに（6月9日と6月12日）奇妙なトラックバックを受けました。事実上スパムなんだけど、「フーン、なるほどね」と感心したので消さずにおくけど、今後同種のトラックバックは削除しますよ。で、どういう仕掛けかというと； まず、多くの人が興味を…

ErlangだってブレイクしたのだからCafeOBJだって…… って、それはないか。Diaconescuの論文*1にあった例： mod R2VECT { pr(FLOAT *{sort Float -> Real}) -- FloatをRealとリネーム [Vect] -- R×Rで定義されるベクトル空間（のつもり） op 0 : -> Vect op <_,_> :</_,_>…

Erlangをまだコソコソいじっていたりするのですが：プロセス間通信を利用する際に、RPC（Remote Procedure Call）みたいな形にすると使いやすいこともあるようです。RPCとは言っても、実際にはリモート（遠隔地）じゃなくて近距離だったりするのですが、、、…

興味を持つ人は非常に少数、かつ反応はありそうにないことを承知でCafeOBJの話を続けます。アーベル群の仕様を次のように書きました。 mod ABGRP { -- Abelian group [A] op _+_ : A A -> A op 0 : -> A op -_ : A -> A vars X Y Z : A eq X + Y = Y + X . -…

咳は止まらないし、めまい（割と本格派）は出るしで、ダメな週でした。で、いま、CafeOBJいじってたりするのだけどね。

まだ咳が止まらない。不調だ。それはともかく：「ソートと指標と型、実例をまじえて」に、CafeOBJのサンプルコードを出したので、久しぶりにCafeOBJを触ってみました。あー、やっぱりこれ面白いな。でも、よく分からないところもありますね。CafeOBJのユーザ…

風邪とは違うような気がするが、、、咳き込むとつらい。

このダイアリーでは、型（タイプ）の話題をけっこう取り上げています。例えば： 今風の型理論入門（本編） デュアルプログラミングとエクソシストゲーム 僕のスタンスは"Types as Theories"、つまり型とはセオリー（形式的理論）だとみなす立場です。で、そ…