λ式のβ変換

この前また妻とふたりで人生ゲームをやった。株を一度に三枚変えるようにしたり、所持金の3桁変動マスは4桁変動にするなどのルールでやってみた。若干ゲームバランスが破綻してしまう感はあるが、スリルがあって面白い。
人生ゲームの攻略法について考察するのも面白そう。すでにやってる人いそうだが。

「計算論」の続き。ここからがλ計算本番という感じ。
λ計算のβ変換とはλ記法であらわされた関数の関数値を求める操作に相当するもの。
定義2.1.2に形式的な定義は書いてあるが、具体的な式で考えた方がわかりやすい。β変換を→で表すことにする。
まずはすごく簡単な例から。
(λx.x)y→y
これが定義2.1.2(1)だ。
問題は(2)の方だ。
M→Nならばλx.M→λx.N。どういうことだ。
(λx.x)y→y
だから例えば
λz.((λx.x)y)→λz.y
ということになる。あたり前な感じか。
次にM→NならばMP→NP。
(λx.x)y→y
だから
(λx.x)yz→yz
ふむふむ。M→NならばPM→PNも同様だ。自然な定義だな。

λ式に対してβ変換を繰り返して具体的な値を得たいのだが、β変換の組み合わせは無数にある。左から変換していってもいいし、右からしていってもいい。最終的な結果は一致するだろうか。
これが2.2節のテーマで、実はChurch-Rosserの定理によってこれは保証されている。有限のβ変換列でそれ以上変換できなくなった場合、そのλ式を正規形という。
すべてのλ式が正規形を持つことは保証されない。また、正規形を持つλ式でも変換の仕方によっては変換が無限に続く場合もある。ただし、この場合もうまく変換すれば正規形にもっていくことができる。
では確実に正規形を得る変換の方法はあるだろうか、という問いには正規化定理が答えてくれる。左から順に変換していけば、正規形を持つ場合は必ず正規形に到達する。
ここまででλ式の基本的な性質は大分わかってきた。
2.3節はとりあえずスルー。

2.4節はλ式なんか考えて何が楽しいのかについて書いてある。
結論を言えば帰納的関数(すなわち計算可能な関数)はλ式によって表現できることが証明される。
計算可能関数の結果を得るためにwhileプログラム(C言語等)を書いて実行してもいいのだが、λ式を書いて実行してもいいわけだ。この場合の計算過程はβ変換そのものだ。コードはλ式、β変換が実行過程。

手続型言語はwhileプログラム、LISPはλ計算を基礎にしていると言えよう。そりゃあ全然違うものになるわな。
 
ジャジャガッチ | LISP | 22:29 | comments(0) | trackbacks(0) |

ラムダ計算

弟に半角/全角キーを含むいくつかのキーが動かないノートpcを1万円で譲ってもらった。
お金を払うのを忘れないようにしなくては。
基本的にはあまり使わないキーが動かないだけなのでそれほど問題はないが、半角/全角キーは困る。
なのでIMEの設定をいじってshift+spaceで切り替え出来るように設定した。Linux風に。これでさしあたっては問題ないな。

「計算論」の続き。
第二章を流し読み。いよいよλ計算。
まずはλ式って何だってところから。
普通、数学では関数を
f(x) = 2x+1
などと表す。引数に具体的な値を入れる場合は
f(2)=2*2+1
などという具合だ。しかし、f(2)=2*2+1という表現では元の関数形がどのような形かという情報が失われている。
そこでλ式というもので表現する。
λx.(2x+1)(2)
λの次に変数を与え、関数形、引数の値の順に書く。
これは1変数関数に対するλ式だが、多変数関数に対しても1変数のλ式で対応できる。
例えばf(x,y)を考える。xを固定してyの関数と考えよう。
λy.fx=λy.f(x,y)
と書ける。次にλy.fxのxを変数と考える。
λx.(λy.fx)=λx.λy.f(x,y)
つまり、「引数はx」、戻り値は「引数yを受け取り結果を返す関数」である。関数を返すことに注意する。これをカリー化というらしい。

で、定義2.1.1に具体的なλ式の定義が書いてある。
λx.Mは関数抽象と呼ばれる。具体的な値になっていない状態だと思う。
MNは関数適用と呼ばれる。代入操作だと思う。

上の例でいえば
λx.(2x+1)
は関数抽象で、
λx.(2x+1)(2)
は関数適用というところか。変数に対してこれらの操作によって得られる式がλ式ということらしい。
λ式の定義がわかったところで一旦中断。
 
ジャジャガッチ | LISP | 21:46 | comments(0) | trackbacks(0) |

計算可能とはどういうことか

少し前に購入した「計算論 計算可能性とラムダ計算」(高橋正子著)の第一章を流し読みした。

計算可能とはどういうことなのか少しずつわかってきた。
内容を簡単にまとめておく。

1.1節ではNプログラムというものが定義される。
これは入力、代入、判定、出力からなる有限の有向グラフであり、よくプログラムを書くときに使われるフローチャートをシンプルにしたようなものだ。
1.2節ではwhileプログラムというものが定義される。これはC言語などの手続き型言語をシンプルにしたもので、input、if〜then〜、do while、outputから成る。
定理1.2.1でNプログラムとwhileプログラムは同等の計算能力を持つことが示される。

1.3節からが本番という感じで、原始帰納的関数というものについて述べられる。
これは初期関数zero()=0、suc(x)=x+1、p_ni(x_1・・・xn)=xiと関数の合成、再帰的定義によって構成される関数だ。
原始帰納的関数はNプログラムで計算可能であることが示される。
しかしNプログラムでは計算可能であるが原始帰納的関数でない例があるため、1.4節で拡張される。
これが帰納的関数で基本は原始帰納的関数であるが、原始的述語の最小解を求める操作が許される。
「Nプログラムによって計算可能な関数」と「帰納的関数」は一致することが示される。

1.5節ではチューリングマシンについて述べられ、これもまたNプログラムの計算能力と一致することが示される。このように種々の計算モデルがあるが、どれも本質的にNプログラムの計算能力を超えない。
より強力な計算モデルは存在しないのであろうと考えられているとのことである。

つまり、実質的に帰納的関数こそが計算可能な関数のすべてであろう、ということだね。
1.6節と1.7節については今のところあまり興味を惹かれないのでスルー。

この本、証明もきっちり書いてあるが読みやすい。証明部分はほとんど飛ばしたけど。面白いのでおすすめ。
 
ジャジャガッチ | LISP | 09:05 | comments(0) | trackbacks(0) |

LISPで連番文字列

一昨日の朝8時ごろに駅を歩いていたらものすごい大声で何やら叫んでいる人たちがいる。
何だろうと思って近づいてみると地元のゆるキャラの応援でした。ゆるキャラグランプリの追い込みらしい。
市役所職員だろうか。
朝っぱらから大変だなあ、と思いつつ、全くゆるさが感じられない応援っぷりに引きました。
流行ってるし、優勝すれば大きなメリットがあるのはわかるんだけど・・・。

さて、LISP。
プログラムを組むときによく必要になるのは連番ファイルの取り扱いだ。少し調べてコードを書いてみた。
文字列の結合にはstring-appendを使うらしい。また、数値を文字列に変換するにはnumber->stringを使う。

(define (f n)
  (define (f-iter n count)
    (cond
      ((< count n) (display (string-append (number->string count) ".bmp")) (f-iter n (+ 1 count)))
    )
  )
  (f-iter n 0)
  )

(f 10)

0.bmp1.bmp2.bmp3.bmp4.bmp5.bmp6.bmp7.bmp8.bmp9.bmp

Script-Fuと組み合わせればフィルダ内の連番ファイルに次々と画像処理を行うことができるな。
ジャジャガッチ | LISP | 06:36 | comments(0) | trackbacks(0) |

Script-Fu

SICPで画像処理を例にとって色々説明している部分があったのがきっかけで色々探していてScript-Fuというものを発見した。
これは有名な画像編集ソフトGIMPのスクリプトで、Schemeがベースになっている。
ちょっといじってみた。ちなみにバージョンは2.8.8。

GIMP自体学生時代に教養の講義で少し触っただけなのでほとんど使い方がわからず、戸惑う部分もあったが、簡単なコードは書けた。
新規画像ファイルを用意し、点を打ち、保存するスクリプト↓

(gimp-context-set-brush "Circle (01)");ブラシの選択
(define image (car (gimp-image-new 256 256 0)));256x256の新規画像
(define layer (car (gimp-layer-new image 256 256 1 "test" 100 0)))
(gimp-drawable-fill layer BACKGROUND-FILL)
(gimp-image-add-layer image layer 0)
(gimp-display-new image)

(define (dot x y) (gimp-pencil (car (gimp-image-active-drawable image)) 2 (vector x y)));2は座標の数 4にして座標を4つにすれば直線が引ける

((lambda (x y) (dot x y)) 128 128)

(file-bmp-save 0 image (car (gimp-image-active-drawable image)) "C:¥¥test¥¥test.bmp" "");ファイルの保存

これをScript-Fuコンソールに入力して実行すればよい(全体をコピペしてenterでOK)。ヘルプ→プロシージャーブラウザで命令一覧が載っているのでこれを適当に参照すれば一応コードは書ける。

GIMPに自作スクリプトとして登録するためには

(define (test u v)
(gimp-context-set-brush "Circle (01)");ブラシの選択
(define image (car (gimp-image-new 256 256 0)));256x256の新規画像
(define layer (car (gimp-layer-new image 256 256 1 "test" 100 0)))
(gimp-drawable-fill layer BACKGROUND-FILL)
(gimp-image-add-layer image layer 0)
(gimp-display-new image)

(define (dot x y) (gimp-pencil (car (gimp-image-active-drawable image)) 2 (vector x y)));2は座標の数 4にして座標を4つにすれば直線が引ける

((lambda (x y) (dot x y)) u v)

(file-bmp-save 0 image (car (gimp-image-active-drawable image)) "C:¥¥test¥¥test.bmp" "");ファイルの保存
)

(script-fu-register
 "test"
 ""
 ""
 "JAJAGACCHI"
 "JAJAGACCHI"
 "November 9, 2013"
 ""
 )

としてscriptsフォルダに入れ、フィルタ→Script-Fu→スクリプト再読み込みして、Script-Fuで呼び出してやればよい。

Script-Fuを使うことでLISPを実用的に使う第一歩を踏み出せたと思う。
ジャジャガッチ | LISP | 06:22 | comments(0) | trackbacks(0) |

SICPメモ(10) 2.3.2記号微分

2.3.2の記号微分が面白そうなのでちょっと読んでみる。次のコードを読み解く。

(define (deriv exp var)
  (cond ((number? exp) 0)
        ((variable? exp)
         (if (same-variable? exp var) 1 0))
        ((sum? exp)
         (make-sum (deriv (addend exp) var)
                   (deriv (augend exp) var)))
        ((product? exp)
         (make-sum
           (make-product (multiplier exp)
                         (deriv (multiplicand exp) var))
           (make-product (deriv (multiplier exp) var)
                         (multiplicand exp))))
        (else
         (error "unknown expression type -- DERIV" exp))))


((number? exp) 0)→式が定数ならば結果は0。(d/dx)const=0だからね。
((variable? exp)
 (if (same-variable? exp var) 1 0))
→式が微分変数に一致しているときは1、そうでないとき0。(d/dx)x=1,(d/dx)y=0ってことだね。
((sum? exp)
 (make-sum (deriv (addend exp) var)
 (deriv (augend exp) var)))
→(addend exp)はexpの二番目の要素を、(augend exp)は三番目の要素を抜き出す。expがsumの形、すなわち(+ u v)の形のとき、uの微分とvの微分を足すってことだね。(d/dx)(u+v)=(d/dx)u+(d/dx)vってことだね。
((product? exp)
 (make-sum
  (make-product (multiplier exp)
   (deriv (multiplicand exp) var))
  (make-product (deriv (multiplier exp) var)
   (multiplicand exp))))
(multiplicand exp)はexpの第三要素を、(multiplier exp)は第二要素を抜き出す。expが積の形(* u v)のとき(d/dx)(uv)=u(d/dx)v+v(d/dx)uになるってことね。

ふむふむ。結構きれいに書けるものだ。
あとはこの手続きで使われているvariable?やらを定義する必要があるがそれはそんなに難しくない。ので省略。
ジャジャガッチ | LISP | 20:29 | comments(0) | trackbacks(0) |

SICPメモ(9) 問題2.17 & 問題2.18

2.2節でlistというものが出てきた。
consでペアを順に繋いだものらしい。

(list 1 2 3 4)
(1 2 3 4)

C言語の配列のように使うには取り扱うための手続きが必要だ。
リストの最後の要素を返す手続きを定義せよ、というのが問題2.17。
要素を取り出すにはcdrを何度か作用させてcarを作用させるのが基本。
例えば(1 2 3 4)で3を取り出したければcdrを2回作用させてcarで取り出せる。
リストが空かどうかはnull?で調べられる。

次のようにしてみた。

(define (last-pair items)
  (define (last-pair-iter item0 item1)
  (cond
    ((null? item1) item0)
    (else (last-pair-iter item1 (cdr item1)))
    )
  )
  (last-pair-iter items (cdr items))
 
  )

(last-pair (list 1 2 3 4 5 6))
(6)

リストが空になるまでcdrを作用させていく。常に作用させる前のリストを保持しておき、空になったとき直前のリストを返せばそれが最後の要素だ。
他の人の解答を見てみるともっと効率のいい方法があるな。面白い。

問題2.18はリストの要素を逆順のリストに変換して出力せよ、というもの。

(define (myreverse items)
  (define (myreverse-iter items r-items)
    (cond
      ((null? items) r-items)
      (else (myreverse-iter (cdr items) (cons (car items) r-items)))
      )
  )
  (myreverse-iter items (list))
  )

(myreverse (list 1 2 3 4))
(4 3 2 1)

SICPだと空の要素をnilであらわしてたけどDrRacketだとnilがないようなので(list)で代用。

すぐに飽きると思ったけど以外に長続きしているSICP。問題がパズルみたいでおもしろい。
ジャジャガッチ | LISP | 21:19 | comments(0) | trackbacks(0) |

SICPメモ(8) 問題2.4

一章後半で待望のλが出てきたわけだが、よくわからんので軽く読んでスルーしていた。
少しずつλが増えてきてよくわからなくなってきたのでちょっとλで遊んでみることにした。

Schemeでいうlambdaって何かというと無名の関数を定義するものらしい。
実はこれまでdefineで関数を定義してきたのは暗にlambdaを呼んでいたらしい。

(define (f x) (* x x))

(define f (lambda (x) (* x x)))
の省略形らしい。無名関数にdifineで名前をつけているわけだ。
次のようにして値を得ることができる。

((lambda (x) (* x x)) 2)
4

2章前半で戸惑ったのは次のような感じの記述。
(define (f x)
  (lambda (m) (m x x))
  )

((f 3) *)
9

ん?関数fの引数はxだけなのにlambdaは引数にmっていう謎の変数がある!
これはどうやら
(f x)が(lambda (m) (m x x))に置き換えられるっぽい。たぶん。
なので
(f 3)は(lambda (m) (m 3 3))に置き換えられて、*を代入すれば3*3が得られるということかな。
ややこしい。
使っているうちに慣れるんだろうけど。
毎日少しでもコードを書かないと忘れてしまいそう。

とにかく、これがわかれば問題2.4が解ける。cons、carと同じ動作をする関数を定義していて、cdrも同じように定義しろという問題。問題自体は簡単だが、動作がややこしい。
(define (mycons x y)
  (lambda (m) (m x y))
  )

(define (mycar z)
  (z (lambda (p q) p))
  )

(define (mycdr z)
  (z (lambda (p q) q))
  )

(mycdr (mycons 2 3))
3

(mycons 2 3)は(lambda (m) (m 2 3))に置き換えられる。
(mycdr (mycons 2 3))は((mycons 2 3) (lambda (p q) q))に置き換えられ、これは((lambda (m) (m 2 3)) (lambda (p q) q))となる。mに(lambda (p q) q)を代入するわけだ。
するとp=2、q=3が代入され、qが取り出される。うーん、ややこしい。
ジャジャガッチ | LISP | 21:03 | comments(0) | trackbacks(0) |

SICPメモ(7) 問題2.1

SCIPでは有理数を扱うため、次のような手続きを定義している。

(define (make-rat n d) (cons n d))
(define (numer x) (car x))
(define (denom x) (cdr x))
(define (print-rat x) (display (numer x)) (display "/")(display (denom x)))

他にも足し算とか引き算とかもある。有理数を作って実行してみると、
(print-rat (make-rat 2 3))
2/3
ただ、少し問題があって、例えば
(print-rat (make-rat -2 -3))
-2/-3
となってしまう。別にいいっちゃいいような気もするがこれを直せという問題。
単に分母が負なら分子と分母に-1をかければいいだけだ。これだと1 -3を与えたとき1/-3と表示されてしまうものも-1/3となっていい感じ。

(define (make-rat n d)
  (cond
  ((< d 0) (cons (* -1 n) (* -1 d)))
  (else (cons n d))
  )
)
(print-rat (make-rat -2 -3))
2/3

簡単だね。
ジャジャガッチ | LISP | 07:24 | comments(0) | trackbacks(0) |

SICPメモ(6) 2.1.1 cons,car,cdr

2章へ突入。
かなり飛ばし読みしているが、じっくり読み込んでいくのは効率が悪いので飛ばし読みでガンガン先へ進みつつ、気が向いたら前に戻ってじっくり読む込む、という読み方をする。
こういう読み方の方が全体像がわかって読み易い。僕は。

2.1.1ではcons、car、cdrというものを使って有理数を扱う例が紹介されている。
consはペアを作るときに使うらしい。

(cons 2 3)
(2 . 3)

ペアのペアも作れる。

(cons (cons 2 3) (cons 4 5))
((2 . 3) 4 . 5)

car,cdrはペアの一つ目の要素、二つ目の要素の値を返すらしい。

(car (cons 2 3))
2
(cdr (cons 2 3))
3
(car (cons (cons 2 3) (cons 4 5)))
(2 . 3)
(car (car (cons (cons 2 3) (cons 4 5))))
2

次のようなこともできるみたい。
(define (f a b) (+ a b))
(define (g a b) (- a b))
((car (cons f g)) 1 2)
3

ふーん。
ジャジャガッチ | LISP | 07:17 | comments(0) | trackbacks(0) |
1/2PAGES | >> |

03
--
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
--
>>
<<
--
PR
RECOMMEND
RECENT COMMENT
MOBILE
qrcode
OTHERS
Since 2013/09/17
LATEST ENTRY
CATEGORY
ARCHIVE
LINKS
PROFILE
SEARCH