うはwww Mosh で Grass 実装したwwww

ちょっと草植えときますね型言語 GrassMosh で実装しました。

    _, ._
  ( ・ω・) んも〜
  ○={=}〇,
   |:::::::::\, ', ´
、、、、し 、、、(((.@)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 は直感的に分かる。

脱線したがそろそろ実装してみるか。

→実装完成