砂山のパラドックスの変形バージョンです。以前考えて、すっかり忘れていたのですが、ふと思い出したので、ここに書いておきます。 数百年前の遺跡は、地中に埋まっている。つまり、当時の人の暮らしていた地面の上に、いつの間にか何メートルもの土が積もっ…

書き味が気に入り最近ずっと使っていたのですが、引っ越し時に段ボールの上で書類を書いていて段ボールを突き破ってしまった際に、ペン先を傷つけてしまい書けなくなってしまいました。しょうがないので本日三宮の店で予備を含め三本購入。スタビロ 水性ボー…

本日、逸翁美術館に行った後、隣の池田文庫に行き、図書館で本をぱらぱら見ていたんですが、その時見つけたネタをご紹介しましょう。よく、「訪米した代議士が、会談中にオヤジギャグを言って、通訳がパニックになる」という冗談があるじゃないですか。有名…

長さ0.5cmぐらいの小さなマカロニなんですが、シチューに入れると素晴らしい味です。 [rakuten:otokonodaidokoro:10001492:detail]

鉄道の始発、バース駅発ブリストル駅行きは、平日は6時半ごろだが、日曜朝は8時半だそうだ…日曜の朝は教会に行け、ということなんだろう、多分。

「とにかくまずコレを読め」（by P先生)。「すばらしかった」そうです。 参考：檜山さんのところの資料編

19:30-20:30。 「リーバス警部」シリーズで有名な犯罪小説作家のイアン・ランキンの講演会に行ってきました。聴衆は年配の夫婦が中心で70人程度。本講演は最新作 "The complaints" の販売促進の一環らしく、The Complaints作者: Ian Rankin出版社/メーカー: …

Persuasion (Penguin Classics)作者: Jane Austen,Gillian Beer出版社/メーカー: Penguin Classics発売日: 1999/06/01メディア: ペーパーバックこの商品を含むブログ (1件) を見るMansfield Park (Penguin Classics)作者: Jane Austen,Kathryn Sutherland,To…

バースの書店、各種トークイベントを開催。サイトはこちら。

イギリス国鉄版「駅スパート」（もしくは路線検索）、サイトはこちら。

メモをとっておかないと忘れそう。The Embarrassment of Riches: An Interpretation of Dutch Culture in the Golden Age作者: Simon Schama出版社/メーカー: Vintage発売日: 1997/12/08メディア: ペーパーバック購入: 1人 クリック: 1回この商品を含むブロ…

Pride and Prejudice (Penguin Classics)作者: Jane Austen,Vivien Jones,Tony Tanner出版社/メーカー: Penguin Classics発売日: 2003/01/01メディア: ペーパーバック購入: 2人 クリック: 7回この商品を含むブログ (53件) を見るI Served The King Of Englan…

数学者には、数学の問題に集中するあまり、周りが見えなくなる逸話を持つ人が多い。そして、それは飲みの席では鉄板ネタとなる。 というわけで、本日紹介された、著名な某教授のネタ。 院生時代の話です。セミナーに現れた彼を見て、指導教官は仰天しました…

http://www.skyscanner.jp/ ヨーロッパの空港で必ず見かける EasyJet や RyannAir の検索が出来て便利。

バースの予習のため、Cが本屋で購入。Emma (Penguin Classics)作者: Jane Austen,Fiona Stafford出版社/メーカー: Penguin Classics発売日: 2003/04/01メディア: ペーパーバック購入: 1人 クリック: 6回この商品を含むブログ (5件) を見る

Agda コードはUTF-8なので、Texでコードの紹介文を作成しようとすると、コードをそのままコピペしたのでは文字化けしてしまう。特に数学記号（例えば）などは、いちいちsjis へ変換するのは大変。 で、MacOSX上で、UTF-8をそのまま使用・変換できる ptex を…

以前、一度MacBookAirのAgdaをインストールしたのだが、間違えてインストールした際のユーザアカウントを消してしまい、新しいユーザアカウントで再インストールをしなければいけなくなった。この一週間というもの悪戦苦闘していたのだが、本日昼間にやっと…

国際会議の発表準備のために、MacBookAirにBeamerをインストールしようとして、この二週間というもの悪戦苦闘していたのだが、本日夕方にやっと完了したので、苦労した点を備忘のためメモしておく。 インストール方法は こちら参照。 sourceforgeからlatex-b…

こちら参照。 カレンダーを登録しても、サーバーの混み具合（？）によって「カレンダーが見あたりません」と出ることもあるので注意。

のために、本日やっとdropboxを導入した。ネットストレージ+シンクロ+バックアップソフトで、無料2GB。これは便利です。

私は、昔からずぼらな性格で、 スケジュールやto do 管理などがうまくできた試しがありませんでした。しかし、今年度になって仕事量が増え、日常業務を廻して行くのも困難な状況になってきました。というわけで、昨年末から試行錯誤した結果、以下のようにな…

本日、資料整理をしたところ、机の上にプリントアウトの山を発見しました。どれも途中まで読みかけで、そして紛失したと思っていたものばかり。自分でもタイトルを忘れていたので、備忘を兼ねてメモっておきます。 "Cut elimination for Zermelo's set theor…

私は、予定の管理にグーグル・カレンダーを使っているのですが、その内容を携帯で見るにはwebアクセスをする必要があり、携帯電話のカレンダーとGoogleカレンダーの同期はずっと方法が分かりませんでした。途中にMacをかませる場合、シェアウェアのspanning …

我が家のネットワークは、リビングにAirMacExtreme（旧型）があり、書斎のiMacと無線でつながっている。しかし、9月にMacを買い替えてから、ネットの反応速度が急激に落ち、その理由を探していた。本日理由が分かったので備忘のためメモ。 どうやらAirMacの…

言語L1, L2, L3 があり、L1-> L2 と L2-> L3 の間が翻訳可能であっても、L1 -> L3 の間の翻訳が不可能な例を考えよう、という話。以下の例は、今年の前半、読書会のときに思いついた（本当に思いつきなんですが）。IG氏の原稿を読んでいる際にふと思い出した…

本日Ktさんから教えていただいた話、備忘のため。

意気消沈すると、少し感傷的になり、ちょっとしたことで涙もろくなることもある。 先週末、東京への出発の直前、変なメールを受け取った。本文は空白、添付はpdfファイルが一つだけ。SPAMかと思ったが、帰ってきた後ファイルを開いてみた。すると「あなたの…

これまで誤解していたが、Agda2のdata typeの型の定義で、 (n : Nat) -> TermSeq n -> Set みたいな定義はよくて（ちなみに TermSeq nは長さがnのTermの列）、 (n : Nat) -> Term -> Pred (n-1) （ただし Pred 0 = Set） みたいな定義は不可能だ ということ…

本日の読書会で話題になり、h師とK氏に指摘されたので。論理的体系の代数的意味論は、哲学者には評判が悪い。なぜだろう、という話。 代数的意味論で、例えば論理式 A の「意味」は（designated value の議論を引用して）{ B : B→A の代数的な値が 1} という…

どうでもいい話だが、携帯電話、7年間同じものを使っていたが、さすがにバッテリーがダメになったので、某社の705NKに切り替えた（番号は変わりません）。ここでは一応個人的な備忘として、セットアップをメモっておく。 Gmail: ブラウザで http://gmail.com…