2002-02-05 ふりむく彼女の微笑はあまりに遠い
λ. 今日も夕方まで寝ていた。明日は寝坊したらまずい。
λ. ちょっとした作業のために某サーバのftpアカウントを友人に教えて貰ったのだけど、ange-ftpでアクセスすると挙動がおかしい。どうやら、ls "-al /." 等とすると実際の/が見えてしまうようだ。
使われているのはWU-FTPD 2.6.1なのだが……
λ. 大学生協インターネットサービス
1月24日に注文した書籍がようやく店舗に届いた。まあこんなものか。
λ. CNSのWnnでトラブル。
eggで変換しようとすると以下のように言われて変換できないように突然なってしまってびっくりした。wnn6-jserver-setupでのadd-wnn-fisys-dict, add-wnn-fiusr-dict, add-wnn-dictの呼び出しがエラーになっているようだ。~/Wnn6/hindo/以下のファイルが壊れてしまったようだ。ファイルを消してしまったら、新しくファイルをつくってくれて。とりあえず解決。
ホスト nls02 の Wnn を起動しました Loading /a/fs03/home/sd01a/SOLARIS/26/new/local/share/emacs/site-lisp/eggrc-wnn... 何かのエラーが起こりました。 何かのエラーが起こりました。
λ. 次世代指導者： 小渕優子さんらを選出 世界経済フォーラム
おいおい。まじっすか。うひひ。
2003-02-05 ごろごろ
λ. 今朝の夢
どっかの温泉に行く夢。いい湯だった。ちなみに混浴ですた(笑)
λ. アッカーマン関数
CPLでアッカーマン関数の続き。萩谷先生の「止まれ」という記事にも、Ackermann関数も、primitive recursiveな汎関数としてならば定義することができる
と書いてあった。さらに、任意のprimitive recursiveな汎関数が停止するということから、Peano算術の形式体系としての無矛盾性を導くこともできる
という事が書いてあって感嘆する。すごいものだなぁ。
λ. category of Chu spaces
これまで「classificationとinfomorphismの圏」とか適当に呼んでたけど、 名前はちゃんとあったようだ。
The category whose objects are classifications and whose morphisms are
infomorphisms is sometimes called the category of Chu spaces,
or the “Chu over Set” category.
λ. infomorphism vs adjunction
ところで、infomorphismの条件「f∨(b) ⊨A α iff b ⊨B f∧(α) 」って、adjointの条件「HomA(F(X),Y) ≅ HomB(X,G(Y))」と似てるな、とふと思った。
これって、例のInstitutionではfunctorがinfomorphismに相当するって話と何か関係ある?
2004-02-05
λ. eventSherpa
in the vanguard (2004-01-30)から、ちょっとしたメモ - eventSherpaとRDFicalをみて、eventSherpaを使い始めてみる。カレンダやスケジューラの類を使うのは初めてなのだけど、なかなか便利そうだ。
オンラインにあるRDFicalのデータを購読できるようなので、とりあえず、学事日程のデータをcronでRDFに落とすようにしておいて、それを購読してみる(スクリーンショット)。
これらのファイルを生成するには、例によって泥臭いスクリプトを書いてるのだけど、こーいうのってやっぱXSLTとか使うべきなんだろうか。
あと、今回初めてakrさんのhtreeを使った。あまり使いこなせてないのだけど、なかなか使い勝手の良さそうなライブラリだという印象を受けた。
2006-02-05
λ. Pattern matching with dependent types.
T. Coquand. Pattern matching with dependent types. In Proceedings of the International Workshop on Types for Proofs and Programs, 1992.
依存型(dependent type)が存在する場合のパターンマッチングの話。パターンをコンテキストマッピングをして形式化し、パターンマッチによる定義が正しい定義であるための十分条件とチェックのためのアルゴリズムを示している。パターンをコンテキストマッピングとして扱うのが面白かった。例えば以下のような定義の場合、
add : (x : N, y : N)N add(succ(m),n) = succ(add(m,n)) add(zero, n) = n
Δ = { x : N, y : N } として、 最初のパターンは { x := succ(m), y := n }: { m : N, n : N } -> Δ 、 二つ目のパターンは { x := zero, y := n }: { n : N } -> Δ というコンテキストマッピングとして扱う。
20050915#p01 に少し追記。
2007-02-05
λ. 大人の常識力トレーニングDS
これまで少しばかり非常識な存在だったので、常識を身につけようと購入してみた。社会人にもなることだし。
最初の診断の結果は7問正解*1で常識力指数59。なんだ、わりと常識的じゃん、俺。でも、苦手ジャンルは「礼儀」で、これは予想通り。
*1 一問暗算が間に合わなくて落した問題があるのが悔しい
λ. 研究会最終発表
せっかくDSを持っていったのに、ピクトチャットするのを忘れてた。 しょぼーん。
打ち上げ
- コスプレはするもんじゃない、させるものだ
- 藪をつついたら萩野先生が
- 大学教授は社会人なのか?
ψ Ze [そういや、イタリアで新BSE患者発症したな。やっぱりというか、、、]
ψ さかい [これですね。 http://www.mainichi.co.jp/news/selection/archive/20..]
ψ 天仙娘々 [天国に涙はいらない、回を追うごとにパワーダウンしている気がするのは気のせいでしょうか。といいつつ、手前は全巻持ってい..]
ψ さかい [天仙娘々さん、はじめまして。 そう言われてみれば確かに最初が一番勢いがあったかなぁ。 個人的には、2巻の「フランダ..]