日々の流転

λ. みな死ね矢

また、懐かしいものを…　たしか、ロマサガⅡにもあったな、グリムリーパーの固有技で。

λ. 時計

昨日書くのを忘れたが、先月の22日に修理に出した我が愛しの腕時計がようやく帰って来た。何でこんなにかかったんだろ。まあ、ちゃんと直ったからいいや。

λ. 「1」「1」「9」「9」4つの数字で「=10」になるような式を作れ

スペースモラトリアムノカミサマより

「1」「1」「9」「9」4つの数字と四則演算、及びカッコを自由に並べて「=10」になるような式を作れ。ただし「19」や「91」などの2桁の数字にするのは無し。あくまで全て1桁の数字で扱うこと。指数も無し。

λ. むむむ…、解けたっ。\ 発想の転換というより、この手の問題では良くあるパターンの答えのような気がする。

λ. 訪問者にやさしいWebサイト作り

ケシゴムに勧められたので、試してみた。う〜みゅ。

あなたのサイトの優しさ度は　156　です。
このチェックは、最高２００，最低０となっています。

訪問者に対してそこそこ優しいサイトに出来上がっていますが、もう１ランク上のサイト作りを目指して欲しいですね。

また、各項目ごとの点数は、
　トップページ：50／50　使いやすさ：27／60　
　アクセスのしやすさ：48／50　そのほか：31／40　となっています。

λ. X-Bender

ところで、Slashdot-Jで送られてくる、X-Benderって何?　fortuneみたいなもの?

λ. 東京電力株主総会 @ 日比谷公会堂

を見学してきた。10時開会で13時ごろ閉会。噂に聞いてた反原発運動とか色々見れて勉強になった。

つーか、何かあるとすぐに「議事しんこー」とか「りょーかい」とか声を張り上げるオッサンがすぐ近くに座ってて、すんげーウザかった。他にも沢山いたし、きっとみんな社員株主なんだろうなぁ。

ところで、脱原発・東電株主運動の主張はあまりに理想主義に走っていてアレかと思ったのだけど、取締役会のそれに対する反論は遥かにダメで、お話にならなかった。

そういえば、南社長の例の発言に関しても予想通り質問があったのだけど、これも結局はぐらかされてしまった。

　電力自由化をめぐり、電気事業連合会の南直哉（のぶや）会長（東京電力社長）は２５日の記者会見で、「原子力は経営努力を前提に取り組むが、幅広く負担する新たな仕組みが必要かも知れない」と述べ、自由化の進展次第で、多額の費用がかかる原発―核燃料サイクル政策を維持するため新制度や税負担など公的な支援を求める考えを示唆した。経済産業省・総合資源エネルギー調査会で行われている自由化議論で、「切り札」の原子力を盾に劣勢を跳ね返す狙いもあるとみられる。

　電力の小売り自由化が進み、競争が激化すると、原発を持つ大手電力会社は、原子力を持たない新規参入者との競争で不利になる可能性がある。特に規模が小さい地方電力は、原発の新規立地について「４０年先を見込む巨額投資は困難になる」（関係者）と危機感を深める。

　南会長は「原子力は、エネルギーセキュリティーや二酸化炭素の排出量削減に不可欠。しかし、自由化によって経営判断として成り立たたない会社が出てくるかも知れない」と説明。支援策として「いろいろな方法があると思うが、税金もひとつ」と語った。自由化の範囲を抑制して一定の需要を保証したり、新規業者の送電線使用量に料金を上乗せしたり、核燃料サイクル推進に税を使う手法などを検討していると見られる。

　政府と業界はこれまで、原子力発電のコストの「安さ」を推進の根拠にしていた。政府が９９年に示した試算では、１キロワット時当たりの発電単価は原子力が５・９円と、石油火力１０・２円、天然ガス火力６・４円に比べて低い。しかし、実際の原発の単価は東京電力で８円程度とされるうえ、今回の南会長の発言は「安さ」を事実上否定した形だ。　【高橋秀郎】

［毎日新聞１月２５日］ ( 2002-01-25-23:21 )

λ. 大学院入学試験　2次試験　面接

9:10分集合で9:30ごろから始まった。奨学金の面接の方が10時集合だったので、早めに順番が来ると思っていたら、案の定最初に呼ばれたグループだった。部屋に入ったら、左から萩野先生,服部先生,川添先生,中村修先生という配置で、知っている先生が3人もいたせいか、落ち着いて受け答えすることが出来た。中村修先生の突っ込みがちょっと厳しくて、川添先生のフォローに助けられりしたけど、あれは冷静になればちゃんと反論できたはずの質問だったので、ちゃんと反論できなかったのはちょっと心残りだ。

とりあえず特に問題も無く面接を終えられたので、多分受かってるだろう。

λ. GAO奨学金の面接

入試の面接は違ってこっちは失敗。多分落ちただろう。敗因は緊張してしまって筋道だった説明が出来なかったことと、あと自分の研究の社会的な意義についてこれまであまり考えたことが無かったことだな。次は負けねぇ!

ちなみに、左から楠本先生,徳田先生,会田先生という配置だった。あと、最後の方で楠本先生に「卒業出来るの?」って訊かれたけど、それは反則ですってば…… (苦笑)

λ. 知識発見法

• MAP推定
• 最尤推定
• ナイーブベイズ
• ベイジアンネットワーク
• Rich Caruana and Alexandru Niculescu-Mizil. An Empirical Comparison of Supervised Learning Algorithms

今日はAbduction勉強会はお休み。

λ. サイコクラッシャーでマリオ

λ. Coq の extraction

<URL:http://d.hatena.ne.jp/syd_syd/20070622#p1> と <URL:http://www.eva-01.jp/d/?date=20070623#p03> あたりを読んで、なるほどと思った。 Coqではextractionをそういう風に使うのね。 AgdaだとそもそもSetとPropの区別が無いから、extractionのようなことをあまり意識したことがなかった(Agdaで書くと下みたいになっちゃうし*1)。考え方の違いが面白い。

Decidable :: Set -> Set
Decidable P = P `Or` (Not P)

lemma :: (C::Context) -> (e::Expr) -> (t::Type) -> Decidable (C |- e : t))
lemma = ...

typeCheck :: (C::Context) -> (e::Expr) -> (t::Type) -> Bool
typeCheck C e t =
  case lemma C e t of
  (inl x) -> true
  (inr y) -> false

λ. お菓子買いだめ

今月のお菓子買いだめ。 ビックリマンとか懐かしいなぁ。

λ. 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は私も参加するつもり。彼らとは別のチームで参加するとは思うけど。

関連

• TSAC Meeting June - Tokyo Society for the Application of Currying Blog at Starling Software
• 6月の Tokyo Society for the Application of Currying (TSAC) に参加します - Inemuri nezumi diary(2008-06-19)
• Tokyo Society for the Application of Currying (TSAC) - TABのつもりですか？(makeは無慈悲なbuildの女王)

λ. WAKE UP キャンペーン

住信SBIネット銀行の WAKE UP キャンペーン というのに当選。 さわやこおふぃというのを貰った。 わーい。

λ. 日常

今日は歯医者に行って、床屋に行って、それから数学基礎論講演会、CLTT読書会と、なかなか忙しかった。

λ. 第３回数学基礎論講演会「ゲーデルの定理　その後１」

題目

ゲーデルの定理　その後１

講師

田中 一之 （東北大学）

内容

この講演会は，同講師による数学基礎論入門シリーズの第３回です．今回と次回（秋予定）はゲーデルの不完全性定理のいろいろな証明について勉強します．

前回に続いて、田中先生の講演第三弾。今回も場所は東工大。 前半はほとんど雑談で、面白かったんだけど、配布資料にそのスライドが含まれていなかったのがちょっと残念。 あと、途中で抜けてCLTT読書会に行こうと思っていたが、雑談のやこれまでの繰り返しの部分が長くて、それはそれで面白いのだけど、なかなか聞きたい話に入らず、抜けるに抜けれなかった。

• ルネ・マグリット(René François Ghislain Magritte)はエッシャー(Maurits Cornelis Escher)と同じ1898年に生まれ。エッシャーよりもむしろマグリットの絵の方が不完全性定理的ではないか。
• こうした循環的な構図というのは昔からある。
• ヤン・ファン・エイク（Jan van Eyck) 「アルノルフィーニ夫妻像」
• シェークスピアと唯名論と劇中劇。当時の舞台では女性が演じるという慣習がなく、女性役も男性が演じていた。男性が女性を演じ、その女性役が劇中劇で男装し……
• カントールはシェークスピアとベーコンが同一人物という論文を書いている。
• 直観主義からの攻撃があったから、論理主義や形式主義がしっかりしたものになっていったという面もあるのではないか。
• 無限の立場 (ルディ・ラッカー)
• クロネッカーは自然数の絶対的実在性を主張。代数的数唯名論的存在、他は研究に値しない。
• 集合論 vs アンチ集合論
• 藤沢 利喜太郎 はクロネッカーに師事し、彼の主張を日本に広めた
• ゲーデルコーディングは、記号を数といつかみ所のないところに移しているのであって、その逆ではない。
• 前回のω無矛盾性と健全性の関係についての質問への回答
  • ω無矛盾 → Π₃健全
  • ω無矛盾 /→ Σ₃健全
• コルモゴロフ複雑性
• チャイティンの主張の問題点
  • 彼の不完全性定理は、定理の複雑さについては何も言っておらず、複雑さについての定理である。実際、「K(s)>n」の形の真なる言明はnより大きい複雑さをもつことは明らかであるが、その言明の証明不可能性の要因が、言明の複雑さであるとはいえない。
  • 定理が公理よりも大きい複雑さを持ちえる。例えば「すべての列xについて，x=x」を唯一の公理として持つ理論は非常に複雑性が低いが、この理論の定理の中にはどんな複雑な列sに対する「s = s」の形の言明もある。それゆえ定理の複雑性は非有界。
  • 決定不能な命題が必ずしも自己言及的言明の形式化である必要はないことを強調したことは重要であが、この点はディオファントス方程式の決定不能製によってもすでに十分例証されている。
• チャイティンの主張: Ωの重要性
  • チャイティンは次のようにいう: オメガのビット並びは論理的に既約、つまりそれよりも単純な公理からは導くことはできない「原子的」な数学的事実、互いに関係を持たずいわば「理由なく真である」ような事実の無限列である。
  • しかし、「オメガのn番目のビットがiである」という言明は、自明でも明らかに真でもない。「より単純な公理から得られない」と主張する根拠も明らかではない。さらに、公理が定理より簡単でなくてはならないという見方は、チャイティンの別の考えに反する。
  • 絶対的な意味で、何が証明できるか否か、説明できるか否か、理由を与えられるか否かについて論ずる理論的な根拠はない。
• パリス＝ハーリントンの命題
  • 集合論のモデルの研究で巨大基数について研究していて、算術についても同じようなことがあるというのをパリスがみつけた。
  • ハーリントンがそれを組み合わせに結びつけた。
  • ラムゼイの定理をちょっと直してパリス=ハーリントンの命題が得られる。
• ヘラクレスとヒドラの戦い
  • 上には伸びないで横に広がるだけ
  • 上の方を切って行けばそのうち退治できる
• 超限順序数
  • 対数の目盛りにするようなもの
• グッドスタイン列
• ゲンツェンが自然数論の無矛盾性を証明したのもε0までの超限帰納法を使って
• 急増加関数f_α
  • リカージョンをα回繰り返して得られる関数
  • f_ωはだいたいアッケルマン関数
• 次回予告: 2010年10月頃「不完全性定理　その後2　—モデル論的議論—」

λ. CLTT読書会 第3回

というわけで、こっちには遅刻。 やっていたのは、 1.4 Cloven and split fibrations 。 定義1.4.8のUFam(ω-Sets)が圏になっていることを理解するのに、みんなちょっとつまずいていた。

• CLTT読書会 第3回 : ATND
• 私が来た後の板書の写真
• 前回

二次会

• 熱力学と圏（１）
• 熱力学と圏（２）