最近 7 日分 / 今月の一覧
2010-03-13 Sat
■ (再)SICP 2.1.3 (問題2.4, 2.5, 2.6) [SICP]
データとは何か。
ヒルベルトのビールジョッキ(λでいうところのα変換?)を思い出した。
「点、直線、それに平面と言うかわりに、いつでもテーブル、椅子、それにビールジョッキというように言い替えることができなくてはならないのだ」
幾何学基礎論 p.207
データは構成されるだけでなく、正しくその要素が取り出せなければならない。
取り出しは別の記法で示されている論理との一致が必要である。
有理数の例)make-rat, numer, denom によって構成されるが、x という整数から n/d が取り出せることと同義であることが示されなければならない。((numer x)/(denom x) = n/d)
これは対(cons, car, cdr)の定義でも例外ではない。
定義(構成)の方法いかんにかかわらず、z が (cons x y) なら (car z) が x で、(cdr z) が y であることが確認できればよい。
言い換えれば、cons や car や cdr でさえも、定義の仕方は様々考えられ、上の条件を満たせば、それはすべて正しいといってよい。
…結局、置き換えモデルで、定義が正しく働くかを調べること…か
本節では cons を、「例えば」
(define (cons x y)
(define (dispatch m)
(cond ((= m 0) x)
((= m 1) y)
(else ("error") m)))
dispatch)
と定義すると、car は (define (car z) (z 0)), cdr は (define (cdr z) (z 1)) と定義でき、
それらが正しく、cons, car ,cdr の条件を満たしていることが示される。
問題2.4 では 上の dispatch とは別途 λm (ただし、m は手続き)を導入して、cons, car, cdr の手続き表現を扱っている。
(define (cons a b) (lambda (m) (m x y))) (define (car z) (z (lambda (p q) p))) 証明 「(car (cons x y)) が x を生じることを証明せよ」 (car (cons x y)) |-> (car (lambda (m) (m x y))) |-> ((lambda (m) (m x y)) (lambda (p q) p)) |-> (lambda (((p q) p) x y)) (|-> ((lambda (q) x) y)) |-> x cdr の定義 (define (cdr z) (z (lambda (p q) q)))
問題2.5 では 対(cons,car,cdr) をなんと積 2^a3^b で表現する。どんな世界が待っているのか? ちなみにこのとき、ヒルベルトの話を思い出した。
問題文の真意をなかなか理解出来なかった。曰く
「a と b の対を積 2^a3^b である整数で表現するなら、非負の整数の対は数と算術記号だけを使って表現できることを示せ」
(define (cons a b)
(* (expt 2 a) (expt 3 b)))
※予備手続き(階乗計算)
(define (expt x y)
(if (= y 1)
x
(* x (expt x (- y 1)))))
(define (car z)
(define (iter z c)
(if (> (remainder z 2) 0)
c
(iter (/ z 2) (+ c 1))))
(iter z 0))
(define (cdr z)
(define (iter z c)
(if (> (remainder z 3) 0)
c
(iter (/ z 3) (+ c 1))))
(iter z 0))
※ car/cdr における iter の意義は、counter(c) をもって、指数を抽出するため。
上の dispatch を参照に。
…こういう世界観もあるんだなぁ。
問題2.6 では、対を離れて、数の定義でも事情が同じであることが示される。チャーチ数と(普段使っている)数の対応を垣間見る。
チャーチ数
; 0
(define zero (lambda (f) (lambda (x) x)))
; +1
(define (add-1 n)
(lambda (f) (lambda (x) (f ((n f) x)))))
; 1
※(add-1 zero) = one から
(add-1 zero)
|-> (add-1 (lambda (f) (lambda (x) x)))
|-> (lambda (f) (lambda (x) (f ((lambda (f) (lambda (x) x)) f) x))) ; f->x
|-> (lambda (f) (lambda (x) (f (lambda (x) x) x))) ; x->x
|-> (lambda (f) (lambda (x) (f (x))))
|-> (lambda (f) (lambda (x) (fx)))
one is "(lambda (f) (lambda (x) (fx)))"
; 2
※(add-1 one) = two から
(add-1 one)
|-> (add-1 (lambda (f) (lambda (x) fx)))
|-> (lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) fx)) f) x))))
|-> (lambda (f) (lambda (x) (f ((lambda (x) fx) x))))
|-> (lambda (f) (lambda (x) (f (fx))))
|-> (lambda (f) (lambda (x) (f(fx))))
+--------------+--+
|λfx.x |0 |
+--------------+--+
|λfx.fx |1 |
+--------------+--+
|λfx.f(fx) |2 |
+--------------+--+
|λfx.f(f(fx) |3 |
+-------------+--+
となっているんだろな。
; +
よって (add 1 2) は (lambda (f) (lambda (x) f(ffx))) のような形になるのだろうな。
(define (add n m)
(lambda (f)
(lambda (x)
((n f) ; ※1
((m f) x)) ; ※2
))) ;※3
※1 (lambda (f) (lambda (x) (fx))) を f に適用して (lambda (x) (fx)) を作り fx の x 部分に加算するものを作る
((lambda (f) (lambda (x) (fx))) f) |-> (lambda (x) (fx))
※2 (((lambda (f) (lambda (x) (ffx))) f) x) |-> ((lambda (x) (ffx)) x) |-> ffx
※3 ((lambda (x) (fx)) ;※1
ffx) ; ※2
|-> ((lambda (x) (fx)) ffx)
|-> f(ffx) ; =3
ちなみにチャーチ数での積(mul)までは考えた。
(mul (λf.λx.ffx) (λf.λx.fffx))
-> λf.λx.(fff(fffx))
になればよいんだろうな。
(define (mul n m)
(lambda (f)
(lambda (x)
((n (m f)) x))))
+-------------------------+-------------------------+-------------+
| n | m | |
+-------------------------+-------------------------+-------------+
|lambda(f)lamda(x)ffx |lambda(f)lambda(x)fffx | |
+-------------------------+-------------------------+-------------+
| |lambda(x)fffx |(m f) |
+-------------------------+-------------------------+-------------+
|lambda(f*)lamda(x)ffx.(lambda(x)fffx)* |(n (m f)) |
+---------------------------------------------------+-------------+
|lambda(x)((lambda(x)(fffx))(lambda(x)(fffx))x) | |
+---------------------------------------------------+-------------+
|(lambda(x)((lambda(x)(fffx))(lambda(x)(fffx))x)x) |((n (m f))x) |
+---------------------------------------------------+-------------+
|(lambda(x*)((lambda(x)(fffx))(lambda(x)(fffx))x)x*)| |
+---------------------------------------------------+-------------+
|(lambda(x)(fffx))(lambda(x*)(fffx))x*) | |
+---------------------------------------------------+-------------+
|(lambda(x*)(fffx))fffx* | |
+---------------------------------------------------+-------------+
|fff(fffx) |Q.E.D |
+---------------------------------------------------+-------------+
参照URL
問題2.6 : λって結局なんなのさー
ラムダ計算入門(pdf)
http://www.csus4.net/hiki/SICPReading/?FujimotoHisa#l79
http://blog.livedoor.jp/dankogai/archives/50458503.html (404NOTFOUND)
http://www.serendip.ws/archives/522 (Serendip さん)
『関数プログラミング教科書』 赤間 世紀 (著) p.39
2010-03-12 Fri
■ Google Apps Script を試す [javascript]
http://d.hatena.ne.jp/shinichitomita/20090612/1244825748
公式のチュートリアル? http://www.google.com/google-d-s/scripts/yourfirstscript.html
を真似てみる
Hellow, World 的なもの
function hellow() {
Browser.msgBox("Hellow, World");
}
入力プロンプト
function hellowWithPrompt() {
var name = Browser.inputBox("Enter your name");
Browser.msgBox("hellow, "+name);
}
カスタム関数(消費税計算)
function shohizei(n) {
return Math.floor(n*1.05);
}
2010-03-10 Wed
■ Erase empty files [commandlinefu]
find . -type f -size 0 -delete もしくは
find . -size 0 -exec rm '{}' \;
find . -size 0 -print0 | xargs -0 rm
http://www.commandlinefu.com/commands/view/3927/erase-empty-files
2010-03-07 Sun
■ サーババックアップ rsync のまとめ的な [rsync][work][maintenance]
[2009-10-31]
ゲートウェイサーバを踏み台にして、ターゲットサーバの 22 番ポートを自分(ローカルホスト)の 33333 ポートにつなぐ。
ssh -fNL 33333:target.server:22 root@gateway.server
コピー元(ターゲットサーバ)もコピー先(ローカルホスト)も、root で実行。
sudo rsync -e "ssh -p 33333" -av --exclude /boot --exclude /root --exclude /proc --exclude /dev --exclude /sys --exclude /media --exclude /floppy --exclude /cdrom root@localhost:/ /mnt
ポート指定の方法に注意。
postgres だけは一度パージしてからじゃないと動かない? (ver8.3 現在)
[2009-11-27] ,(必ず起きるユーザfatal問題への対応は [2008-07-18])