2012年色々あったので適当にまとめておこうと思う。 1月: twitter再開した記録がある。あと適当にこなした卒研。 2月: 結構頑張った。最近研究してることの種は全部ここで蒔かれたと言ってもいい。 3月: 某つどいをネットで眺める。このへんの記憶はない。 4…

SGLの4章読んでTopos導入をしている感じなのですが、 generalized elementってなんやねん という話で、ちょっと思ったことを書く。 Definition: をtopos、をその対象とします。 一般化元(generalized element)とは射のこと。 と言われてもなんのこっちゃ。 …

演習問題淡々と。 3章を読んでいるのですが、ここら辺でSchemeの肝になってる静的スコープと説明と動的なデータをどうやっていじるかの説明が入っている感じです。 今回は3.3章のMutable Data Structureのところを読んでいます。 ;;;;;;;;;;;;;;;;;;;;;;;;;;…

SGL読んでるけど、topos考えるときはやはりSetsとの対応を念頭にしながらするとよい、ということがわかりました（小並感）あと、この本、本当にIntroductionって形容がぴったりで、読みやすいですね。今まで敬遠してたのがバカバカしいです。 簡単なのでみん…

Haskellでなんちゃって Turing Machine 作ろうとしたら謎仕様になったとうという話。 もともと monad 書く練習しようと思って色々データいじっていたんだけど、かなり脱線したので一応書いておきます。 実はこの辺は教科書で勉強したことがなくて、かなり記…

quotationがよくわかりません、という話になりました。実際、proc. (quote )はexpressionをすぐに評価するもので、なんですか、評価はapplicative-orderじゃないんですか！みたいな感じになりました。修行不足なので出直します。

はい、今期はおわり。 お疲れ様です。にゃ

K(S(SI(K(S(K(S(S(KS)K)(S(S(KS)K)I)))(S(S(KS)K)I(S(S(KS)K)(SII(S(S(KS)K)I)))))))(K(S(SI(K(S(K(S(S(KS)K)(SII(S(S(KS)K)I))))(S(S(KS)K)(S(SII)I(S(S(KS)K)I))))))(K(S(SI(K(S(S(KS)K)(S(K(SII(S(S(KS)K)I)))(S(S(KS)K)(S(S(KS)K)(S(SII)I(S(S(KS)K)I)))…

演習問題淡々と。面倒なので、実装しなさいみたいな問題の解答だけ： ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Exercise 2.65 implement the union-set, intersection-set for binary tree data (define (union-set1 tree1 t…

今週はお休みです。 代わりになんか書きます。 SICPも2.3章に入るわけなのですが、ここからシンボリックデータを扱えるようになります。 これを利用して、代数的な操作を実装してみようと思う。 これから上げる例は、１変数多項式の展開形を求めるもの。 た…

Schemeでλ計算とか。 ;; Church-encoding of nat (define zero (lambda (f) (lambda (x) x))) (define (add-1 n) (lambda (f) (lambda (x) (f ((n f) x))))) ;; (add-1 zero) ->* (lambda (f) (lambda (x) (f x))) ;; (add-1 (add-1 zero)) ->* (lambda (f) …

なんか需要あるかと思って、[\square],[\diamondsuit]周りの話でも書こうと思ったけど面倒なのでやめました。 ああ、なんか Approachability とか Good point とか I[lambda] とかそのへんのお話。 I[lambda]の構造を弄る話に関しては Foreman も色々アナウ…

全然進まねえ。

SICP1.3章読みました。 特に何にもないです。 結局procedureって何なのかがわからないまま1章を終えた感じです。 気持ち的には、関数みたいなもので、それがfirst-classになるのは、ありがたい話です。 だめだめnyannyan。

まあ(台風)一過です。 台風で今週の勉強会軒並み中止になっているので書くことありませんが、ちょっといま勉強中の本職のことについて。次の定理の証明を読みました： ZFCで非可算個の可測基数が存在すると仮定する。このとき、において、選択公理の否定が成…

ということになってほしい。

でもまあ考えてみれば、がsupercompactならとかのサイズは(が正則基数なら)丁度になるわけで、べつにココらへんの計算にGCHはいらない。 (Solovayの結果を参照しなさい。あるいは、スパコンのもつ強いstatoinary reflectionによる影響を考えなさい。)てこと…

もくもく。 マーティンの公理を使う練習をしました。 MAD族とマーティンの公理の関係について話しました。 とりあえず、2章はこれでおしまいです。 整礎集合とその階層について説明しました。 3章もこれで終わりで、次は、4章に入ります。 演習問題は[9]と[1…

なんかTLでHaskellでフィボナッチ数列の40項の単純再帰の計算が40秒かかる、とかなんとか話題になっていたので、最近の式の評価戦略のこともあるのでなんか書く。えーと、普通にフィボナッチ数列のn項"fib n"を求める式を書こうとすると、以下のようになると…

勉強不足てのはつらいものです。ああああ、ちょっと昔の記事直しましたはい。SICPですが1回1subsectionのペースで読み進めることにしました。ということで、Section1.1をよみました。 内容は基本的なLisp表現についてです。割と気になった点として、1.1.3-4…

はーい。 報告。 c.c.c.半順序の具体例についていくつか触れました。 コーエン実数を加える強制がc.c.c.の例になっていることを確かめました。 マーティンの公理について説明しました。 ぐらい。演習のほうは誰もやってきてなかったようなので、ぱぱっと自分…

土日で某圏論セミナーに参加してきました。いや、話題が強制法とトポスとか行くしかないではないか！、ということで、名古屋Forcing警察(自称)が駆けつけました。 強制法入門コースでひと暴れしてきました。いやあ、楽しかったです。圏論理解したい＞＜一応…

このブログ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を読み始めることになったので、その覚え書きがメ…