2012-12-30

終幕

その他

2012年色々あったので適当にまとめておこうと思う。

1月: twitter再開した記録がある。あと適当にこなした卒研。
2月: 結構頑張った。最近研究してることの種は全部ここで蒔かれたと言ってもいい。
3月: 某つどいをネットで眺める。このへんの記憶はない。
4月: 大学院入学。勉強会やろうぜみたいなことを言い出す。
5月: SICP勉強会とその他怪しげな勉強会開始。同時にこのdailyを始める。
6月: 勉強会と講義に忙殺される。
7月: 区切り。
8月: 小休止。すごいHaskell楽しく学ぼう！本ですごいHな言語をいじいじしてました。
9月: 初旬に某つどいに行って来ました。下旬は院のゼミ。この辺で研究がちょっと進んだ、かも。
10月: ゼミがぽしゃりまくるスランプ。一方勉強会は超楽しくなるしあれでした。この辺からSGL読み始めています。
11月: 某モナドイベントやら某若手の会に行ってきたり。あとはいろいろ言語のお勉強を適当にしたり。
12月: ※後に追記

11〜12月にかけてが一番動きが激しかったかもしれないので、12月を別枠で書きます：

SICP4章に入りました！SchemeでSchemeの処理系を記述するという、一番楽しい部分です。1-3章で勉強してきた事柄が有機的に繋がり、心躍りました。
前々からサブで使ってるPCにUbuntuを入れていたのですが、実験的にFreeBSDを入れました。案外楽しい。
就某活がスタートしました。どうなることやら。
来年3月の某なんとかに向けて準備でいろいろと余裕がありませんでした。
ルービックキューブをマスターしました！！！！←重要

とまあ。
大して何もしていないつまらない人生ですが、アウトプットは大事ですよ。
反省点は…あーあれしておけばよかったな、ってことが結構多いことですね。
これは痛いです。
来年も行動指針とかどうしようかなとか、考えているのですが、それはまた今度で。

それでは、また来年。ご達者で（自分に向けて

2012-11-05

(੭ु´･ω･`)੭ु⁾⁾(੭ु´･ω･`)੭ु⁾⁾

SGL

SGLの4章読んでTopos導入をしている感じなのですが、
generalized elementってなんやねん
という話で、ちょっと思ったことを書く。

Definition:
$\mathcal{E}$ をtopos、 $B$ をその対象とします。
$B$ 一般化元(generalized element)とは射 $b : X \to B$ のこと。

と言われてもなんのこっちゃ。
集合論でいうところの元が元っぽい感じは外延性が成り立っていることに由来しています。
特に、内包公理(正確には分離公理)を適用して得られる集合は集合の外延性によって一意的に定まり、
このことが、 $\{x \in B \mid \varphi(x) \}$ という内包表記を許している所以です。
このことと、一般化元の話が実は対応しています（というのを人から聞いて教わった）。

Definition:
$\mathcal{E}$ とtopos, $S$ を $B$ の部分対象、すなわち、 $m: S \to B$ をmono射とします。このとき、 $B$ の一般化元 $b: X \to B$ が
" $S$ の中にある"(b is "in $S$ ")とは、 $\chi_S \cdot b = \mathrm{true}_X$ を満たすことと定義する。
ただし、 $\chi_S$ はtoposのsubobject classifier $\mathrm{true} : 1 \to \Omega$ から定義される $S$ の $B$ 上の特性写像 $\chi_S: B \to \Omega$ で,
$\mathrm{true}_X$ は射 $\mathrm{true}_X : X \to 1 \to^{\mathrm{true}} \Omega$ のこと。

この時、次の"外延性定理"が成り立ちます：

Theorem(Extensionality):
$\mathcal{E}$ をtopos、 $B$ をその対象、 $S$ と $T$ を $B$ の部分対象とする。この時、次の二条件は同値である：

$\{ b \mid \textit{$b$ is "in $S$"} \} = \{ b \mid \textit{$b$ is "in $T$"}\}$

$\chi_S = \chi_T$

ようは、部分対象の外延たる一般化元を全部集めてきてそれが一致していれば、部分対象を抽出してる特性写像も一致するというわけです。
証明は読者の演習問題とする（手元にはあるけど書く体力はない（可換図式書きたくない））。

というわけで、なんとなくトポスのイメージは湧いてきました。
ただ、まだgeometricなイメージが足りないので修行が必要です。切磋琢磨するですん♫

2012-11-05

(੭ु´･ω･`)੭ु⁾⁾

sicp

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exercise 3.12

(define (last-pair x) (if (null? (cdr x)) x (last-pair (cdr x))))
;; The procedure which changes (a. b. c. .. z) to (z)
(define x (list 'a 'b))
(define y (list 'c 'd))
(define (append x y) (if (null? x) y (cons (car x) (append (cdr x) y))))
(define (append! x y) (begin (set-cdr! (last-pair x) y) x))
(cdr x)
(begin (append! x y) (cdr x))
;; create local environemnt to compute (last-pair x)
;; compare (begin (append x y) x) and (begin (append! x y) x)

;; xがappend!で新しく置き換わるというだけで面白い話ではない

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exercise 3.13

(define (make-cycle x) (set-cdr! (last-pair x) x) x)
(define z (make-cycle (list 'a 'b 'c)))
(begin (display (car z))
       (newline) (display (cadr z))
       (newline) (display (caddr z))
       (newline) (cadddr z))
;; gosh> a b c a
;; i.e. z = the loop (a b c a b c a b c ...)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exercise 3.14

(define (mystery x)
  (define (loop a b)
    (if (null? a) b
	(let ((temp (cdr a))) (set-cdr! a b) (loop temp a))))
  (loop x '()))
(define (v y)
  (define (f x y) (if (= x y) () (cons x (f (+ x 1) y))))
  (f 0 y))
(define w (mystery (v 10))) ;; reverse of list
;; (0 1 2 .. 8 9) -> (9 8 7 .. 1 0)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Exercise 3.18-19

;; 3.18 Find a procedure that determines whether a list contains a cycle

(define (have-cycle? x)
  (define (exists? b xs)
    (cond ((null? xs) #f)
	  ((b (car xs)) #t)
	  (else (exists? b (cdr xs)))))
  (define (exists-self-ref? x ys)
      (if (exists? (lambda (y) (eq? x y)) ys) #t
	  (begin (set! ys (cons x ys)) (exists-self-ref? (cdr x) ys))))
  (exists-self-ref? x ()))

;; 追記. exists? の代わりに memq 使えばもっとすっきりした感じ

(define v (cons 0 ()))
(begin (set-cdr! v v) v) ;; loop (0 0 0 ..)
(define x (cons 0 (cons 1 ())))
(begin (set-cdr! (cdr x) x) (set! x (cons 1 x))) ;; loop (1 0 1 0 1 ..)
(have-cycle? v) ;; true
(have-cycle? x) ;; true
;; ys=(list x) -> (list (cdr x) x) -> (list (cdr (cdr x)) (cdr x) x) -> (list (cdr (cdr (cdr x))) (cdr (cdr x)) (cdr x) x)
;; Then we have True since (eq? (cdr (cdr (cdr x))) (cdr x)) = true.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 3.19 implement 3.18 with constant space

(define (have-cycle1? x)
  (define (count b x)
    (cond ((null? x) 0)
	  ((not (b x)) (count b (cdr x)))
	  ((b x) (+ (count b (cdr x)) 1))))
  (define (exists-self-ref? x y depth)
      (if (>= (count (lambda (y) (eq? x y)) x) 2) #t
	  (exists-self-ref? x (cdr y) (+ depth 1))))
  (exists-self-ref? x x 0))

(have-cycle1? v) ;; true
(have-cycle1? x) ;; true

若干注釈で、コンスタントスペースの解釈を入力xに対して、その計算の領域が|x|の定数倍程度で済むと解釈しました。
おそらく、3.18だとysの領域確保に|x|の2乗程度の領域を使っているので、それを改善しますという文脈の話です。
ここで書いたprocedureだと、successive cdrの結果全部を記憶する代わりに、successive cdrを何回適用したかのみを記憶して領域を節約している感じです。
ただ、計算時間と計算領域は常にトレードオフの関係にあるので、これが真に改善になっているかは何とも言えません。

とまあこんな感じでだらだら。
あとはつまんない感じだったので、省略します。

2012-10-30

にょん٩(๑❛ᴗ❛๑)۶

その他

SGL読んでるけど、topos考えるときはやはりSetsとの対応を念頭にしながらするとよい、ということがわかりました（小並感）

あと、この本、本当にIntroductionって形容がぴったりで、読みやすいですね。今まで敬遠してたのがバカバカしいです。
簡単なのでみんなどんどん読みましょう。（研究からの逃避）

2012-08-19

うにゃーーーー

Haskell

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

data Alphabet = Empty | EOF | TChar Char deriving (Show, Eq)
type Tape = Int -> Alphabet
type Head = Int
data Control = NotMove | LeftMove | RightMove | Write {write :: Alphabet} deriving (Show, Eq)
data State = Initial | Halt | FreeState {num :: Int} deriving (Show, Eq)
type MutState = (Head, State)

type TransFunc = State -> Alphabet -> (Control, State)

data TM = TM {stNum :: Int,
              tape :: Tape,
              state :: MutState,
              transFunc :: TransFunc}

readHead :: TM -> Alphabet
readHead m = let t = tape m
                 h = fst $ state m
             in  t $ h

nextTape :: TM -> Tape
nextTape m = let st = snd $ state m
                 h = fst $ state m
                 tp = tape m
                 a = readHead m
                 tr = transFunc m
                 c = fst $ tr st a
             in  case c of NotMove -> tp
                           LeftMove -> tp
                           RightMove -> tp
                           _ -> (\n -> if n == h then (write c) else tp $ n)

nextState :: TM -> MutState
nextState m = let st = snd $ state m
                  a = readHead m
                  tr = transFunc m
                  c = fst $ tr st a
                  nextst = snd $ tr st a
                  h = fst $ state m
              in  case c of LeftMove -> (h-1, nextst)
                            RightMove -> (h+1, nextst)
                            _ -> (h, nextst)

moveTM :: TM -> TM
moveTM m = let nextStN = stNum m
               nextT = nextTape m
               nextS = nextState m
               nextTF = transFunc m
           in  TM {stNum = nextStN,
                   tape = nextT,
                   state = nextS,
                   transFunc = nextTF}

applyWhile :: (a -> Bool) -> (a -> a) -> a -> a
applyWhile b f x = if b x == False then x else applyWhile b f (f $ x)

runTM :: TM -> (Tape, Head)
runTM m = let lastm = applyWhile (\tm -> (snd $ state tm) /= Halt) moveTM $ m
          in  (tape lastm, fst $ state lastm)

showTape :: Tape -> [Alphabet]
showTape t = takeWhile (\a -> a /= EOF) $ map t [0..]

newTapeWithln :: Int -> Tape
newTapeWithln l = \n -> if n == l then EOF else Empty

使用出来るアルファベットAlphabetは空記号Empty,EOF,とChar型のものに限ることとしています。
テープは両側に無限に伸びるテープの表現として型Int->Alphabetを使います。
命令Controlは不動、左移動、右移動、テープへの書込からなります。
状態Stateは始状態Initial, 終状態Halt, あと自由に使える状態からなります。
このもとで、Turing Machine は状態集合、テープ、headの位置を持った状態、遷移関数の四つ組からなるものとして定義します。
ここで、遷移関数の型はState->Alphabet->(Control, State)であり、現在の状態とheadの読むテープのアルファベットを引数として、命令と遷移後の状態の組を返すものです。

まああとは自明でしょう。
普通はEOFなんて記号は使わないのですが今回はテープの表示の便宜上導入しました。
最後のnewTapeWithln関数は引数lに対してl番目にEOFを書き込んだだけの空テープです。

試しに、EOFが出現するまで空テープに'a'を書き込むsampleTM1と、2進数の1bit-shiftをするsampleTM2を書いておきます。

{- The Turing Machine which prints 'a's until EOF appears -}
sampleTM1 = let sampleStN1 = 1
                sampleT1 = newTapeWithln 5 -- represents [Empty, Empty, Empty, Empty, Empty, EOF]
                sampleS1 = (0, Initial)
                sampleTF1 st a = case (st,a) of (Initial, _) -> (NotMove, FreeState 0)
                                                (FreeState 0, TChar 'a') -> (RightMove, FreeState 0)
                                                (FreeState 0, EOF) -> (NotMove, Halt)
                                                (FreeState 0, _) -> (Write (TChar 'a'), FreeState 0)
                                                (_,_) -> (NotMove, Halt)
            in  TM {stNum = sampleStN1,
                    tape = sampleT1,
                    state = sampleS1,
                    transFunc = sampleTF1}

{- The Turing Machine which shifts a binary sequence(i.e., this corresponds to numeric Double-procedure) -}
sampleTM2 = let sampleStN2 = 6
                sampleT2 = \n -> case n of 0 -> TChar '0'
                                           1 -> TChar '1'
                                           2 -> TChar '0'
                                           3 -> TChar '1'
                                           _ -> newTapeWithln 4 $ n
                {- sampleT2 represents [0,1,0,1, EOF] -}
                sampleS2 = (0, Initial)
                sampleTF2 st a = case (st,a) of (Initial, _) -> (NotMove, FreeState 0)
                                                (FreeState 0, TChar '0') -> (Write (TChar '0'), FreeState 1)
                                                (FreeState 0, TChar '1') -> (Write (TChar '0'), FreeState 2)
                                                (FreeState 1, _) -> (RightMove, FreeState 3)
                                                (FreeState 2, _) -> (RightMove, FreeState 4)
                                                (FreeState 3, TChar '0') -> (Write (TChar '0'), FreeState 1)
                                                (FreeState 3, TChar '1') -> (Write (TChar '0'), FreeState 2)
                                                (FreeState 3, EOF) -> (Write (TChar '0'), FreeState 5)
                                                (FreeState 4, TChar '0') -> (Write (TChar '1'), FreeState 1)
                                                (FreeState 4, TChar '1') -> (Write (TChar '1'), FreeState 2)
                                                (FreeState 4, EOF) -> (Write (TChar '1'), FreeState 5)
                                                (FreeState 5, EOF) -> (NotMove, Halt)
                                                (FreeState 5, Empty) -> (Write EOF, FreeState 5)
                                                (FreeState 5, _) -> (RightMove, FreeState 5)
                                                (_, _) -> (NotMove, Halt)
            in TM {stNum = sampleStN2,
                   tape = sampleT2,
                   state = sampleS2,
                   transFunc = sampleTF2}

結果は以下の通り：

*Main> showTape $ fst $ runTM sampleTM1
[TChar 'a',TChar 'a',TChar 'a',TChar 'a',TChar 'a']

*Main> showTape $ fst $ runTM sampleTM2
[TChar '0',TChar '0',TChar '1',TChar '0',TChar '1']