読んだ本の数：8冊読んだページ数：2349ページナイス数：43ナイス黒猫の遊歩あるいは美学講義藝術批評とミステリのミクスチャー。幻想的な恋愛小説でもあるな。読了日：01月07日 著者：森 晶麿ビブリア古書堂の事件手帖―栞子さんと奇妙な客人たち (メディア…

昨年末に[twitter:@h_gyobukyo]と[twitter:@KingKusunoki]から「音出ししたいんだけど、ギター弾いてくれない？」と誘われたので、二つ返事でOKして本日スタジオ入り。で、課題曲として与えられたのが以下。 Falling Star by PINK CLOUD Low and Top by PINK…

読んだ本の数：3冊読んだページ数：860ページナイス数：10ナイス預言者ピッピ(2)続き、出るんでしょうか？読了日：12月02日 著者：地下沢 中也グイン・サーガ・ワールド3 (ハヤカワ文庫JA)えっ、牧野グインは次で最後？もっと読みたいなー。読了日：12月02日…

読んだ本の数：7冊読んだページ数：1938ページナイス数：27ナイス開かせていただき光栄です―DILATED TO MEET YOU― (ハヤカワ・ミステリワールド)18世紀の倫敦を舞台にしたミステリー。登場人物が皆個性的でこの話だけで終らせるのはもったいないなぁ。背景と…

読んだ本の数：11冊読んだページ数：2604ページナイス数：29ナイスちはやふる（14） (Be・Loveコミックス)読了日：10月01日 著者：末次 由紀結晶銀河 (年刊日本ＳＦ傑作選) (創元ＳＦ文庫)どれも面白かったが、「皆勤の徒」のヌメヌメしたイメージが素敵。読…

読んだ本の数：10冊読んだページ数：1686ページナイス数：32ナイス邪神宮クトゥルフ神話を題材にした異種格闘技戦。読了日：09月04日 著者：岩井志麻子中国嫁日記 一webで読んでたけど、馴初めを描いた書き下ろしが読みたくて購入。出会いって不思議ですね。…

読んだ本の数：7冊読んだページ数：2603ページナイス数：27ナイス異形たちによると世界は…蓮コラが苦手だった私には、「観察者」のラストカットが一番キツかった。しかし延流ちゃんにまで「ババひいたー」とか言われちゃうニャル様って…。読了日：08月01日 …

読んだ本の数：5冊読んだページ数：1672ページナイス数：17ナイスベッドルームで群論を――数学的思考の愉しみ方身近のちょっとした話題を数学的に考えてみると…というエッセイ12篇。最後の章で紹介されていた器械時計は凄いね。400年に一度しか動かない仕掛け…

次いつやるかわからないし、多分また忘れてるだろうから忘備録として書いておこう。引っかかったのは次の二点。水を止めなくちゃいけないわけだが、野晒しになっている止水栓の蓋が固くて開かない。砂が噛んでたりするのかと洗い流したりしてみたが、ダメ。…

読んだ本の数：8冊読んだページ数：2849ページオスカー・ワオの短く凄まじい人生 (新潮クレスト・ブックス)何処までが現実で何処からが虚構なのか。オタク青年とその一族の人生を通して、ドミニカの暗黒時代を描いた作品。読了日：06月05日 著者：ジュノ デ…

読んだ本の数：11冊読んだページ数：3636ページ華竜の宮 (ハヤカワＳＦシリーズ Ｊコレクション)魚舟ってパーンの竜と並ぶぐらいのパートナーにしたい生物だと思うが、どうよ？ ツキソメと彼女に関する情報がどうなったのか、エピローグからは窺い知ることが…

読んだ本の数：12冊読んだページ数：3736ページ数学ガール／乱択アルゴリズム確率論とアルゴリズム論が乱択アルゴリズムへと収斂していく様が素敵。乱択アルゴリズムについては、参考文献を読んでみようかな。読了日：04月03日 著者：結城 浩ヒプノスの回廊―…

子供が所属している吹奏楽部の定期演奏会。毎年、学年度末に一年の〆として開かれ、最高学年生にとっては今までの部活動の集大成であり、これを最後に引退となる演奏会。だが、今回の震災で残念ながら中止となってしまった。しかし、今日、その替わりとして…

読んだ本の数：9冊読んだページ数：2163ページ郭公の盤正統伝奇ホラーと思って読んでたら…。これだから大阪人は信用ならんwww ルカー(ですよね？)には吹いた。読了日：03月02日 著者：牧野 修,田中 啓文図書館戦争LOVE&WAR 7 (花とゆめCOMICS)番外編で小牧に…

読んだ本の数：11冊読んだページ数：2890ページ エステルハージ博士の事件簿 (ストレンジフィクション)ストーリーもだけど文体にも眩惑させられた(^^;読了日：02月05日 著者：アヴラム・デイヴィッドスンテルマエ・ロマエ I (BEAM COMIX)風呂ネタだけでここ…

読んだ本の数：4冊 読んだページ数：818ページちはやふる（10） (Be・Loveコミックス)多くの人に支えられながらも、戦う時は一人。襷を作ってくれた宮内先生に礼をするシーンにちょっとうるっとした。読了日：01月09日 著者：末次 由紀密姫村抗うこと叶わぬ…

キャンペーンやってるってことで。日常的に使うシーンがあるかどうか、現状ではかなり微妙なんだけど物欲だけは無闇に掻立てられるんだよねぇ(^^;;

読んだ本の数：8冊 読んだページ数：1684ページ マジック・キングダムで落ちぶれて (ハヤカワ文庫SF)社会システムがどう変わろうとも、人の浅ましさは変わらない。ウッフィーって仕掛けは自己顕示欲への皮肉かな読了日：12月03日 著者：コリィ・ドクトロウの…

読んだ本の数：5冊 読んだページ数：1538ページ狼と香辛料〈14〉 (電撃文庫)相手の心に踏み込んでいく勇気読了日：11月03日 著者：支倉 凍砂もいちどあなたにあいたいな久々に素子節を堪能した気がする。"卑怯階級"は刺さるなぁ(- -;読了日：11月07日 著者：…

リストに関する証明でもinductionが使えるよという話。まずはリスト中に指定した数がいくつあるかを数えるcountという関数を定義。 Fixpoint count n l := match l with nil => 0 | a::tl => let r := count n tl in if beq_nat n a then 1 + r else r end.…

ex.1 addの定義は以下。 Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.最初は下記のように書いた。 Lemma ex1' : forall n m, add n (S m) = S (add n m). Proof. induction n. intros m. simpl. reflexivity. rewrite IHn. reflexivi…

4.2 タイトルの"Stronger Statements"ってのはより厳密な命題って感じですかね？命題で使われている関数がいくつかのパターンマッチで定義されている場合は、成立すべき初期段階が複数必要ですよという話でいいのかな。例で使われるのはevenb。定義は以下 Fi…

4章は自然数を扱った証明でよく使われるtacticの紹介。 4.1 まずはinductionというtactic。こいつは数学的帰納法ってやつですね。 sum_nは2章で定義していて、 Fixpoint sum_n n := match n with 0 => 0 | S p => p + sum_n p end.ということで数学的帰納法…

ということでexerciseをやってみた。 ex.1 まずは定石に従い、introsすると 1 subgoal A : Prop B : Prop C : Prop H : A /\ B /\ C ============================ A /\ BHをさらに分割するためにdestructを適用。 1 subgoal A : Prop B : Prop C : Prop H1 …

3.3.2 rewrite 次はrewriteというtactic。 式変形だと思えばよいかな。左辺を式変形して右辺と同形になることを示すというわけ。 まずは分配法則を適用してみる。分配法則を表す定理は何かを探すのにはSearchRewriteというコマンドが使える。 SearchRewrite …

3.3 引き続き、いろんなtacticの例。 演算子/\に対して左辺と右辺に分割を行う場合は、3.2で出てきたように destruct H as [H1 H2]という形でdestuctというtacticを適用したけど、\/に対しては destruct H as [H1 | H1]と分割後の仮定を表すシンボルの間に|…

読んだ本の数：12冊 読んだページ数：2782ページバカとテストと召喚獣 (1) (角川コミックス・エース 256-1)読了日：10月04日 著者：夢唄,まったくモー助バカとテストと召喚獣 (2) (角川コミックス・エース 256-2)読了日：10月04日 著者：夢唄,まったくモー助…

いよいよ本題の定理証明へ。 3.2 Lemma hoge : … で証明すべき式を宣言。hogeは式につけられる名前。証明が完了すれば以後定理としてhogeの名前で参照できるようになる(らしい)。 Propは命題、/\は論理積を表してる。ということで論理積演算で交換律が成り立…

2.1 定数の定義 Definitionで定数定義というかbindですね。関数をbindするには下の略記が使えると。 2.2 条件式 ブール値を扱うにはBoolをImportしておく。 あるデータ型に対してどんな関数が定義されているかは、SearchやSearchAboutで調べられる。 2.3 自…

Checkは定義を表示。 Eval compute in ex でexを評価 という解釈でいいのかな。