erutuf

Require Import List PeanoNat Arith.
Import ListNotations.

Set Implicit Arguments.

Lemma fold_left_map : forall (A B C : Type)(f : A -> B) g l (init:C),
    fold_left g (map f l) init = fold_left (fun x y => g x (f y)) l init.
Proof.
  induction l; simpl; auto.
Qed.

erutuf

今学期受けたMITのCSの授業2

アメリカでは春学期が終わり、私は無事にPhDの一年目を終えました。秋学期の終わりに受けた授業の感想を書いたわけですが、今回も書いてみようと思います。

Cryptography and Cryptoanalysis

暗号理論の授業です。試験はなく、隔週の宿題のみで成績が決まるのですが、今までの人生で受けた授業で一番ハードでした。今学期の私の時間はほとんど暗号に消えていました。ちなみに担当の教員は Shafi Goldwasser と Vinod Vaikuntanathan で、暗号理論では著名な二人です。ちなみにMITの暗号理論の研究者といえば他にもたとえばRonald Rivest(RSA暗号の発明者の一人)がいるなど、大物揃いです。(実は私は授業を受けるようになってからそのことを知ったのですが……。)

授業の内容をざっと並べると、

1. Perfect Secrecy(Shanon Secrecy)
2. Computational Secrecy, One-Way Functions, Hard-Core Predicates

erutuf

Require Import List Arith Ascii String.
Import ListNotations.
Open Scope string_scope.

Inductive prim := PtrIncr | PtrDecr | Incr | Decr | Get.

Inductive stmt :=
| SNil : stmt
| Prim : prim -> stmt -> stmt
| Put : stmt -> stmt

erutuf

今学期受けたMITのCSの授業

私はこの秋にMITのCSのPhDコースに入学しまして、先日期末試験を終えて冬休みに突入しました。MITは(おそらくアメリカの大学院ならMITに限らないと思いますが)本当に日本人が少なく、興味がある人がいても情報を手に入れづらいと思いますので、受けた授業の感想でも書いてみようかなと思います。ただし、私が受けたのは次に示すように数学っぽいものだけだったので興味の違う人には参考にならないかもしれませんが……。

私が今学期受けた授業は、

• 18.404/6.840 Introduction to Theory of Computation
• 6.820 Foundation of Program Analysis

の二つです。二つだけというと少ないように聞こえるかもしれませんが、それぞれ週に2回、90分の授業が行われるので4コマ分です。さらに、こちらでは大学院の授業でも宿題などが多く課されるのが普通ですので、一般的な日本の大学院より授業は大変なんじゃないかなと思います。(もちろん、私も日本の大学院全般を知っているわけではないので同程度に授業がハードな日本の大学院もあるのかもしれません。)

erutuf

import Test.QuickCheck

data BracketStr = BracketStr [Bool] (Maybe (BracketStr, BracketStr))

lenBS :: BracketStr -> Int
lenBS (BracketStr s Nothing) = length s
lenBS (BracketStr s (Just (b1, b2))) = length s + lenBS b1 + lenBS b2 + 2

bs2str :: BracketStr -> String
bs2str (BracketStr s b) =

erutuf

Require Import Program List.
Open Scope list_scope.

Lemma fold_right_ext : forall (A : Type)(f g : A -> A -> A) xs x0,
  (forall x y, f x y = g x y) ->
  fold_right f x0 xs = fold_right g x0 xs.
Proof with simpl in *.
  intros.
  induction xs; [auto|]...
  rewrite H.

erutuf

Require Import Program.
Open Scope list_scope.

Require Import List.

Lemma fold_right_tail : forall (A B: Type) (f: A -> B -> B) xs x b0,
List.fold_right f b0 (xs ++ [x]) = List.fold_right f (f x b0) xs.
Proof with simpl in *.
  intros.
  rewrite <- (rev_involutive (xs ++ [x])).

erutuf

Require Import List.
Import ListNotations.

Set Implicit Arguments.

(* begin hide *)

Definition is_true x := x = true.

Coercion is_true : bool >-> Sortclass.

erutuf

let rec find quot node =
  if quot.(node) = node
  then node
  else
    let repr = find quot quot.(node) in
    quot.(node) <- repr;
    repr

let union quot node1 node2 =

erutuf

Require Import List.
Import ListNotations.

Definition Board := list (list nat).

Definition size (board : Board) := length board.

Definition val (n m : nat)(board : Board) := nth m (nth n board []) 1.

Fixpoint fill' m (l : list nat) : list nat :=