最初に Alloy の事を知ったのは http://d.hatena.ne.jp/keigoi/20090210/p1 を読んで、面白そうだと思った。でも、http://alloy.mit.edu/ のウェブサイトを見てもどこへ行ったら良いのか分からなくて、意味不明すぎて放置していた。しばらくして、同僚が研究で Alloy を使っている事が分かった。これは素晴らしい。というのも、前から私は Coq とか、CafeOBJ とか、論理っぽい事に興味があったんだけど、周りにこういう事を話せる友達がいなかったので寂しい思いをしていたからだ。正直 Alloy の妙にオブジェクト指向風の文法に馴染めなかったけど、同僚に Coq を勧めるより自分で Alloy を勉強する方がはやいと思ってチュートリアルをやる事にした。←いまここ。
ようやく分かった事。Coq と Alloy は一階述語論理を使っているという以外似てない。例えていうと Coq はそろばんで、Alloy は電卓。Coq はコンピュータが勝手に考えてくれるという事は無くて、考えるのは自分。一方 Alloy はある範囲の中で答えや間違いを探してくれる。だけど無限の物は扱えない。
しばらく Alloy のチュートリアルをやっていたけど、滅茶苦茶分かりにくいので本を買う事にした。Coq の時もウェブ上の情報では全然分からなかったし、もしかしてこういうのは本を買うのが正道かも。本が届くまでのんびりする事にする。
本当に私がやりたい事は、スクリプトが書けるアニメーションツールを作るとか、そういうアプリ寄りの事だ。何でここまで寄り道しているのかと自分で悩む事も多い。しかし今まで色々作って思ったのが、例え単純なツールでも背後に一貫性が無いと改良と共にどんどん複雑さが肥大してしまう。
それを避けるために、ツリー型の構造やダグを使ったアクセス、テンプレートなどなど情報整理の方法があるんだけど、どれもこれも目先の問題解決だ。自分が人生の中で生み出す全部のデータを統一された手法で扱えないといけないはずなのに、全然これでは届かない。これって全然大げさな話じゃない、せめて 10 年前に名も知れぬツールで作ったゲームのキャラクターの服の色だけ変えて作り直すような事をさくっとしたいだけだ。
で、もしかして、どこかに究極のザ・整理法みたいな物があるんじゃないか、あるとしたら、そのヒントは証明や形式手法、はたまた良く知らない数学の中にあるに違いないと思ってこういう事をやってるわけです。
