Diary?::2009-03

2009-03-01
Sun

(18:07)

なんか風邪ひいたっぽい。そんなに症状は酷くないけど、やたら体がダルい。

明日までに治ってるといいんだがなあ（ちょっと明日は休めないんで）。

2009-03-02
Mon

(20:31)

今日は散々な一日だった。

風邪ひいてるけど、ちと重要なレビューが午前中にあるので出社（午後から病院行く予定だった）
出社後、レビューは午後からの予定であることが判明（明日の予定と間違えてメモってた）
結局「とっとと病院行ってこい」と言われて早退

これだったら一日休めば良かったな。

(21:57)

多少は回復してきたので Web 見てたら、マジコンに輸入・販売の差し止めと在庫の廃棄を求める判決だってさ。というか既に仮執行の段階? まあ当然だろうな。

ところで「マジコン禁止したらユーザーがさらに減る」とかいう意見をたまに見かけるんだけど、これ本気で言ってるのかな。マジコン対策などの研究開発に企業のリソースが割かれていて、それが本体価格に跳ね返ってきたり、あるいはゲームの開発費用の削減に繋がったりして、それでクソゲーやガッカリゲーが出てるかもとかその程度の想像力も働かないのかねえ。言っとくけど俺はクソゲーなんざタダでもいらねえぞ。

確かにこの手の奴はイタチごっこになったり、あるいはユーザに不便を強いる結果になってバッシングを受けたりって事に繋がるんだけど（CCCD 騒動とかな）、ぶっちゃけ効果のほどが怪しくても法的措置や回避技術の開発ってのが求められたりするわけだしな。

2009-03-04
Wed

(19:49)

医者から処方された風邪薬がやたらと眠気を誘発するので一日しんどかったが、まあ明日一日で完治するだろ。幸い明日は先方の担当が休暇で俺も特に急ぎの作業がないので、ついでに休みを取ることにした。

それで明日はセブンスドラゴンの発売日だけど、とりあえず買うだけ買って積んでおくことになりそう。何せまだ冒険記の方が完結してないわけだからなあ（大体終わりは見えてるんだが）。流石にここで一旦中断するのは気持ち悪いし、何より妹二号が許さんだろ。

2009-03-06
Fri

(20:50)

病み上がり早々に見たソースコードがダークマター以外の何者でもないというのは、精神衛生上非常によくない。一体何が凄かったのか、かいつまんで書いてみる。

まず最初に次のようなユーティリティクラスがあるとする。というかあった。

public class BizDateFormatter {
    /**
     * 和暦変換。
     * 引数のオブジェクトから日付メンバを取り出し、WYYMMDD形式の文字列にして返す。
     */
    public static String toWareki(SomeObject aObj) {
        //実装は略（諸事情により結構長い）
        //ちなみに他のメソッドはない
    }
}

これだけなら別に良かったんだが、次のようなクラスがあるのを知ってのけぞった。

public class BizDateFormatter2 {
    /**
     * 和暦変換。
     * 引数のオブジェクトから日付メンバを取り出し、をWYYMM形式の文字列にして返す。
     */
    public static String toWareki(SomeObject aObj) {
        //BizDateFormatter#toWarekiのコピペ改変コード。一致率は90%ほど
        //そのメソッドを呼んで戻り値をちょこちょこと修正とかいう発想はないらしい
    }
}

この時点でケツと頭が四つに割れそうになったが、この後さらに BizDateFormatter3, BizDateFormatter3s, BizDateFormatter4, BizDateFormatter4s といったふざけたクラスとコピペメソッドが出てきて、なんかもうどうでも良くなった。これらの中身は/区切り日付処理が入ってるとかそういう違いがあるだけで他は全部コピペ、コメントも当然コピペ、そしてそれはソースの内容と合ってない。コーディングの掟では「コピペ禁止がもっとも有用なコーディングルールかもしれない」というネタがでてきたけど、そういうネタが成立するには笑うに笑えない現実が必要で、今日直面したこれはその一例だ。

他にも「2000行のメソッドを長いからといって分割させたら『カット&ペーストで別メソッドにして、コンパイルエラーが出なくなるまで分割後のメソッドの引数を増やす』という大技を繰り出された」など、傍から見てる分には面白いけど当事者としては己れが殺人鬼にならないように自制するのが大変な事例は腐るほどあり、まともなコードを書くつもりのない奴とそのような戯け者を解雇しない経営者をアフガンの地雷源に放り込まない限り俺は長生きできないなと思ったので日本政府は殺人許可証を俺に発行しろ。

あとこれは今となってはどうでもいいが、俺と同じチームに投げ込まれた技術者というか技術者モドキの中で一番凄かったのは俺がソースコードの記述例に「中略」の意味で書いた「...」とか「:」をそのまま書いて「コンパイルエラーになります」とか言ってきた奴で、そいつの尻拭いで俺は徹夜作業とかをするハメに陥ったりしたのだが、まあ今となっては笑い話だ（厳密に言えば、このような人生の浪費としか言えない体験はネタにでもしないと元が取れない）。

2009-03-07
Sat

(21:59)

エトリア冒険記、ようやく完結。こんなに時間がかかったのは逆鱗マラソンのせいで、しかもネタ的に全然面白くないときてやがる。しょうがねえからそこはすっ飛ばして、医術防御なし、アダマースなし、真竜の剣なし、そもそもレベル最大のメンバーが2人とかいう条件でフォレスト・セルを倒してみたというか倒すハメになった。さすがに乱数固定を使わざるを得なかったが（トラッピング戦術だと三回目のランダム行動の前にケリがつくことが多いので、勘で倒せなくもない）、それでもまあ面白いというかドラマティックな戦いだった。

他の部分も偉大なる赤竜をファイアガードと医術防御なしで倒すとか、所々で新しい解き方をできたので、逆鱗マラソンを除けばまあ割と満足な結果かなあ。逆鱗というかいわゆるレア狙いはもうプレイ時間の水増しでしかないと俺は思っていて、その点は世界樹IIがかなり解決してる（博識入れればなんとかなるし、単なる激レアがない）。

とりあえず後書きの替わりにいくつか書こうと思うけど、まずは今回の脳内ストーリーの登場人物、というかその職業が決まるまでのことについて。まず最初に決定していたのはカースメーカーの加入で、これは鞭ダークハンター中心で運用する際には必要不可欠といえる。他の職業でもサポートは出きるが、斧ソードマンは頭封じしかないし、そもそも普通にスタンスマッシュした方が強いので除外。レンジャーに至ってはサジタリウスの矢とダブルショットが鬼のように強く、普通にレンジャーメインになるので除外。なので鞭ダークハンターのサポートはカースメーカーが適任なのだけど、そうなると初期メンバーの誰を外すかという問題になる（4人旅は却下）。

ここで候補に上がるのがアルケミスト。ちょうど第4階層あたりでスキルポイントが足りなくなり、力不足を感じて自ら離脱するにはうってつけ。上に書いた通り、他の職業は離脱するインセンティブに乏しいしね。ちょうど物語の核心部分でいなくなるけど、まあそこはいろいろと補間しよう。ちなみにアルケミストが主人公っぽく進むことになったのは俺としても想定外で、キャラクターが勝手に動き出して収拾がつかなくなった。最初にプレイしたときは第4階層で離脱して戻ってこなかったんだけど、結局は第6階層以降で復帰することになった（実際のところ、第6階層はアルケミストがいると楽だ）。

あと時間がないという理由で経験値稼ぎを殆どせずに進めたので、殆どのボスにレベル補正で大ダメージを受けるという有様で、第6階層に至っては初回プレイ時よりも10以上低いレベルで突入するハメになってしまい、勝手に転がり出したキャラクターも相まって二周目なのに自分で展開がわかんねーという割と前代未聞な状態になった。フォレスト・セルに挑んだときのレベルは完全に事故。最初はねえ、途中で投げた妹二号の参考になっかなーと思ってやってたけど、途中からの強行軍と変態戦術は何の参考にもならないなこりゃ。

ちなみに最大の誤算はその妹が「テラモエスwwwwww」とか書いたメールを寄越しくさってきた事で、お前それはちょっとヤメてくれ。俺のロールプレイの主役級は基本的に俺が書きやすい口調で書いてるので、そのキャラで掛け算を押っ始めるというのは、つまり、その。

というわけで今からセブンスドラゴン始めます。

2009-03-08
Sun

(00:53)

というわけでセブンスドラゴンを始めたのだが、まずは小手調べということで適当にキャラを作って適当に始めたら最初の戦闘で死人がバッチリ出たので、やはりというかなんというかボタン連打でクリアできるゲームじゃないねこれは。これはマゾゲーマーな傾向のある俺にとっては歓迎だ。

さてそれで困ったことが一つ。このゲームでもロールプレイ件プレイ記録はやるつもりだけど、何ていうか今のところゲームの区切り感が見えねえ。個々のクエスト単位だと細かすぎるし、それ以上の流れは見えてないしなあ。ダンジョンRPGはその点「ダンジョンAをクリア」「X階層までクリア」で区切れるから、その後のまとめが楽なんだよな。一見自由さのかけらもない息苦しい升目区切りのダンジョンが、実は思わぬ利便性を持っているという。まあ、その辺は適当にやってみるか。

あとセブンスドラゴンって公式でファンサイトキットが配布されてるから、世界樹の時みたいに公式の画像をトリミングしてアイコンを作るとかやらなくて済みそう。これはとても有難い。

(17:17)

昨日の強行軍で疲れたせいか、起きたら昼過ぎだった。そっから飯食って家ん中片付けたりしてたんで、結局セブンスドラゴンはそこまで進められたない。現状では最初のボスを倒して、次のミッションが発動されたところ。ひとまずファーストインプレッションを書くと、大体こんな感じ。

エンカウントが多い。ヒーラーにエンカウント低下スキルがあるんで、それ使おうかな
レベルを1上げるのにスキルポイントが2必要なスキルとかある。強スキルの予感
実はそんなに難易度的にはシビアじゃなさげ。もう一つぐらいレベル下げても最初のボスは倒せたかも
攻撃力/防御力と魔法攻撃力/魔法防御力がそれぞれPOWとINTで算出されるのは、直感的と言えば直感的
- でもナイトあたりはどうすんだろ（殴れるナイトか紙防御のナイトになりそう）。中盤以降は攻撃力はマスタリーでの補正が大きいとかそういうバランスになってくのかな
スキル振り分けによるパラメータいじりはやっぱり楽しい。ただ、世界樹みたいに手軽に休養して振り直しとかできなさげ
クエストの段取りが面倒。「依頼人を探す」「オフィスで仕事を受ける」「クエストを完了」「依頼人に報告」「オフィスで報告して報酬ゲット」というのは面倒過ぎるだろう。この点、酒場で全部完結してた世界樹とか依頼人と直に交渉してたエルミナージュは良かった

とりあえず最初のボスを叩き潰した後の面子はこんな感じ。俺はあんまりギルドの人数を増やしたくないクチなんで、最後までこの面子で行く予定。ちなみにギルド名は「Endtyme」で、これは Cathdral のアルバムから取った。キャラクターの名前も当然メタル系だが、今回は少しマニアック過ぎたかも（エルミナージュの時よりひどい）。

- スキルはPOWを伸ばしぎみにして、ヴァンパイアを取得。後述のランヒルドと組み合わせて戦わせる予定
- ソードトラップでトラップリアクト発動とかリプレイスファーストから全体魔法で雑魚殲滅とか、夢が広がりまくり
- 名前の元ネタは某有名ドゥームメタルバンドのギタリストから
- 開発者が「レアドロップはイベントで取れ」と言っていたが、ドロップアイテムがメイン資金稼ぎ手段なので鑑定学に全振り
- 攻撃手段はとりあえず火属性を伸ばしてみた。三属性を伸ばすのは無理だろうから、火属性が通用しない時にどうするか考え中。いっそ無色呪文を伸ばすべきか
- 名前の元ネタは、某有名ゴシックメタルバンドのアルバムクレジットをよく読めばわかるかもしれない。わかったら凄いよ
- 序盤なんで、回復はキュアがレベル1もあれば充分。まずはなるたけ早くリザレクションを覚えさせようか
- 後衛にいる限りは殴る必要がないんでPOWは伸ばしてないけど、いっそPOWを伸ばすべきか。ステータス異常が重複するんなら、毒攻撃を覚えさせてもいいんだが。
- 名前の元ネタは某ゴシック寄りメロディックデスメタルバンドのキーボーディストから
- 何も考えずに落葉金切りを覚えさせたらスキルポイントが足りなくなった。このまま落葉金切りを伸ばして出血地獄の夢を見てもいいですか
- プリンセスリアクトが「他のメンバーのリアクトに合わせて発動」とか恐ろしい事になってるので、ソードトラップからのリアクトに合わせて手数でゴリ押しとか、デッドマンリアクトから回復呪文を使うとか、やべー夢が広がりすぎる
- 名前の元ネタは某ドローンアンビエントユニットとか某スラッジバンドのヴォーカリストから。わかった人は人間としてどうかと思う

というわけで暫く進めてみて、作れそうだったらセブンスドラゴンも世界樹の時みたいなページを作る予定。だけど、ちょっとこれは難しいというか面倒そうだなー。

(19:49)

……なんじゃこりゃああああああああああああああああ!?

と叫びたくなるような驚愕の展開がセブンスドラゴンに待っていた。これはあれだ、ネタバレとかまずできんな。いや少年漫画的に燃える展開なんでアリなんだけどさ。

ってか脳内設定とおもくそ矛盾してるんだけど、一体どうすんだこれ。

(22:44)

とりあえずセブンスドラゴンのコンテンツを作ろうと思ったら、必要な画面写真を撮り忘れた事に気がついてちょっと最初からやり直しに。いや普通はそんなことやらないけど、あんまり進めてなかったからまあいいか。

コンテンツのデザインというかフォーマットは既にできてるというか、この手のコンテンツを作るためのフレームワークのようなものを作ってあるので、材料が揃っていい感じに電波を受信できたら即刻作成可能になってる。

問題はどこまでネタばらしするかだけど、世界樹IIの時もネタバレ全開だったからまあ気にしない方向で行くか。

2009-03-09
Mon

(20:53)

仕事で目にするクソのようなソースコードについて、最近本気で権利が欲しいと思うようになってきた。もちろん個人や組織を特定できるような情報は削除した上でだけど、それを全部インターネット上で公開したい。とにかく、システム開発の現場では様々な理由によりクソのようなコードが生産されるのだ。

初心者がいきなりフレームワーク開発チームに投入される
納期不足により一筆書きしたコードを納品
腐敗したコードを忙殺されてるリーダークラスがレビューできずに素通し
フレームワークが極めてパンキッシュな作りでその上のアプリケーションのコードが極左的アナーキズム状態
上流工程の担当者が何かをキメていたとしか思えない設計書を作成
開発規約・標準がデスクリムゾンの取扱説明書みたいになっていて理解不能
プロマネがアレだったりして命令系統が旧日本軍と大差ない惨状
クライアント企業で応仁の乱が起こってプロジェクトが頓挫、半端なコードを形の上でも納品、しばらくして再開したときに阿鼻叫喚の地獄絵図

ちなみにこれら全部を実際に目にしたことがある、というか一つのプロジェクトで同時多発的に起こったのが多い。

それはともかく、人間が成長する一番の方法は派手に失敗してから深刻に反省することで、次にいい方法は他人の失敗から学ぶことだ。その意味で、クソのよなコードを反面教師として共有することには意味があると思うんだが。

2009-03-10
Tue

(23:21)

そういや今週は社員旅行があるんだった。面倒くせえなあ。今となってはサボりたくて仕方がないが、でも旅行の行き先を経営してんのが最近入った後輩の両親で、流石にこのネタを逃すのもなあ。

ちなみにセブンスドラゴンプレイ記録は執筆が難航中。なんかNPCの台詞がやたら多かったりして、撮影した画面写真の数が1話あたり100枚越えそう。

2009-03-11
Wed

(19:40)

「内作フレームワークが持つリスクを考慮すべきですよ＞某大手 SIer さん」がまったく他人事に思えない今日この頃。それでなんでそんな情けないことになってるかというと、ドキュメンテーション含めたメンテナンスの要員がきちんと確保されていないのがよくあるパターン。実例を一個挙げると、

元請けがフレームワークを作り始めるが明らかにパワー不足
アプリ開発の丸投げ先である下請けがなし崩し的に開発に関わる
いつの間にやら元請けがフェードアウトをし始める
本来の設計者と現行の設計者の設計思想の妥協点が見つからないうちに元請けが完全にフェードアウト
下請けは要員的にギリギリなのでドキュメンテーションや周辺ツールに手が回らなくなる
契約の関係上そのフレームワークを使い続ける事になっているが、メンテナンスできる人間は極わずか

とか。まあ別にメンテナンスの問題は内作フレームワークに限った話じゃなくて、フリーソフトウェアのフレームワークでもダメな奴はダメだからな。ただそれでも実績のあるフリーソフトウェアのフレームワークを使わずに自分たちで開発するというのなら、それ相応のメンテナンス要員は確保しないとな。

あと極稀にフレームワーク開発者がマジもんの大戯け者で会社の方針とかと全然別の次元でメンテナンスが不可能という強烈なケースがあるけど、これは今のところ一回しか経験してない。ピンハネ産業や自称・上流工程ばっかやってる会社が何かの電波を受信して自社製フレームワークで下請けをロックオンとかやろうとしたんじゃねえかとか、そういう会社に間違って入った技術オタクが鬱憤晴らすのに作ったんじゃねえかとか、本当に開発者が何かキメてたんじゃねえかとか、いろいろ思うところがあるけど真相は闇の中。

(23:06)

たまーにこういうどうしようもない物が食べたくなるんだよな。

それでセブンスドラゴンのプレイ記録だけど、できれば今週中に最序盤の分をアップしたいところ。世界樹の時もそうだけど、書いてるうちに筆が滑りまくって収集が付かなくなりそう。

どうでもいいけど今回の目標：第1話で街から出る

2009-03-12
Thu

(20:30)

電車の中吊り広告で見た実写映画番ドラゴンボールへの原作者コメントがあまりにもフリーダムだった。「原作者としては『え?』って感じ」「別次元の『新ドラゴンボール』として鑑賞するのが正解かもしれません」というのを堂々と書いてるのは凄いな。

そして俺は別次元のドラゴンボールなぞまったくもって見たくないので、多分これは頼まれても見ない。

2009-03-13
Fri

(01:27)

セブンスドラゴンのプレイ記録を公開。世界樹のときみたいなサブタイトルが思いつかなったりとか、章立てに再考の余地があるとか、気になるところだらけだけどひとまず晒しとく。

今回は第1話でちゃんと街の外にでてモンスターと戦闘したり、クエストをこなしたりできたのが快挙といえばそうだ。世界樹はねえ、初代もIIもギルド結成しただけで第1話終了とか本当に俺は何をやってたんだろう。もっともその分今回は1話1話の容量がでかくなってるというか、プレーンテキストで既に42K書いてるとかますます内容がアレになってるとか、なんかもう開き直るしかないわけよ。

そういやこのゲーム、開発者は「クリアタイムは普通にやって30時間」と見積もってるけど、俺は今プレイ時間が5時間で文章書くのに同じぐらいの時間がかかってるから、まあ寄り道含めて完結するまで100時間コースといったところでしょうか。コストパフォーマンス的には大変優れていると言えるか。

(20:01)

調査のためにソースコードを貰う→必要な物が抜けまくっていて全然ビルドできない
全部入りのソースコードを要求する→やっぱりまだ全然ビルドできない
いい加減にしろ、第一ドキュメントもまだ揃ってないんだ、とっとと全部くれと要求→渋られる
粘り強くそれらがないと作業できないと説明→やはりビルドできないコードと抜けのあるドキュメントがくる

何だこの会社。

(20:57)

私信：シグマハーモニクスは地雷と聞いたぞ。

2009-03-14
Sat

(07:29)

というわけで社員旅行に行ってくる。それで未だに殆ど準備してねーとか、今初めて旅行日程見たとか、酔い止め買い忘れたとか、なんかもういろいろダメダメだけど、まあいいやどうにかなんだろ。

2009-03-15
Sun

(17:57)

社員旅行から帰ってきたわけだが、いやはや酷い旅行だった。何が酷かったって、初日に偕楽園というところに行ってきたんだけど、ちょうどその時間にえらいこと雨が降っていて、まったく楽しめなかったというか体力を消耗しただけだった。だったら2日目の願成寺白水阿弥陀堂を先にして、偕楽園を2日目にすればよかったような。何しろ2日目はムカつくほど晴れたからな。

その白水阿弥陀堂は後輩のご両親が管理してるところなんだが、なんと国宝に指定されているところだった。こっちは単にお参りってか親父さんの薀蓄話を聞いて終わりだったから、天候とか関係なかったんだけどな。

旅館に着いてからはDSを持ってきた面子を集めてマリオカート大会とかやってた。流石に8人同時対戦とかやると一撃で順位がトップからケツに落ちる無茶苦茶なカオスで、最初はクッパ+タイラントでやってた俺はもう負ける負ける（HVC+ストリームラインに変えてからは割と勝てたけど）。

飯は2日目昼食の寿司を除けば比較的外れで、理由は単に俺の嫌いな無脊椎動物、茄子、椎茸などが大量に出てきたから。まあこれは偏食してる俺が悪いっちゃ悪いが（寿司は魚類だけ食えばいいのであんまり問題無いんだよな）。

2009-03-16
Mon

(22:26)

最近とあるプロジェクトの見積りをやってるんだけど、ファンクションポイントで出てくる係数とかって結局は「経験的にこんぐらい」っていう代物なんだよな。それでも大体の規模感は想像できるから無駄とか無意味とは思わないけど、でも馬鹿正直に適用できるかというと疑問な部分もある。

ちなみにソフトウェアの見積りについては、そのものずばりなタイトルの「ソフトウェア見積り」がいい本に思える。ファンクションポイントの数字に1ヶ所エラッタがあるように思えるけど（難易度の低い内部論理ファイルの係数が低すぎる）、まあその辺はおいとこう。ぶっちゃけその辺の数字は他に資料があるのでどうでもいいっちゃいいし、企業によってはファンクションポイントの数え方が違ってたりするし。

それよかこの本の読みどころってのは、「見積りと計画はまったく別のもの」「プロジェクトが直面する不確定要素を考慮することが、正確な見積りである」といったあたりの「ソフトウェア見積りとは何ぞや」的な部分で、ここは本当に読む価値があると思う。特にプレッシャーによって不当に狭い幅の見積りを出してしまうといったあたりの記述にはまさにその通りと言わざるを得ない。

そういや「アクティビティの見落とし」とか「過小見積り」で盛大に炎上して、終いにゃメンヘラを数人排出して大変な騒ぎになったプロジェクトにいたんだよな、俺。そのプロジェクトでは極度な締め付け管理などでプレッシャーを与えた結果、それが不当に幅の狭い見積りや過小見積りに繋がっていて、結局それは改善されずに俺はプロジェクトを離れたんだっけ。

ところで「不当に幅の狭い見積り」「過小見積り」の原因はプレッシャーだと書いたけど、実際には楽観的過ぎる見積りでもこれらは起こるし、それらのケースは充分過ぎるほど多い。楽観的な考えと過酷なプレッシャーによる抑圧が同じ結果を生むというのは面白いというか、俺はハードコアな楽観論者は実は何かしらのプレッシャーを感じていたり、物凄いコンプレックスを抱えていて、心の奥底では大変な抑圧状態にあるんじゃないかと常々疑っている。

(23:24)

というわけで本業の方の修行もしないといけないんで、ちょっとセブンスドラゴンの進み方が遅くなってるなー。なのでセブンスドラゴンプレイ記録の進行もスローダウン。一応竹林まで進めていてレベルは17ぐらいなんで、その1つ前のイベントまでが次回の更新内容になるかな。

あ、プレイ記録への感想メールはちゃんと読んでるので、返信がなくてもお気になさらずに。

2009-03-17
Tue

(21:27)

ここ数日の仕事があまりにもかったるくて、ついつい居眠りしそうになる。やってる事は単純で、既存の設計書からモジュールと機能の一覧と CRUD を割り出し、それを元にファンクションポイントを計算するというものなのだけど、提供されている資料が若干錯乱しているのがアレだ。

例えばモジュール一覧に定義されているモジュールの設計書がなかったり、そもそも実装すら提供されているソースコードの中に見つからなかったりとかが普通にある。そもそもソースコード自体がコンパイル不能なので、何が悪いのかさっぱりわからない。大まかな見積りだけならそれでもできるけど、相手の会社はやる気あんのかな。

2009-03-18
Wed

(00:18)

「今日のウンコ」とかいうタイトルのspamを受け取って、「スカトロのお誘いか。勘弁してくれ」とか思っていたら、実はそれは「今日のワンコ」というタイトルだった。獣姦も勘弁だな。

※当然、中身は読んでない。

(20:41)

クソのようなというかクソその物な作業が一段落した。改めて俺は単純作業の繰り返しが嫌いなんだと痛感。

2009-03-20
Fri

(00:46)

檜山さんのセミナー（第三回）に行ってきた。今回は内容的に俺がまとめを書けるレベルじゃねえと思っていたら、他の参加者から「また徹夜してまとめ書くんでしょ」と言われてもう後に引けない状況。

というわけで風呂入って一休みしたら執筆開始。

(01:24)

追記：檜山さんによる添削・補足・解説記事が公開されているので、そちらも参照してください。

さっき檜山さんから参加者に送られたメールに「論理学の教科書を見たらカリー/ハワード対応に到達するまで普通は半年から一年かかるらしい」とか書いてあって、それを150分のセミナーでやるとかどんだけロックなんだよと思った。こんな時間からまとめを書こうとする俺も大概だが、まあいいや。執筆開始。内容がかなりの圧縮版だった事もあったので、俺の方で端折ったり調べたことを追加したり説明の順序を入れ替えたりしているので、そこら辺は注意。

今回のセミナーはまず算術回路・算術計算図という代物を使った計算過程の視覚化のトレーニングを行い、それを踏まえた命題論理の推論ステップの可視化と、そこから型付きラムダ計算と命題論理の対応関係、つまり今回の本題であるカリー/ハワード対応を導き出した。

まずは算術回路・算術計算図からなのだけど、細かく解説しているとキリがないので、算術回路については思い切って端折って、算術計算図を重点的に使う。理由は算術計算図はテキストエディタだけでも気合で書けるからだ。それでは本題の算術計算図に入る。算術計算図は以下のような定義が使われた。

任意の二引数の関数 f に対して
 
 x    y
--------- [f]
 f(x, y)
 
一引数の関数 g に対して
 
  x
------ [g]
 g(x)
 
定数 a に対して
 
---- [Const]
 a
 
複製
 
   x
-------- [Dup]
 x    x
 
入れ替え
 
 x   y
-------- [Exch]
 y   x

ここに「(+), (*), 5」だけが定義済みの関数・定数であるような系を当てはめて計算を行ってみる。例えばその系に引数として 2 を渡した時の計算例が以下のものになる。

     ---- [Const]
2      5
---------- [+]   ---- [Const]
     7             5
------------------------- [*]
        35

また、算術計算図では計算マクロと計算済み定数が使える。以下は二つの引数をそれぞれ自乗して加算する SQSUM マクロの例である。

以下の計算過程を SQSUM と定義するものとする。
 
   x               y
------- [Dup]   -------- [Dup]
 x   x            y   y
------- [*]     -------- [*]
 x * x            y * y
-------------------------- [+]
  x * x + y * y
 
3  4
----- [SQSUM]
 25

計算済み定数については割愛。大体一緒のノリだ。というかこの時点ですでに1時間使っていて消耗気味なんだよ! こっから先は適宜割愛しまくるし、これで大体雰囲気は掴めたものとして話を続ける。

まず最初の前提として、論理と算術の間には以下のような対応関係がある。

論理	算術
演繹系	算術回路キット
推論	基本演算
証明図	計算図
演繹系の証明図	算術回路キットの計算図
証明可能	計算可能
derived rule	計算のマクロ
公理	最初から使える定数
定理	計算済み定数

なので論理の方でも証明図を算術計算図のように使えるものとし、その使い方は以下のようになる。

 仮定1  仮定2
----------- [推論]
   結論
 
------ [公理の使用]
  公理

また、 And 記号として∧を使うものとし、以下の推論規則が成り立つ。

連言の片側を取り出す：
A∧B
---- [Sel-1]
 A
 
A∧B
---- [Sel-2]
 B
 
二つの流れを合流させ、連言を作り出す：
 A    B
-------- [And]
  A∧B

推論規則とは別に構造規則というものもある。

   A
-------- [Dup]
 A    A
 
 A   B
------- [Exch]
 B   A
 
 A
--- [Id]
 A

これらを利用すると、以下の交換法則が成り立つ。

        A∧B
-------------------- [Dup]
A∧B             A∧B
---- [Sel-2]    ---- [Sel-1]
 B                A
---------------------- [And]
        B∧A

これらを使ってセミナーでは連立方程式を解いてみたりしていて、正直これを書くのはかなりしんどいのだけど、まあ頑張ってみるか。まずは以下の連立方程式を考えてみる。

2x + y = 5
3x - 2y = 4

代入法を使えば y = 5 -2x から x = 2, y = 1 というのが簡単に導けるが、ここでは証明図を使った推論ステップで「2x + y = 5 かつ 3x - 2y = 4 ならば x = 2 かつ y = 1」という結論を導いてみる。

               2x + y = 5 ∧ 3x - 2y = 4
------------------------------------------------------[ Dup]
2x + y = 5 ∧ 3x - 2y = 4             2x + y = 5 ∧ 3x - 2y = 4
-------------------------- [Sel-1]   --------------------------- [Sel-2]
2x + y = 5                                 3x - 2y = 4
------------                                  :
y = 5 - 2x                                    :
--------------------- [Dup]                   :
y = 5 - 2x        y = 5 - 2x               3x - 2y = 4
    :            ---------------------------------------
    :                   3x - 2(5 - 2x) = 4
    :            -------------------------------
    :                     x = 2
    :            ---------------------- [Dup]
y = 5 - 2x        x = 2          x = 2
-------------------------         :
         y = 1                   x = 2
       ---------------------------------- [And]
                 x = 2 ∧ y = 1

この図を見てドン引きしてる人もいるかもしれないけど、セミナーではマジでこういう図を手書きしてたんだよ!

ところでこの図では「2x + y = 5 かつ 3x - 2y = 4 ならば x = 2 かつ y = 1」の推論ステップを記述しているわけだが、ここで「ならば」に相当する記号「⇒」を導入する。セミナーでは別の記号が使われていたけど、俺の使ってるフォントにはその記号が無いのでご勘弁。

この場合、前述の命題は「2x + y = 5 ∧ 3x - 2y = 4 ⇒ x = 2 ∧ y = 1」と記述でき、この⇒は含意と呼ばれるものだという。この含意を導入できる状態にある場合、先の命題の仮定部分（2x + y = 5 ∧ 3x - 2y = 4）は既に仮定ではないので消し去ってしまい、論理式の中に埋め込んでしまえる。この推論規則を演繹定理（DT）とする。証明図での現れ方は以下のようになる。

 A
------ [何らかの推論]
 B
 
上記が成り立つ場合：
 #1
----
 A
---- [何らかの推論]
 B
---- [DT #1]
 A ⇒ B

ところで連言（∧）には連言から一方の要素を抜き出して連言を消去する推論規則があったが、含意にも消去を行う推論規則がある。これはモダスポネンス（MP）と呼ばれるもので、「P ならば Q である。 P である。よって Q」という推論規則。所謂「ソクラテスは人間だから死ぬ」とかの三段論法の事らしい。

A ⇒ B    A
------------ [MP]
     B

ここまでに出てきた推論規則は「Sel-1」「Sel-2」「And」「DT」「MP」の5つなのだが、これらはそれぞれ以下のように論理記号の導入・消去を行う。

推論規則	役割	ノート
Sel-1	∧-消去1	1番目の選択
Sel-2	∧-消去2	2番目の選択
And	∧-導入	二つの流れの合流
DT	⇒-導入	演繹定理
MP	⇒-消去	モダントポネス

論理記号には当然他にも様々な種類があり、それらに導入・消去を行う推論規則がある。例えば「または（∨）」に対しては多分以下のような推論規則が成り立つはず。

導入：
A   B
------ [Or]
A ∨ B
 
消去：
A ∨ B     A ⇒ C   B ⇒ C
---------------------------
            C

ところでまとめの冒頭で「命題論理」という言葉を使ったけど、命題論理では命題の詳細な中身には関わらずに証明可能性だけを扱う。また、今回のセミナーでは∧と⇒（及びそれ関連の推論規則）に構造規則だけで構成された自然演繹のサブセットを用いた。

……というところが大体前半戦の内容。ここから後半戦だけど体力が無くなってきた。

まずはいくつかの論理式の証明図を書いてみる。いちいちかったるいかもしれないけど、この後で使うんだよな、証明図を。

まずは「A ⇒ A」の証明図。

  A
------- [Id]
  A
 
DT を用いて仮定の部分を論理式に埋め込む：
 #1
-------
  A
------- [Id]
  A
------- [DT #1]
A ⇒ A

続いて (A ∧ B) ⇒ A。

まずは以下の形にする： 
A ∧ B
------- [Sel-1]
  A
 
DT を用いて仮定の部分を論理式に埋め込む：
 #1
------
A ∧ B
------- [Sel-1]
  A
------- [DT #1]
(A ∧ B) ⇒ A

最後に A ⇒ (B ⇒ (A ∧ B))

∧-導入を行う：
A    B
------- [And]
A ∧ B
 
DT で二つの仮定のうち B を埋め込む：
    #1
    ---
A    B
------- [And]
A ∧ B
------- [DT #1]
B ⇒ (A ∧ B)
 
もう一度 DT：
#2  #1
--- ---
A    B
------- [And]
A ∧ B
------- [DT #1]
B ⇒ (A ∧ B)
------- [DT #2]
A ⇒ (B ⇒ (A ∧ B))

さて、上の証明図で DT を行っていく過程を「ラムダ抽象っぽい」と思った人はビンゴ。何がどうビンゴなのかの話のために、今からラムダ計算の話に移る。

これまでのセミナーでは型無しラムダ計算だけをターゲットにしてきたが、今回は型を導入し、またタプルの概念も導入する。タプルについては「任意の二つの型の順序対」というのが普通の定義……かな。とりあえずタプルについての操作を以下に示す。

タプルは (x, y) で表す
(x, y).1 = x
(x, y).2 = y

それじゃあ、先に出した算術計算図でタプルを操作してみようか。ここではタプルを生成する二引数の関数 t だけを定義してある。

    x    y
    ------ [t]
    (x, y)
---------------- [Dup]
(x, y).1  (x, y).2
------------------ [t]
    (x, y)

「おいこれさっきの命題論理で見たぞ」という人はまたしてもビンゴ。ここでのタプルの操作は以下のような推論規則の適用そのものだ。

    A    B
    -------- [And]
    A ∧ B
--------------------- [Dup]
A ∧ B             A ∧ B
------ [Sel-1]  ---------- [Sel-2]
  A                  B
------------------------ [And]
        A ∧ B

続いて型付きラムダ計算。セミナーでは例の絵算に型情報を付与したものを扱っていたけど、まあとりあえずフォーマルなラムダ式でやってみようか。型は(A, B) -> C という事にしておく。

λy:B. λx:A. (f(x, y):C)

もういい加減疲れてきたので一気に核心の所から書くと、命題論理における DT はまさにラムダ抽象の事であり、その一方で MP は関数適用である。個々の命題記号は基本的な型（A とか B な）であり、論理式は型の表現であると言う事。他の部分についても命題論理と計算の世界で対応が見られ、その対応をカリー/ハワード対応という……らしい。

だから例えば (A, B) -> C というプログラムがあった場合、それは即ち A ∧ B ⇒ C の証明に他ならないというのがカリー/ハワード対応の言っていることで、どういうわけかはわからないけど直観的には納得できるように思える。例えば次の証明図を考えてみる。

             A    B 
            -------- [And]
A ∧ B ⇒ C   A ∧ B
-------------------- [MP]
         C

こいつをちょっとばっかり弄くったとして

               A  B
              ------ [t]
(A, B) -> C   (A, B)
--------------------- [関数適用]
          C

対応しているように見えない? 演繹定理の方も似たような感じで、どんどん⇒を導出していく過程ってラムダ抽象を進めていくように見える。それで何でそんな対応が存在するのかはさっぱりわからんのだけど、ここでキーワードとして出てきたのがデカルト閉圏。ただしこれは名前が出ただけで終わってしまったようなものなので、今のところ詳細は不明。

俺が端折ってしまった部分や懇親会で出た話題にもいろいろと面白いものがあったんだけど、もう空が明るくなってきてしまったので一旦寝る事にする。気力が残っていれば他の部分についても書くかもしれんが、多分無理だろ。さすがに仕事帰りにセミナー寄って、そっから4時間半ぶっ続けで執筆というのは無謀過ぎた。

(11:21)

流石に一気に書き上げただけあっていろいろおかしな記述とかがあるなー。ちょくちょく直していくんで、まあその辺もご了承願いたい。

2009-03-21
Sat

(13:35)

Red Bull も相当にケミカルな味わいのジャンクドリンクだったが、もしかしたらこいつはそれを上回るケミカルさ加減かもしれない。俺は比較的こういうジャンクな味わいが好きだったりするんだけど、流石にこれはちょっとキツいかも。

飲みなれれば違うかもしれないけど、そこまでして飲むものじゃねえよな。確かコカコーラも Buzz とかいう Red Bull のバッタもんを販売して、それが物凄い短命で終わってたけど、 ROCKSTAR★R も同じ運命をたどりそうな気がしなくもない。

2009-03-22
Sun

(15:28)

ここ最近更新の停滞していたセブンスドラゴンプレイ記録を一気に更新。世界樹と違って区切り感がやや曖昧だから、一通りプレイしてから清書しないとちゃんとした構成にし辛い。しかし今回は明らかにキャラの台詞を多くしすぎたなー。世界樹I/II両方の反省点として主役級のキャラだけが延々喋ってるというのがあったんで、今回はそれを是正しようと思ったら、全員の台詞量が底上げされてしまって、何かもう平均で一話あたり10KBとか書いてるんだけど。

あとキャラクターがどんどん変な性格になってきてるけど、これは完全に計算外。最初考えてた戦略とは違ったブチ切れ戦略で戦っているうちに、それに合わせてキャラクターの脳内設定にも補正が入っていって、その結果としてはああいうことになっちまった。

2009-03-23
Mon

(19:51)

今朝はやたら風が強くて、総武線がやたら遅れまくってた。各駅停車で次の駅まで 50 分かかるとか勘弁して欲しいけど、総武線だからなあ。

2009-03-24
Tue

(20:21)

ここに来てソースコード（超絶スパゲティ）と設計書が食い違いまくりという事が判明。えーと、俺はもう逃げていいかな?

それはともかく、セブンスドラゴンの方はフリーシナリオ編にまでは進んでるんだけど、ちょっとレベルが低過ぎるのか苦戦気味だ。フリーシナリオになる前のボスを撃破したときは全員レベル30だったんだけど、それってもしかして推奨レベルよりも低かったりするのか。

2009-03-25
Wed

(21:15)

疲れた。何に疲れたって、仕事があまりにも退屈で疲れた。「新聞読んでマインスイーパやって帰るだけのおっさん」とかの話をたまに目にするけど、俺にはその生活は絶対に無理で、最近の仕事の退屈さ加減はだんだんそのレベルに達しつつある。人間は過労によって死ぬことあるけど、退屈に殺されることもあるんだよ。

2009-03-28
Sat

(18:04)

二日連続で日記を書かなかったのは仕事の不毛さに完全にやる気デストラクションになっていたせいなのだが、いつまでも不貞腐れているわけにも行かないのでセブンスドラゴンプレイ記録を更新してみる。とりあえず今回はフリーシナリオに突入するところまで。

今回はプレイ動画を撮ってみたけど、ちょっとこれは撮影環境をどうにかしないとダメだ。フレイムイーター戦は自軍のステータスがよく見えなかったので、そこは暗算しながらプレイしてた。操作にもたついたりちょっと意味不明な行動があるのはそのせい。

しかしみんなどれぐらいのレベルで進行してるんだろ。えらいこと苦労してダンジョンを突破してるんだが。もっとも俺の編成は雑魚に弱い代わりに強敵相手にレベル格差無視で戦えるので、相対的にドラゴン相手には苦労していなかったりするんだけどな。