うはwww Mosh で Grass 実装したwwww
ちょっと草植えときますね型言語 Grassを Mosh で実装しました。
_, ._ ( ・ω・) んも〜 ○={=}〇, |:::::::::\, ', ´ 、、、、し 、、、(((.@)wvwwWWwvwwWwwvwwwwWWWwwWw wWWWWWWwwwwWwwvwWWwWwwvwWWW
実行の様子
; w を表示 (grass-eval "wWWwwww" e0 d0) => w ; 1 + 1 の答えを w の数で表示 (grass-eval "wwWWwv wwwwWWWwwWwwWWWWWWwwwwWwwv wWWwwwWwwwwWwwwwwwWwwwwwwwww" e0 d0) => ww ; 無限の草 (grass-eval "無限に草植えときますねwWWwwwwWWww" e0 d0) => wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww ....
Grass 実装の動機
- Mosh で実用的なコードを書こう
- 以下の難しそうなテーマを学習
- 操作的意味論
- ラムダ計算
- チャーチ数
- 難しい式を読めるようにしたい。こういうの→(App(m, n) :: C, E, D) → (Cm, (Cn, En) :: Em, (C, E) :: D) where E = (C1, E1) :: (C2, E2) :: … :: (Ci, Ei) :: E' (i = m, n)
コードと言い訳
動作させるには trunk 版の Mosh が必要です。
コード(あれ。Google code 死んでる)
あとコードの後に仕様の理解する過程のメモを残しておきました。
; grass.scm - Grass interpreter ; http://www.blue.sky.or.jp/grass/ ; ; Copyright (c) 2008 Higepon(Taro Minowa) <higepon@users.sourceforge.jp> ; ; Redistribution and use in source and binary forms, with or without ; modification, are permitted provided that the following conditions ; are met: ; ; 1. Redistributions of source code must retain the above copyright ; notice, this list of conditions and the following disclaimer. ; ; 2. Redistributions in binary form must reproduce the above copyright ; notice, this list of conditions and the following disclaimer in the ; documentation and/or other materials provided with the distribution. ; ; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ; "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT ; LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR ; A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT ; OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, ; SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED ; TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR ; PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF ; LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING ; NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS ; SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ; ; $Id$ (define (make-app n m) `(app ,n ,m)) (define (make-abs n c) `(abs ,n ,c)) (define (make-primitive tag val proc) `(primitive ,tag ,val ,proc)) (define (primitive? p) (match p [('primitive . more) #t] [else #f])) (define (primitive-val p) (third p)) (define (primitive-proc p) (fourth p)) (define (primitive-is? p tag) (eq? (second p) tag)) (define church-true (cons (make-abs 1 (make-app 3 2)) (cons '() '()))) (define church-false (cons (make-abs 1 '()) '())) (define (make-char ch) (make-primitive 'char ch (lambda (c) (if (eq? c ch) church-true church-false)))) (define out (make-primitive 'proc '() (lambda (c) (unless (primitive-is? c 'char) (error "out:charcter required")) (display (primitive-val c)) c))) (define succ (make-primitive 'proc '() (lambda (c) (unless (primitive-is? c 'char) (error "succ:charctor required")) (let1 v (char->integer c) (if (= v 255) (integer->char 0) (integer->char (+ v 1))))))) (define in (make-primitive 'proc '() (lambda (x) (let1 c (read-char) (if (eof-object? c) x (make-char c)))))) (define w (make-char #\w)) (define (grass-eval text env dump) (define (rec code env dump) (define (env-ref i) (list-ref env (- i 1))) (define (nth-code n) (car (env-ref n))) (define (nth-env n) (cdr (env-ref n))) (match code [(('app m n) . c) (let1 mth (env-ref m) (if (primitive? mth) (rec c `(,((primitive-proc mth) (env-ref n)) . ,env) dump) (rec (nth-code m) `((,(nth-code n) . ,(nth-env n)) . ,(nth-env m)) `((,c . ,env) . ,dump))))] [(('abs 1 cc) . c) (rec c `((,cc . ,env) . ,env) dump)] [(('abs n cc) . c) (rec c `((,(list (make-abs (- n 1) cc)) . ,env) . ,env) dump)] [() (if (null? dump) '() (rec (caar dump) `(, (car env) . , (cdar dump)) (cdr dump)))] [else (error "grass-eval runtime error")])) (rec (parse text) env dump)) (define e0 `(,out ,succ ,w ,in)) (define d0 `(((,(make-app 1 1)) . ()) (() . ()))) (define (parse text) (define (normalize t) (list->string (filter (lambda (p) (memq p '(#\w #\W #\v))) (string->list (regexp-replace-all #/W/ (regexp-replace-all #/v/ (regexp-replace-all #/w/ t "w") "v") "W"))))) (define (parse-body t) (aif (#/^(W+)(w+)(.*)/ (if t t "")) (cons (make-app (string-length (it 1)) (string-length (it 2))) (parse-body (it 3))) '())) (map (lambda (x) (aif (#/^(w+)(.+)/ x) (make-abs (string-length (it 1)) (parse-body (it 2))) (error "syntax error"))) (string-split (normalize text) #\v))) (grass-eval "wwWWwv wwwwWWWwwWwwWWWWWWwwwwWwwv wWWwwwWwwwwWwwwwwwWwwwwwwwww" e0 d0) (grass-eval "wWWwwww" e0 d0) (grass-eval "無限に草植えときますねwWWwwwwWWww" e0 d0)
あと church-true あたりが間違っている気がします。
仕様の理解の過程
Grass the grass-planting programming languageにある英語で書かれた詳しい仕様を読み解いていきます。
そもそも操作的意味論を知らないも同然だし、記号の意味も知らない。
まずはこれから。
I ::= App(n, n) | Abs(n, C) C ::= ε | I :: C
App と Abs が何かというのはとりあえず考えないで記号的に読みとる。
- ::= は定義(?)を表す
- :: は cons を表す(::= と似ているけど関係ないのがいやらしい)
- | は or 。
- ε は nil を表す
ので、日本語で書くと
- I ってのは App(n, n) または Abs(n, C) のどちらか
- C ってのは nil または cons(I C)
ということかな。
nil と cons ってことで気付くと思うけど C はリストになり得る。
たとえば cons(App(x, x) nil) や cons(App(x, x) cons(Abs(y, C) nil)) はいずれも C であり。
リスト形式で書けばそれぞれ (App(x, x)), (App(x, x) Abs(y, C)) となる。
ここまでは分かった。
n
n は正の整数。
App(m, n)
操作的意味論の記述の前に書かれている通り App は関数適用。
m, n はそれぞれスタック上のインデックスで、関数の位置、引数の位置を示す。
多分あとで詳細な説明があるはず。
Abs(n, C)
Abs は関数定義。
n は引数の数。
C は関数本体。(Cの定義により、関数本体が関数定義を含んで良いことが分かる。
ここまでのまとめ
- I はコードの要素
- App(n, n) か Abs(n, C)
C はコード
-
- I のリストか、空
f E D
- f は semantic object
- E は environment
- D は suspended computation(中断して再開を待っている計算)
を定義するらしい。
f ::= (C, E) E ::= ε | f :: E D ::= ε | (C, E) :: D
記号を読みとると
- f は (C, E) だ
- E は f のリストだ(空も含む)
- D は (C, E) のリストだ(空も含む)
あれれ。E と D の違いが分からない。とりあえず保留しておこう。
マシンの状態を変化させるルール
Grass の操作的意味論はマシンの状態を変化させるルールで定義されるらしい。
マシンの状態は (C, E, D) で表わされる。
特定のルールで状態が変わることを
(C, E, D) → (C', E', D')
と表現するみたい。
C はコードの塊。
ルール1
簡単そうなものから。
関数定義がコードの塊の先頭にあるとき。
n = 1 ってことは引数の数が1つ。
(Abs(n, C') :: C, E, D) → (C, (C', E) :: E, D) if n = 1
2つの事が起こる。
- コードの塊の先頭から Abs(n, C') を取り除く。
- (C', E) を E のリストの先頭に追加する。
関数の body とそれを実行する環境をリストに追加する感じ。
ルール2
(Abs(n, C') :: C, E, D) → (C, (Abs(n - 1, C')::ε, E) :: E, D) if n > 1
関数定義がコードの塊の先頭にあり、引数が2つ以上。
- コードの塊の先頭から Abs(n, C') を取り除く。
- (Abs(n - 1, C')::ε, E) を E のリストの先頭に追加する。
- n = 1 のときは C' だったものが Abs(n - 1, C')::ε になっている。これは何だ。
- そうか引数の数が n - 1 の関数定義を関数の body にしているのか。
ルール3
(ε, f :: E, (C', E') :: D) → (C', f :: E', D)
記号の意味が分かり、だんだんと直感的に読めるようになってきた。
コードの塊が空(nil)になったので D の先頭から ('C, E') を取り出して実行を継続する。
これは return だね。
ルール4
(App(m, n) :: C, E, D) → (Cm, (Cn, En) :: Em, (C, E) :: D) where E = (C1, E1) :: (C2, E2) :: … :: (Ci, Ei) :: E' (i = m, n)
さて一番難しそうなやつ。関数適用。
- コードの塊から App(m, n) を取り出す。
- D の先頭に (C, E) を追加。
- return 先を push することに相当。(適用の後に戻ってくる)
- environment の先頭からm 番目の (Cm, Em)を参照する。
- コードの塊に Cm を設定する。
- 関数の body のコードに相当。
- 引数 (Cn, En) :: Em を environment に設定する
さてと関数適用では何が起きる?
- C(コード)が関数本体になる
- 関数適用後の戻り場所が D に追加される
- 引数の environment (Cn, En) + 関数が作られたとき(定義されたとき)の environment が environment になる。
- ここはまだ良く分からないが保留
(App(m, n) :: C, E, D) → (Cm, (Cn, En) :: Em, (C, E) :: D) where E = (C1, E1) :: (C2, E2) :: … :: (Ci, Ei) :: E' (i = m, n) (Abs(n, C') :: C, E, D) → (C, (C', E) :: E, D) if n = 1 (Abs(n, C') :: C, E, D) → (C, (Abs(n - 1, C')::ε, E) :: E, D) if n > 1 (ε, f :: E, (C', E') :: D) → (C', f :: E', D)
プリミティブ
おおよそ理解できたが Church Boolean (λx.λy.x) が分からない。
ラムダ計算 を勉強するか。(http://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%A0%E3%83%80%E8%A8%88%E7%AE%97)
面白いなあ。しまった。これを読んでから草のドキュメント読めば良かった。
abs って「ラムダ抽象」の略なのだな。
説明とても上手なので理解が早い。
つまり、チャーチ数は1引数関数を受け取り、1引数関数を返す高階関数である。
あれ。1引数関数を返すってのが分からないな。
SUCC := λn f x. f (n f x)
おおお。ノートに書いてみたら確かに n + 1 が出てくる。
PLUS は直感的に分かる。
脱線したがそろそろ実装してみるか。
→実装完成