Redundanz

僕の言葉は、人と話をするためにあるんじゃない。

0523

 ホワイトボードを買いました。最近の目標が生活をビジュアライズすることなので、なかなか強力な道具になりそうです。しかし家の壁が妙に硬くって画鋲を受け付けてくれないので、うまく壁にかける方法を考える必要があります。粘着テープ的なものを使うか。

 計算数学を受けに駒場へ。講義が始まる前に加法氏に会って足されてきました。文字上の特殊記号に対応するボディランゲージで定義して括弧付きの言葉を別途説明することなしに明示的に使う方法の話とか生活を最適化する話とか。こだわりの強い人と話すのはやっぱり楽しいですね。

 計算数学。Coqを使ってみました。型概念の理解があやふやなので、型が命題に対応している!と言われてもピンと来ないのですが、とりあえず何かがどうにかなって定理が証明されました。何がどうなっているんだ…
 型を定義したあと関数を定義することでなにかが起こっているようなのですが、関数が定義できたということがどういう風な意味で定理を証明することにつながるのかを把握せねばならないようです。やはり関数型言語を勉強する必要があるぽい。ちょっと興味がわいたのでまた今度いろいろ弄ってみようと思います。すごいH本を買いに行こう。

 夕方からバイト。全く案件がやって来なかったので、将来に備えて複素数平面の勉強をしていました。二時間位でチャートに載っていたパターンは網羅してしまったのですが、全体的にあんまりおもしろくないです。これで難しい問題つくるの難しいんじゃないかな。