Today アクセスカウンター Yesterday アクセスカウンター

ホワット・ア・ワンダフル・ワールド

私は知識に何ものかを付け加え,また他の人々がより多くのものを付け加える手助けをした --- G.H.ハーディ

全記事一覧 << 2008/07 12345678910111213141516171819202122232425262728293031 2008/09 >>

プロフィール

あろは (alohakun)

  • Author:あろは (alohakun)
  • 若槻俊宏 (WAKATSUKI toshihiro)

    連絡先 : alohakun ___at___ gmail.com
    mixi : http://mixi.jp/show_friend.pl?id=182927
    twitter : http://twitter.com/alohakun

    abstract

    プログラミングという人間の知的行為を体系化し,単なる職人芸ではなく,サイエンスにするための研究をしています.

    具体的には,等価変換計算モデルに基づいた,仕様記述からのプログラム合成の研究をしています.

    もっと噛み砕くと,プログラムの正しさをどのように定式化し,どのような枠組みで,どのように変換を進めていけば,正しさを保証したまま,効率的なプログラムを手に入れることができるのか,ということについて研究しています.

    キーワード : equivalent transformation, computation model, programming paradigm, formal specification, program synthesis













    あわせて読みたい


    この日記のはてなブックマーク数


    スカウター : ホワット・ア・ワンダフル・ワールド


    Map









    FC2 BLOG RANKING

FC2カウンター

ブロとも申請フォーム

この人とブロともになる

Thinkpad X61s の HDD 換装

2008/08/07(木) 17:35:20

最近大学の研究室 PC が調子悪くて,ずっと Thinkpad X61s をメインマシンとして使用していたのですが.

モバイルノートと思っていたのですが,なかなかどおしてけっこう使える.普通にメインマシンになりますね (セカンドモニタをつなげば) まぁ,普通にデスクトップよりもメモリ多いですしね (2 GB 最初から積んでる) 音も静かで快適です.

しかし,やはり OS やアプリケーションの起動スピードだけは,HDD のせいかかなりもたつく感じがします.というわけで,7200 rpm の HDD に換装してみることに.D2D だけだと不安なので,ついでに古い HDD がバックアップメディアにもなりますし (DVD 焼けるドライブが無い… CD-R だと枚数が多すぎで.結局 HDD のバックアップは HDD が一番楽という)

HDD : HITACHI (旧 IBM のグローバルストレージテクノロジーズ) の 120 GB SATA 7200rpm HGST (HTS722012K9SA00)

北大横のツクモで,5 年間保障入れて 9505 円.

SATA usb 2.0 HDD 外付けケース : NOVAC の 2.5”SATA はい〜るKIT USB ベーシック (NV-HS210U)

札幌駅前のヨドバシカメラで 1480 円.

研究室の PC の怪しくなった HDD 換装のために,HDD と完全 HDD 交換 2008 を大学経由で注文済みなのですが,まだ届かないので,とりあえず Acronis TrueImage 11 の体験版を試してみることに.

とりあえず,普通にインストールして起動して,指示にしたがっていけば HDD のクローンが作れます.30 分もかかりませんでした (なぜか一回目に,C ドライブをロックして再起動してクローン処理が始まる直前,パーティションの構成が違う!みたいなエラーが出て失敗することがありますが,二回目だと上手くいったりします.謎).

ウェブを検索してみると,後は付け替えるだけで普通に起動した人が多いようです.

Thinkpad は HDD の交換も非常に簡単で,ネジを外して,カバーを横にスライドして,舌をひっぱって取り出して,HDD のネジを外して付け替えるだけです.ここまでは非常にスムーズ.

しかし,起動せず… ファイルや D2D は,全てちゃんとコピーされてるみたいなのに.
何か他のメディアで起動しようにも,今ドライブが手元に無いという.

とりあえず,元の HDD に戻して,今これを書いてます.最初 HDD 外すのに抵抗感があったのですが,何回も HDD 付けては外したので,すっかり慣れてしまいました.

起動した後 ThinkVantage の Rescue ane Recovery から,バックアップしつつリカバリすれば良さそうなんですが,面倒で今まで一度もバックアップしてませんでした.

しかたがないので,古い HDD で Windows が起動した後,R&R を起動して,バックアップを作り中.

その後で,もう一回クローンして,また起動しなかったとしても,バックアップから復旧するという計画.

しっかし,バックアップえらい時間かかりますね.0 % のまま 15 分ぐらい経過して,全く進展が無いので不安になってたのですが.その後,少しずつ進み始めました.現在は 13 % ぐらいで,推定残り時間 113 分とか,どんどん増えていきます.不安すぎる.

まぁ,一度ちゃんとバックアップを取っておくこと自体は悪くないので,気長に待ちます.




2 時間かけてバックアップとって,30 分かけて再びクローンディスクして,また結局起動しなくて,30 分かけてバックアップから復旧を試みたんだけど,結局起動せず.工場出荷時から,Windows システムだけのバックアップを試みてもだめ (また 20 分)

7 時間もかけたあげく,結局新 HDD を D2D からリカバリした.ここで工場出荷時の状態に戻るまで 1 時間.D2D できただけでも良かったのかな ? ある意味古い HDD に D2D (というか,旧システム丸ごと) のバックアップが残ってる状態なわけだし,これはこれで.

とりあえず,古い HDD を外付けして,Mozilla のブックマークとかだけ取り出して,Firefox インストールして,今これを書いてます.新しい HDD から初書き込み.

う〜ん,リカバリの時,ドライバ以外,何も余計なソフト入れない方が良かったかもね.

120 GB の HDD に 80 GB の HDD のクローンをリカバリしたので,40 GB ぐらい余りました.システムの管理で,D ドライブを作る.

とりあえず,私が Windows にまず入れるソフトウェア.なるべくソフトインストールしたくない,設定したくないデフォルト至上主義な人なので,必要最小限.

・必須
Thinkpad キーボードユーティリティ (一つ前の記事参照.ブラウザキーを殺す),Firefox

・研究関係
MinGW/MYSY,pLaTeX2e,ETI,MS-Office (研究室アカデミックパック)

ほとんど古い HDD からそのまま持ってきて終了かな.PATH の追加が面倒だけど…

RA の後からほぼ半日潰れてしまい,深夜まで苦労したかいあって,やっぱり 7200 rmp の HDD はキビキビしてて速い気がします (プラシーボ効果)

それにしても,コンピュータのトラブルでこんなに手間取ったのひさしぶりな気がする.昔,Linux の環境構築に夢中になってたころはしょっちゅうだったんだけど.最近はもう,コンピュータはパワーポイントと LaTeX が使えれば良い,という境地です.

結局何が悪くて起動しなかったのか謎.今度くる完全 HDD 交換で,研究室 PC の HDD をクローンする時は,もっとスムーズにいって欲しいなぁ… いいかげん,こんなしょうもないことで手間取ってられない時期です.




D ドライブができたので,ページキャッシュ(スワップ)ファイルを D に 4096 MB とることに.起動ドライブじゃないところにスワップを取るとなんか早くなるらしい.

ついでに regedit を起動して ClearPageFileAtShutdown とか DisablePagingExecutive を 1 に.大量にファイルをコピーして断片化がえらいことになってたので,デフラグもしまくりです.

せっかくなんで,高速化に貢献しそうなことは全部やっておきます.クラシックスタイルで,視覚効果とか最低はデフォですね.

まぁ,正直,それほど体感は変わらないかも (たぶん,慣れてきたあたりに 5400 に戻したら実感できるのかも.遅い → 速いは実感できないけど,速い→遅いはけっこうイライラすると思う).

デフラグとか,ディスクアクセスしまくるようなときの処理は,多少速くなったような気がします.HDD で律速になるからどうでも良いと考えていたんですが,やっぱり X61s は無印よりも CPU パワーが弱いのかな ? (バッテリーの持ちが無印よりも 1 時間ぐらい増えるから,ある意味長所なんですが,HDD 換装したらその唯一の長所も無くなる罠が w)

やっぱりなんかまだ起動が遅い気がするんだよなぁ… 1 分かからないぐらいなので,十分速いと言えば速いんですが.

あと 2 年ぐらいして SSD が安くなってきたら,また試してみよう.低消費電力も追求できる.




R&R で HDD 全体バックアップとか,HDD を酷使する作業の時,換装の効果が非常に顕著に出ますね.5400 rpm の時は,予想時間 110 分とか表示されていたのに,7200 rpm だと 45 分とかです (しかも,途中で延長されない.ガンガン進む) すごい速い
メモTB:0CM:0 このエントリーを含むはてなブックマーク | livedoorクリップ livedoorクリップ BuzzurlにブックマークBuzzurlにブックマーク newsing it!

Thinkpad X61s のブラウザキー封印

2008/08/06(水) 13:14:16

矢印キーの↑の左右に付いている 「進む/戻る」 (ブラウザキー) が鬼のようにウザイです.もう既に 10 回ぐらい,うっかり矢印キー押そうと思って押してしまい,twitter などに書いていた文章が消えてしまいました.

ちょっとぐぐっただけでも,同様の被害者多数.

IBM も,キーボード カスタマイズ・ユーティリティー にわざわざ 「ブラウザキーを有効にする」 なんていう項目作るぐらいなら,デフォルトで無効にするか,完全廃止にしておけば良いのに… 明らかにみんな迷惑してると思う.

とりあえず,上のサイトから (自分の場合は) 1qkcb8jp.exe とかいうファイルをダウンロードして実行.C:\drivers\WIN\KEYCUSTM が作られるので,その中の Setup を実行してキーボードカスタマイズユーティリティをインストール (再起動必要)

[すべてのファイル] > [ThinkVantage] > [キーボード カスタマイズ・ユーティリティ] を実行して,[キーの応答速度]タブの 「ブラウザ・キーを有効にする」チェックボックスをオフ.
メモTB:1CM:0 このエントリーを含むはてなブックマーク | livedoorクリップ livedoorクリップ BuzzurlにブックマークBuzzurlにブックマーク newsing it!

5.25 インチ光学式ドライブ用外付けケース

2008/07/27(日) 20:00:30

Thinkpad X61s には光学式ドライブが付いてないのでいろいろ不便です.研究室のアカデミックパックの MS-Office とかもインストールできません.

普通に USB か何かの外付けドライブを買っても良いのですが,けっこう高い.近所の PC ショップとかだと,一番安い中古でも 7 〜 8 千円前後はする感じでした (今時 CD-ROM だけのドライブとか売ってないし,たぶん逆に高い.外付け FDD でさえ 3 〜 5 千円ぐらいしてるし!Thinkpad X61 純正外付け FDD なんて 8 千円とかする)

どうしたものかな〜と思っていたら,IDE-USB の変換するやつさえあれば,デスクトップ機のドライブを外して note PC で使えるという情報を小耳に挟みました (昨日の北海道関数型言語勉強会の @osabou さんに感謝)

ヨドバシカメラで店員の人に聞いてみたら,なんか微妙に高い (7 千円前後) ものしか無かったのですが.北大前のじゃんぱらで,何やら怪しい商品を発見.3 千円と比較的安価.

メーカー:TIMELY 型番:R-CASE5.25B

けっこうデカいですし,ファンの音が大きいのですが,デスク機のコンボドライブを外して組み立てたら,普通に使えました.なんか説明書に,ドライブのジャンパーピンをマスターにするとか書いてたのですが,うちの (パソコン工房のオリジナル.5 年ぐらい前に OS 無しで 6 万円ほどで購入したもの)はなんにも無かったので,何もしなくても使えました.

デスクトップの光学式ドライブは比較的安い上に,速度が圧倒的に速いので,普通に外付けドライブを買うよりも拡張性が高くて良いんじゃないかと思います.どうせドライブなんて普段は持ち運ばないわけですし.

Linux でも,刺すだけで認識してくれる感じです./dev/sr0 あたりを mount したり,ogle とかの DVD に設定して Open すれば,普通に使えます.今まで通りデスク機でもドライブが使えるわけなので,このまま外付けのケースに入れたまま使い続けようと思います (デスク機にぽっかり空洞ができてしまったので,今は適当なビニール貼ってる)

# なんか画質がかなり乱れてしますいますが… どこが原因なのかの切り分けがまだできてません(ogle で開いたんですが,mpalyer とかだと普通に見えるのかも.今ちょっと apt-get dist-upgrade で mplayer の update がコケて,一時的に uninstall してる)

[ 1114.057947] usb 4-5: new high speed USB device using ehci_hcd and address 3
[ 1114.190952] usb 4-5: configuration #1 chosen from 1 choice
[ 1114.193971] usb 4-5: New USB device found, idVendor=05e3, idProduct=0701
[ 1114.193984] usb 4-5: New USB device strings: Mfr=0, Product=1, SerialNumber=0
[ 1114.193988] usb 4-5: Product: USB Storage
[ 1114.318208] Initializing USB Mass Storage driver...
[ 1114.320571] scsi0 : SCSI emulation for USB Mass Storage devices
[ 1114.321108] usbcore: registered new interface driver usb-storage
[ 1114.321115] USB Mass Storage support registered.
[ 1114.330826] usb-storage: device found at 3
[ 1114.330835] usb-storage: waiting for device to settle before scanning
[ 1119.364129] usb-storage: device scan complete
[ 1119.364718] scsi 0:0:0:0: CD-ROM COMBO IDE4816CO 0037 PQ: 0 ANSI: 0 CCS
[ 1119.432136] Driver 'sr' needs updating - please use bus_type methods
[ 1119.437223] sr0: scsi3-mmc drive: 16x/16x writer cd/rw xa/form2 cdda tray
[ 1119.437235] Uniform CD-ROM driver Revision: 3.20
[ 1119.437332] sr 0:0:0:0: Attached scsi CD-ROM sr0
[ 1119.472173] sr 0:0:0:0: Attached scsi generic sg0 type 5

まだ CD 焼けるかとかは未検証ですが,一応ちゃんと情報取れてるみたいです.

# cdrecord dev=/dev/sr0 -scanbus
scsibus0:
0,0,0 0) 'COMBO ' 'IDE4816CO ' '0037' Removable CD-ROM
0,1,0 1) *
0,2,0 2) *
0,3,0 3) *
0,4,0 4) *
0,5,0 5) *
0,6,0 6) *
0,7,0 7) *
メモTB:1CM:0 このエントリーを含むはてなブックマーク | livedoorクリップ livedoorクリップ BuzzurlにブックマークBuzzurlにブックマーク newsing it!

Thinkpad X61s (7666-77J) 購入

2008/07/17(木) 20:57:27

5 年ぐらいぶりに新しい PC 買いました.あと,我が家で初めての Windows 機です.

ずっと,学会やゼミ,勉強会などのために,持ち運びがしやすい note PC が欲しかったのですが.

期待していた新型の EeePC も,高い重いデカいと散々な感じで,一時は MacBook の中古で良い出物があった (core 2 duo 2.0 GHz / Mem 2 G / 英語キーボード) ので,心が動きかけたのですが.やはり,白い note PC とか無いなと (あと,大きくて持ち運びしんどそうだし.Mac はハードの選択肢がほとんど無いのが…).

そんなこんなでいろいろ悩んでいたところ,タイムリーなことに,先週の i-うぃん堂 の特価セールで,Thinkpad X61 と X61s が同じ値段で安売りされていました.夏の感謝セールとかで,送料が無料の上,8 万円以上のアウトレット品を買うと無料でメモリ 1 GB 増設キャンペーン (計 2 GB積まれる) とかもありーので,代引き手数料込みで 85430 円.

やはり Thinkpad は超カッコいい.これだよこれ,他の軽量モバイル note PC など全くに相手にならない.これは買うしか無いでしょう.

X61 と X61s のどちらにしようか迷ったのですが,

(1) 基本的に s の方が軽量化のため元値が高価 (231000 円 vs 168000 円)なのでお得 (まぁ,アウトレット品なので微妙なんですが)

(2) X61 の方は CPU クロックが上 (core 2 duo 2.2 GHz) なのは良いものの,発熱量が多そう (Matz さんが低温火傷という事例あり).X61s は 1.4 GHz なので,クロックは下ではあるが,もともとモバイル note PC に速度など求めてないので,発熱量が低い方が良いに決まってる.

(3) X61 は Windows Vista が初期インストール (X61s は XP) だが,おそらくビデオチップがチップセット内臓で,メモリが 2 GB 程度で HDD も低速の X61 では使い物にならない

(4) X61s ならば重量も 1.3 kg 弱ぐらいなので,1 kg 弱ぐらいの UMPC と重さ自体はそれほど変わらない (X61 だと 1.43 g ぐらいで 500 g ぐらい違う).

というわけで X61s に決定しました.X61 が X30 系列 (パワフルモバイル)で X61s が X40 系列 (スリムモバイル) らしいです.

僕は Thinkpad の X40 に強い憧れがあったのですが,その後継機種がこんなに安く手に入るとは.

防水キーボードでコーヒーがこぼれても大丈夫「火事の炎にさらされ、消火ホースからの水を浴び、2階の窓から放り投げられ、さらに数昼夜の間ずぶ濡れになった家財道具の残骸にまみれ」ても全てのデータが無事だったなど,数々のレジェンドに彩られた愛すべき過剰品質,プロフェッショナル御用達の高級機種の代名詞だった Thinkpad.

それが中国企業 lenovo によりコモディティ化し,単なるイチ家電製品になってしまったということなのでしょうね.常に僕達の憧れだった,赤緑青に輝く IBM のロゴが消えてしまったのは悲しいですが,そのおかげで,僕のような貧乏学生の手にも届く価格帯にまで降りてきてくれたわけで,これはこれで大変素晴らしいことだと思います.

まだ今のところは IBM のチェックもしっかりしていて,生産体制にも以前と比べて大きな変化は無いようですし,X61 は評判がなかなか良い感じです.大事にしようと思います.
メモTB:0CM:0 このエントリーを含むはてなブックマーク | livedoorクリップ livedoorクリップ BuzzurlにブックマークBuzzurlにブックマーク newsing it!

1+1=2を証明するためには1万ステップ以上かかるよ,という話

2008/07/17(木) 18:31:55

なんかすごいサイトを見つけてしまいました.

Metamath Proof Explorer Home Page

数学の基礎付けに関する 20 世紀の記念碑的偉業と称えられながらも,歴史上何人がこれまで読破したのか,と常にネタにされる Principia Mathematica (12 万円,2000 ページ!) に,1+1=2 の証明が載ってるっていうのはわりと有名な話だと思いますけど.

追記 : Radium Software Development 2006-06-30 : Proof that 1 + 1 = 2

# ちなみに,三巻組の大著の全文をオンラインで見ることができます."From this proposition it will follow, when arithmetical addition has been defined, that 1+ 1= 2."

このサイトでは,全ての定理が索引付けでハイパーリンクされていて,例の 1 + 1 = 2 の証明も,トップレベルから全てのサブ命題を追うことが可能になってます.

Theorem o1p1e2 4165

なんと 1518 個のサブ定理を 11086 ステップかけて証明する必要があるそう.

定理っていうのは,プログラムにおけるサブルーチンみたいなものなんですけど.
もし,途中の定理を全て「インライン展開」すると 10 億ステップを超えるとか.




ちなみに,us.metamath.org では,現代公理的集合論 ZFC (1+1=2 程度ならば,公理 C は必要ないみたいですが) を数学の基礎においているみたいですが,PM の初版では分岐階型理論 (theory of types),2 版では単純階型理論 (simple theory of types) という定式化が採用されているそうです

ラッセルの論理学は確かに時代後れである。ゲーデルその他の数理論理学者の批判をまつまでもなく、ラッセルの論理学が厳密さを欠いているということは、いまや周知の事実である。たとえば、『数学原理』には公理は与えられているが、推論法則を欠いている。したがって、やかましくいえば、『数学原理』において公理以外の定理を導出することは不可能である。また、初版において用いられている分岐階型理論においても、また、一九二五年に発表された第二版において採択された単純階型理論においても、その定式化は甚だしく厳密さを欠いている。そして、これらの理論が組合せ論理学の立場から正しく再構成されたのは比較的最近のことなのである。

(中略)

すでに述べたように、『数学原理』に内在するいろいろの技術的欠陥を現在の進んだ立場からあげつらうことはむづかしいことではない。しかし、理性の分析、あるいは、その再構成という仕事に哲学史上はじめて着手することによって、十九世紀的理性、あるいは、ドイツ観念論的理性と訣別して現代への第一歩を踏みだしたという点において、『数学原理』に代表されるラッセルの論理学の功績は永遠に残るであろう。したがって、『数学原理』が現代ヨーロッパにおげる最高の思想的所産であるというボヘンスキーの手放しの礼讃もけっして誇張ではあるまい。

ラッセルは哲学者で,メタ数学は 「数理哲学」 なんですよね.数学の道具を使って,人間知性を哲学している.

もう一つ引用.

バートランド・ラッセルのポータルサイト (著書解題4)ラッセル著『数理哲学序説』(中村秀吉・解題) 『ラッセル協会会報』n.4(1966年5月)pp.3-5.

ラッセルのこの方面で業績は、師のホワイトヘッドとの共著である大作『数学原理』に集大成されているといってよい。かれは1900年から1910年頃までの、かれの人生における最良の10年間をこの仕事の完成に惜しみなくささげたのである。しかしこの本は非常に大冊であるばかりか、かなり冗長な、ほとんど退屈な記号の羅列なので、実際に通読した人はほとんどないといっても過言ではあるまい。これを通読した人は一ダースしかいないだろうとか、ことによると、これを書いたラッセルとホワイトヘッドだけではなかろうか、などといううわさもたてられたほどである。しかしラッセル自身はここにとりあげる『数理哲学入門』において、ほとんど記号を使わないでその平易な解説を試みたのである。この『数理哲学入門』は、ラッセルが1918年5月から1919年9月まで(松下注:「1918年9月」の間違い)、反戦運動のかどで、獄につながれていた間に一気に書き上げたもの(注:獄中での執筆)である。われわれは彼の集中力にも驚くのであるが、同時に、いかほど自分がやったことの要約とはいえ、ほとんど参考書もない不便ななかで、これほど明晰かつ性格に『数学原理』の要点を叙述できたことに一驚を禁ぜざるえないのである。
本書ではまず数学のもっとも基本的概念である自然数列から問題が説き起こされ、自然数の定義が導入される。がんらい哲学では、自然数を何か感性的対象とふつうの一般者との両面をもったもの、ないしその中間者として、独自の対象と考えられてきた。一方、ペアノは自然数の公理系をつくるのに成功し、ある命題群を満足する勝手のものとして自然数を陰伏的に定義した。ラッセルはこの両方の考え方にあきたらず、個々の自然数を相似な、個物のクラスのクラスとして定義した。これによって個々の自然数は純粋に論理的な慨念であるクラスに還元されることになり、その把握に何か特殊な直感力のようなものを必要としなくなったのである。同時に、ペアノの公理とは違って現実的個物との関係もつき、一と他の関係のような哲学的アポリアにも一応の答を用意できることとなった。
メモTB:1CM:3 このエントリーを含むはてなブックマーク | livedoorクリップ livedoorクリップ BuzzurlにブックマークBuzzurlにブックマーク newsing it!

最近のコメント

リンク

このブログをリンクに追加する

最近のトラックバック

人生の残り日数

日本人男性の平均寿命は 28700日.

RSSフィード

カテゴリー