型推論において、推論結果が妥当であることってどうやって証明するんだろう。そんなのウェブを調べれば乗ってるんだろうけどさ。っていうか推論規則に則って推論していけばその結果は妥当なのか？そんないい加減じゃだめだよね、たぶん。
そもそもである。ある型体型Tの推論規則Rが正しい規則であることを証明しないといけないか。それを証明すれば、Rを適用して推論できた結果って妥当だよな。ほんとか？そういう議論をすることに意味はあるのか？
こういうとき、目が見えれば本を借りてくるなりして調べられるんだけどなあ。ウェブの情報も参考にはなるけれど・・・。型付きラムダ計算についてでも調べれば答えは出るかな。
そういや以前この日記で、「型推論アルゴリズムにはHindley/Milner型と高橋メソッドというのがある」と書いた気がする。その後すぐ、高橋メソッドってのはプレゼンテーション技法の一つだということに気づいたのをすっかり忘れていた。ただ単に俺が見たページは、Hindley/Milner型のアルゴリズムを高橋メソッドで説明しようとした、という筆者のブログだっただけだと思われる。なんだよ。ちぇっ！
ところで、電車の時刻表を作るのって、一種の最適化問題だよな。シンプレックス法でやれるのかどうか知らんが。まあシンプレックス法については「制約条件の下で線型方程式だか線型不等式だかを解く」ってことぐらいしか知らないからよく分かりませんが。っていうか、ちゃんと勉強すりゃよかったな、計画数学。
と、今になっていろいろ後悔してるわけですが。LHAの圧縮にはハフマン符号が使われてるんだっけ、ハミング符号が使われているんだっけ。ああ、そんなことも知らないようじゃ俺もまだまだだな。調べておこう。
ぜんぜん関係ないけれど。マックのグラコロっていつやってたの？なんか今年はもう終わったようですが・・・。知らなかった。食えばよかった。しかもチーズグラコロとかいうのもあるんだって？なんだよそれ。うまそう。