言語ゲーム

とあるエンジニアが嘘ばかり書く日記

Twitter: @propella

チクタクで作ったロケット着陸ゲームから微分方程式を求める方法

今 The Haskell School of Expression isbn:0521644089 を読んでいます。これは Haskell でマルチメディアを扱うという、どんな読者を対象にしているのか疑問が残る偏った本なんだけど、未来の eToys の為に新しいネタを探している僕にぴったりのヒントが沢山書かれています。特に10章の『誘導による証明』(?) と13章の『単純なアニメーション』は組み合わせたら全く eToys の為にあるようなテーマです。

僕は前々から、アランさんのデモの中の、ちょっとづつ加速度を足していってはい、これで微分方程式を子供が扱えるようになりますというやり方には、全然違うやん!と疑問を覚えていたのですが、じゃあどうすりゃいいのか分からなかった。だけど SOE の 10章にあるプログラミングを使った方法を使えば、ある二つの関数が同じかどうかが項の置き換えだけで証明できる。

例えば eToys であるリンゴ落下の例題。リンゴが落下する時のチクタクを使った動きは、前の座標から次の座標を加速度の分だけ次々と足して行くという物。それに対して、微積分で習うやり方は時刻 t についての二次方程式を使うやり方。チクタクの方法から二次方程式の方法に、機械的なタイルの置き換えだけで書き換える事が出来たら、その二つの方法は同じ意味だと証明出来る。証明できたら、加速度がどんどん大きくなるという直感的な表現と、時刻に対する関数だという宣言的な表現を自由に往復できるようになる。

こんな都合よく行くかわからんけど、またすぐ忘れないように一応ここに書いておきます。