このブログsicp勉強します詐欺になっている可能性ががなにか書かねば！ ということでまずは本日の活動報告：Schemeの処理系ですがGaucheにしました（遅。 一応emacs上で動くようにして、適当にS式の再帰処理とかで遊んで終了〜（それだけ ますますやるやる詐…

進捗報告： Δ-system補題の証明をしました。 cccの位相空間についていくつか説明しました。 時間がなくて演習問題ができなかったのが悔やまれる。 スピーカーの方に負担をかけました。 最近ちょっと疲労がたまってます。。。 気合入れていきますよー。(((o(^…

もう向いてないんじゃないかと思いました………。 現実逃避したい。 うんCoqでClassicalをつかった証明の練習。 ここにあるやつ。 参照： http://coq.inria.fr/library/Coq.Logic.Classical_Prop.html Section Classical_Prop. Require Import Relations_1. Req…

ひとりHandbook読破会を開催中です。 エア参加者募集中(^^) nya~

なにこれ深夜テンションやばいにゃん。

勝手にオーガナイズすることになった他の勉強会の報告もします。 なんやかんやで人数多くて数学科の学生さんと合同でやってます。そもそもこっちのほうが本職なんだが。えー。まあしゅーごー論なのです、はい。 kunenの本を読んでます。 2章のclub集合の解説…

相変わらずCoq書いてるけど進歩ないすなぁ。Coqの特徴ってのはまあ、Inductive型が使えて帰納法ができてハッピーというアレなんだけど、あまりそこに到達していないとこがなんとも。 証明中にやりたくてもできないという知識的欠陥で、Arithmeticの周辺でラ…

このblogについていくつかsrbについて：まずsrbはさらばの意です... 1.[接続詞] それならば 2.[感動詞] 別れの言葉、さようなら.srbの身分： 情報系(笑)のM1です。専攻はヒミツ。 blogの内容： 訳あってSICPを読み始めることになったので、その覚え書きがメ…