2008-06-01 [長年日記]
λ. 日常
ふと、サンダルが欲しくなったので買いに出かける。靴屋で買おうと思っていたが、途中立ち寄ったイトーヨーカドーで紳士の靴セールとかいうのをやっていて、20%オフだったので、なんとなく買ってしまった。
ついでに、使うあてのない商品券を金券ショップで売却。あと、バスカードを買おうと思ったら売切れてて残念。
夕食は久しぶりにグラタン食べた。
![[グラタン]](./images/20080601_1.jpg)
λ. 高齢者対策、配当100万円以下非課税 自民、マル優制度で検討
高齢者にも色々な人がいるだろうに、このような一律の優遇制度を導入するくらいなら他にやることがあるのでは?、と思ってしまう。
【追記】 「骨太の方針2008」(経済財政改革の基本方針2008)には取り入れられなかったようだ。
2008-06-03 [長年日記]
λ. セマンティクス
セマンティクスって？ - ひげぽん OSとか作っちゃうかMona- あたりの話。すご〜〜く大雑把に説明してみる。
「(2*3)+(4*5)」という式は、(2*3)+(4*5) → 6+(4*5) → 6+20 → 26 と書き換えできるよね、というのが操作的意味論(operational semantics)。正確にはsmall-stepの操作的意味論。どういう書き換えが出来るかを通常は再帰的に定義する。操作的意味論は良く知らないので、詳しい人にお任せ。
「(2*3)+(4*5)」という式は26という数を表しているよね、とか「明けの明星」は金星を指す表現だよね、というのが表示的意味論(denotational semantics)。何を表しているか、何を指し示しているかが意味。発想としては一番簡単だと思う。こちらも部分式の意味から再帰的に意味を定義する。
公理的意味論(axiomatic semantics)は、命令型言語のプログラムというのは状態を書き換えるコマンドだという立場。それで、プログラムの実行前の状態で成り立っている条件と、プログラムの実行後の状態で成り立っている条件との間の関係によって、プログラムの意味を考えたり検証したりしましょうというアプローチ。例えば、「i = i + 1」というプログラムがあって、その実行後の状態で i==5 が成り立っていたら、実行前には i==4 が成り立っていたに違いない、とかそんなの。
すご〜〜く大雑把にしか説明してないけど、どれも本当は奥が深いです。
蛇足
操作的意味論も表示的意味論も言語の研究にはずいぶん使われているけど、一般のプログラマにとって馴染み深いのは「契約による設計(Design By Contract)」とかJMLとかの背景にある公理的意味論ではないかと思う。
![[トマト鍋(?)]](./images/20080605_0.jpg)
2008-06-06 [長年日記]
λ. 計算と論理のための自然枠組NF/CAL by 佐藤 雅彦
本論文では，計算機上での証明記述および検証を支援するシステムNF/CALを紹介する．NF/CALの設計はフレーゲによる判断の分析の影響を受けており，人間が自然言語を用いて日常的に行う判断活動を自然に形式化したものになっている．
ずっと積読中だったものを消化。ワークショップの“Types for Verification”で“A simple theory of expressions”という講演を聴いたときには何が嬉しいのかよく分からなかったが、以下に引用する部分を読んでようやく動機が理解できた。
これらのシステムの多くは型理論に基づいており，もっぱら専門家による使用を前提としている．そのためシステムの利用には型理論の知識が必要となり，学部で計算や論理を教育するためのシステムとしては不適当である．本稿で紹介した式の理論は，計算や論理の基礎的事項を，最初から説明するための必要性から考案したものであるが，同時に我々が日常的に用いる自然言語が本来持っている構造を自然に反映したものになっている．
しかし、NF/CAL面白そうだな。 CALは昔使わせてもらったことがあって、そのときには挫折してしまったのだけど、出来たらまた試してみたいものだ。
2008-06-07 [長年日記]
λ. 第五回東京理科大学ピアノの会OB会演奏会
というものを聞きに行ってきた。
演奏していた曲
例によって、演奏されていた曲を ナクソス・ミュージック・ライブラリ(Naxos Music Library, NML) で探してみた。
- 「主よ、人の望みの喜びよ」ト長調 BWV. 147 / J.S.バッハ
- ショパンのエチュードに基づく練習曲第1番ハ長調 / ショパン / ゴドフスキー編
- ピアノ・ソナタ第2番変口短調「葬送」op.35より第3楽章「葬送行進曲」 / ショパン
- 子守歌変二長調op.57 / ショパン
- 2つの伝説 S.175 より第2番「波を渡るパオラの聖フランシス」 / リスト
- バラード第4番 ヘ短調 Op. 52 / ショパン
- 交響詩「フィンランディア」作品26 ピアノ編曲版 / シベリウス
- ピアノ・ソナタ第8番ハ短調「悲愴」 Op. 13 より第3楽章 / ベートーヴェン
- 10の小品op.12より第7番「前奏由」ハ長調 / プロコフィエフ
- ピアノ・ソナタ第14番嬰ハ短調「月光」op.27-2より第1楽章,第2楽章 / ベートーヴェン
- エチュードop.10より第12番「革命」 / ショパン
- 亡き王女のためのパヴァーヌ / ラヴェル
- アンダンテ・スピアナートと華麗なる大ポロネ—ズ 変ホ長調 op.22 / ショパン
- ピアノ・ソナタ第21番ハ長調「ワルトシュタイン」より第1楽章 / ベートーヴェン
あと、「黒猫フンジャッタっ!」という曲も弾いていた。
λ. プログラミング言語の意味論 by 勝股審也
おもしろいみろん - d.y.d で紹介されていたので、読んでみた。Adequacy や Full Abstraction についてはきちんと勉強したことがなかったので、(さわりだけだとは思うけど)勉強になった。
2008-06-08 [長年日記]
λ. “A constructive proof of equivalence of formalism od DCG's with the formalism of type 0 phrase-structure grammars” by Marica D. Prešić and Slavisa B. Prešić
We present a proof that definite clause grammars (DCG's) are equivalent in their generative power to type 0 phrase-structure grammars. The proof is constructive and it actually describes an algorithm for transferring from a language description by type 0 grammar to DCG characterization. The proof has been inspired by the proof given in [MA93] but our approach is considerably simpler and the constructed DCG grammar is much more efficient. The paper also suggests how computer implementation of the algorithm can be developed.
以前にTwitterで「DCGの言語クラスはtype-0」と書いたときに持ち出した論文を読んだ*1。 記法がよく分からないのだけど、引数の項で記号列を持って、書き換え規則を全て引数の項を書き換える形の規則にするということか。 そうすると、確かに0型文法をDCGで表現すること自体は自明だが、そのままだとProlog等の深さ優先でのSLD導出じゃちゃんと列挙出来ないのでは?*2
λ. 風神録Normalを魔理沙(B)で初クリア
![[準備「神風を喚ぶ星の儀式」]](./images/20080608_0.png)
世間はすっかり新作だと思うけど、そういえばまだ風神録あんまりやってなかったなぁと思い、まだNormalをクリアしてなかった魔理沙(貫通装備)でNormalをクリアしてみた。
久しぶりなこともあって、いつも以上にボロボロ。
東方風神録 リプレイファイル情報 Version 1.00a Name hiro Date 08/06/08 23:22 Chara MarisaB Rank Normal Stage All Clear Score 29768812 Slow Rate 0.18
2008-06-09 [長年日記]
λ. ハードオフで古いメモリとLANカードを処分
部屋を片付けていて出てきた古いメモリ128MB(PC2100U-25330-A0)とPCカードのLANカード(LPC2-CLT)をハードオフで処分。メモリは200円、LANカードは50円で売れた。わーい。
2008-06-11 [長年日記]
λ. Audibleを試す
Audibleは前から試してみたいと思っていたのだけど、無理なく続けられる 年収10倍アップ勉強法(勝間 和代)で紹介されていたので、手を出してみることに。 調べてみると、プラチナプランが14日間無料で試せる(= 2冊分無料でダウンロードできる)そうなので、早速登録。 勝間さんのCD、テープを聴いて勉強しよう!!: Audible再入門には「いろいろな場所でひっかかります」と書いてあったので、戦々恐々だったのだけど、当時に比べると簡単になっているのか、特に何もひっかかるところもなく、すぐにiPodで聞けるようになった♪
最初は何を聴こうかと思ったけど、考えるのが面倒だったので、一冊は適当に Rich Dad, Poor Dad: What the Rich Teach Their Kids About Money - That the Poor and Middle Class Do Not! にしてみた。もう一冊は後で考える。
2008-06-12 [長年日記]
λ. 最近のLast.fmクライアントでiPodを認識できない件
最近、Last.fmクライアントをアップデートしたら iPod を認識しなくなってしまって困ってしまった。どうも、ChangeLogを見ると、1.5.0.18515 (13/3/08) の Brand new system for iPod scrobbling using iTunes plugin instead of the LastFMHelper
が影響してそうなので、この変更が行われる前のバージョン 1.4.2 に戻したら直った。
Last.fmのダウンロードページからは古いバージョンへのリンクは張られていないけど、ファイルはそのまま残っているので、<URL:http://cdn.last.fm/client/Win/Last.fm-1.4.2.58376.exe> などからダウンロード可能。
λ. おしごとの英語（フレーズ編）を完了
iKnow!のおしごとの英語（フレーズ編）-ビジネス英語チャンネルを完了した。 開始したのは4/18なので2ヶ月弱か。我ながらよく続いたものだ。 次はどのコースをやろう。
2008-06-13 [長年日記]
λ. また国債買った
去年の8月に利付国庫債券(5年)(第65回)を買った。このときは表面利率1.5%で、その後の募集では利率が下がっていたのだけど、今日から募集している利付国庫債券(5年)(第72回)では表面利率が1.5%に戻っていたので、また少し買ってみた。
2008-06-14 [長年日記]
λ. RHG読書会::東京 Practical Common Lisp
スピリチュアルコンピューティングwww
λ. Googleトランジットのガジェット
乗り換え検索にはいつもGoogleトランジット（乗り換え検索）というガジェットを使っていたが、Google公式のGoogle トランジット(日本) に乗り換えた。 結果の候補の表示方法がわかりやすい。 経路を地図上に表示してくれるのは最初はどうでもよいかと思った*1けど、見ていると案外楽しい。
*1 重要なのは移動時間等であって物理的な位置ではないから
2008-06-15 [長年日記]
λ. ボーナスの使い道?
「今年のボーナスの使い道は?」というアンケートの結果を見たけど、アンケートの設問自体に違和を感じる。 普通はボーナスなどはまず自分の資産の一部として組み入れて、その上で資産全体の運用状況から見てどういった支出をするか考えるわけで、ボーナスと支出の間に直接的な関係は小さいと思うので。
2008-06-16 [長年日記]
λ. Smullyan's drinkers' paradox を Alloy で
Paradoxes of classical predicate calculus - ヒビルテ (2007-08-28) で Smullyan's drinkers' paradox を扱った。
これは英語で書くと「In any non-empty bar, there is a person such that if she drinks, then everyone drinks」で、論理式で書くと「∃p. (drink(p) → ∀y. drink(y))」というもの。 古典一階述語論理での演算子の意味を考えれば、当たり前ではある*1のだけど一見するとパラドクスに思えてしまう。
こないだは Agda で証明したので、今度は Alloy でも試してみる。
-- 個体領域
sig Person { }
fact { #Person > 0 } -- 個体領域は空ではない
-- 述語
one sig Drinkers { ext : set Person }
pred drink(p : Person) {
p in Drinkers.ext
}
-- test
pred show() { }
run show for 10 Person
-- Smullyan's drinkers' paradox
assert paradox {
some x : Person | drink[x] implies (all y : Person | drink[y])
}
check paradox for 10 Person
これを Alloy Analyzer でチェックしてあげると、ちゃんと「No counterexample found」となる。 また、ここで「fact { #Person > 0 }」を削除すると、ちゃんとPersonが一人もいない例が反例として得られる。
2010-12-23 追記
上の書き方はあまり良くなかった。
- 空でないことは、濃度演算子を使うより、someを使って表現したほうが良い。
- 部分集合はDrinkersのようなシグネチャのフィールドにしなくとも、部分集合シグネチャを使えばより直接的に表現できる。
直すと以下のようになる。
-- 個体領域
sig Person { }
fact { some Person } -- 個体領域は空ではない
-- 述語
sig Drinker in Person { }
pred drink(p : Person) {
p in Drinker
}
*1 (∃p. ¬drink(p)) ∨ (∀y. drink(y)) と等しいので
2008-06-17 [長年日記]
λ. コメントキーフィルタ＆プラグイン
最近、またコメントスパムがひどくなってきたので、コメントキーフィルタ＆プラグインを導入してみた。 最初は青木さんのパッチ(+ artonさんの携帯向けパッチ)にしようかと思ったのだけど、アップデート時のことを考えて、パッチを当てずに済むこっちにしてみた。
2008-06-18 [長年日記]
λ. Firefox 3
Download Day ということなので、家を出る前にダウンロードしようと思ったら、どのサイトも重くて大変だった。
最初は様子見のつもりだったけど、随分高速になっているし、使っているアドオンのうち重要なものは Firefox 3 に対応済みのものが多かったので、早速乗り換えることに。 僕の環境では、Firefox 2 は起動しっぱなしだとだんだんメモリとCPUの使用量が増えていって重くなったり、頻繁にクラッシュしたりしていたので、そういうのが解決するといいなぁ。 タブの切り替えに慣性がついたのがちょっと楽しい。
【2008-06-28 追記】 SFC CLIP: 光る日本列島という記事によると、Firefox 3 の灯 - 日本灯 を手がけたのは環境情報学部専任講師の筧康明という方らしい(c.f. 筧康明研究室ウェブサイト)。 へー
2008-06-21 [長年日記]
λ. Ruby会議2008 1st day
これから出発。色々な人にお会いできるのを楽しみにしています。
「Laurent Sansonetti氏は、id:ogijun氏と瓜ふたつ」らしいけど、そんなには似ていなかった気がする。
懇親会
須藤さんにショッカー人形をもらって、らびっとゆーざずぐるーぷ「ショッカー」に引き込まれた(笑
![[ショッカー仰向け]](./images/20080621_0.jpg)
![[ショッカーうつ伏せ]](./images/20080621_1.jpg)
2008-06-23 [長年日記]
λ. Audibleその後
先日、Audibleを試す - ヒビルテ (2008-06-11) でAudibleを使い始めた。
それで、無料でダウンロードするもう一冊を何にするかを悩んでいたが、結局 Amir D. Aczel の God's Equation: Einstein, Relativity, and the Expanding Universe (Unabridged) にすることにした。実は最初はサイモン・シンの本を探したけど、それは無かったので。
次に、The New York Times か The Wall Street Journal のいずれかのPodCast購読が無料サービスでついて来ていたようなので、とりあえず The Wall Street Journal を選ぶ。毎日50分前後のPodcastなんで、結構ごつい。果たして聴く時間はあるのだろうか(^^;
それから、PlatinumのMembershipは2冊/月の権利込みで月$22.95なのだけど、1冊/月の権利込みで$14.95のGoldで私には十分かなと思ったので、無料お試し期間が終わる前にPlatinumからGoldにダウングレード。 そしたら、Membership Renewal Date が無料お試し期間開始日の2週間後ではなく、1ヶ月に伸びていた。無料ダウンロードできる冊数は増えないけど、Podcastを無料購読できる期間が延びたことになる。ちょっとラッキー。
2008-06-24 [長年日記]
λ. tDiaryのセクションアンカーにtitle属性を
[tDiary-devel] [PATCH] セクションアンカーにtitle属性を
現在のtDiaryのセクションアンカーは、同じ文字列でありながらリンク先が異なってしまっていて、アクセシビリティの観点からはあまり好ましくないので、アンカーのtitle属性にサブタイトルのテキストを入れるパッチを提案してみた。
きっかけは ダイアリー設定を試しに変更 - 檜山正幸のキマイラ飼育記 から はてなダイアリーの見出し設定は2段にした方がいいよ - ぼくはまちちゃん！(Hatena) を読んで、そういえばtDiaryはどうなっていたかと思ったこと。ただ、実際には検索エンジンのクローラはtitle属性はあまり見ていないようで、SEO的には意味がないようだけど。
2008-06-25 [長年日記]
λ. RTM で Doug Ireton 氏の方法を使ってみる
これまでRTMのタグやスマートリストの機能はあまり活用していなかったのだけど、Doug Ireton 氏の記事 Remember The Milk 日本版 公式ブログ » Remember The Milkで快適GTD (ゲストポスト) を読んで、便利そうだったので取り入れてみた。
使いやすくなったとは思うけど、タグをちゃんとつけるのを忘れてしまったときに、タスクを見逃すことになってしまいそうで、そこは少し怖い。 あと、Doug Ireton 氏のコンテキストタグの分類は私にはちょっとしっくりこないところがあるので、その辺りは自分に合うように試行錯誤する必要がありそう。
2008-06-26 [長年日記]
![[買いだめしたお菓子]](./images/20080626_0.jpg)
λ. Tokyo Society for the Application of Currying
Tokyo Society for the Application of Currying (TSAC)に参加。oskimura さんから、TSAC について聞いてはいたのだけど、今回、池上さんが参加されるということなので、oskimuraさんを誘って思い切って参加してみた。 こういうデフォルト英語な集まりに参加するのは初めてだったけど、参加して本当に良かったと思う。
今回の内容は、池上さんからのQuickCheckとそのRuby版RushCheckの紹介。Curt Sampson さんによる QuickCheck in Erlang の紹介。それから ICFP の作戦会議。
QuickCheck in Erlang の話は、Types for Verification のときに John Hughes さんから 聞いたことがあって、そのときは良く分からなかったけど、今回は普通に理解できた。 ただ、ちょうど知人から プログラミングErlang(Joe Armstrong/榊原一矢) を借りたまま積読になっていたので、せっかくだからこの本でErlangの予習して行けば良かったなぁ。 ちょっと勿体ないことをしてしまった。
ICFPは私も参加するつもり。彼らとは別のチームで参加するとは思うけど。
関連
2008-06-27 [長年日記]
λ. Heinrich Kleisli の写真
Kleisli圏(Kleisli category)の名前の由来になった Heinrich Kleisli 氏の写真をたまたま発見。
2008-06-28 [長年日記]
λ. tDiaryに日表示から月表示へのリンクを
日表示からその月の日記一覧の表示に移動したいと思うことが良くあったので、簡単なプラグインを書いてみた。
# navi-this-month.rb
alias navi_this_month__orig__navi_user_day navi_user_day
def navi_user_day
result = navi_this_month__orig__navi_user_day
if @mode=='day'
this_month = @date.strftime( '%Y%m' )
result << navi_item( "#{@index}#{anchor this_month}", "#{navi_this_month}" )
end
result
end
def navi_this_month; "月表示"; end
2008-06-29 [長年日記]
λ. 『The Numbers Behind Numb3rs: Solving Crime With Mathematics』 by Keith Devlin and Gary Lorden
を読了。(後で書く)
Keith Devlin は、昔 20021206#p02 で書いたような話から、「infonの人」というか意味論とか基礎論の人というイメージを勝手に持ってたけど、こんなこともやっていたのね。
それから、これを読んで Numb3rs を観てみたくなったんだけど、US の iTunes Store だと一話$1.99で購入できるのに、日本の iTunes Store だと購入できないのね。とほほ。
関連
ψ ちこ [わたしはちょっと腰が引けていたので,まだ買ってません...面白そうだったら買ってみようかと思うので, 感想に期待して..]
ψ くるる [Keith Devlinは最近は研究というよりは啓蒙活動の人みたいですよ。毎週ラジオに出ているらしいですし。私たち集..]
ψ たけを [Numb3rsは自分も前から凄く観たいと思ってるんだけど、日本だとDVD化もされてなくて、なかなか観られる機会がない..]
ψ さかい [おお、こんなにコメントがあるとは珍しい。 ＞ちこさん 一般向けの本なのであまり個々の技術について詳しい説明はないで..]
ψ たけを [そのamazonのサイトをよく見るんだ。「予約できるようになったらお知らせします」と書いてあるだけで、まだ予約できな..]
ψ さかい [がーん、品切れじゃなくて、そもそもまだリリースされてなかったのね orz # 一応、お知らせEメールに登録しとこ……]
ψ かがみ [季節外れですみません。Devlin に関連する自分のページを検索したらこちらを捕捉。いま丁度 Constructib..]
ψ さかい [いえいえ、コメントありがとうございます〜]
2008-06-30 [長年日記]
λ. “A functional quantum programming language” by Thorsten Altenkirch and Jonathan Grattage
We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive semantics of irreversible quantum computations realisable as quantum gates. QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings explicit. Strict programs are free from decoherence and hence preserve superpositions and entanglement - which is essential for quantum parallelism.
量子コンピュータのための関数型言語QMLについて。QMLはゲートやそれに対応するコンビネータを直接記述するのではなく、普通の関数型言語のような書き方の出来る言語。 非可逆な量子計算を表す圏FQCと可逆な量子計算を表すその部分圏とを、非可逆な古典計算を表す圏FCCと可逆な計算を表すその部分圏とに対応させながら、言語を構成していっているのが面白い。 ただ、細部については、私は量子力学はもとより線形代数をちゃんと勉強していないので、良く分からず悔しい。
![[サンテザイオン]](./images/20080630_0.jpg)
