CSP Over NSL

この記事は HDL Advent Calendar 2015( http://qiita.com/advent-calendar/2015/hdl )の記事です。

パルテノン研究会( http://www.parthenon-society.com/ )あたりに出そうかなぁと思っていたら塩漬けになってしまっていたものです(いくつか問題があることもあり)。実装はまだ作成しておらず、手作業による「こんな感じにできたらいいな」というProof of Concept未満のコンセプトだけの内容という感じですが、何かの参考になったら、と思います。

まずCSPについてですが、CSPはCommunicating Sequential Processesの略で、並行システムを相互に同期通信する逐次的なプロセス群としてモデル化するものです(詳細は wikipedia:Communicating Sequential Processes や、教科書『並行システムの検証と実装』を参照)

次の「NSL風」コードを見てください。

declare producer_consumer {
    output o;
}

module producer_consumer {
    reg init_reg[2] = 0b01;

    reg s_flip = 0b0;

    $channel_self(chan, 1)

    any {
        0b1 : init_reg = {init_reg[0], 0b0};
        init_reg : {
        }
    }

    $process(Main) $par {
        $start(Sender);
        $start(Receiver);
    }

    $process(Sender)
        $send(chan, s_flip) -> $start(Sender)

    $process(Receiver)
        $recv(chan, "o=") -> $start(Receiver)
}

CSPによる「生産者-消費者」のモデリングを、マクロプロセッサで処理するっぽい構文でNSL中に記述したようなつもり、のものです。

CSPにおける単純なプロセスは、次のような形をしています(形式的な定義の一部を抜粋したものです)。

プロセス : プロセス名
プロセス : イベント → プロセス
イベント : チャネル送信
イベント : チャネル受信
チャネル送信 : チャネル名!変数名
チャネル受信 : チャネル名?変数名

これらを使って、生産者と消費者(送信者と受信者)をプロセスとするように次のようにモデル化し、

Sender = chan!s_flip → Sender
Receiver = chan?o → Receiver

これを言語(+マクロプロセッサ)による記述っぽく変換すると、最初に挙げたリストのようになる、というわけです。

最初のリストから、最終的には次のようなNSLを生成したい、という感じになります(このリストは実際にNSLとして有効なものです。また、CSPの実現として十分なものにはなっていません。それと、ランダムに待ちが入るようなコードが入っているのは、動作チェック用に追加しているもので、形式的な変換中に入れる意図ではありません)。

declare rand_gen simulation {
    output o;
    func_in get_rand():o;
}

module rand_gen {
    func get_rand {
        return _random[16];
    }
}

declare producer_consumer simulation {
    output o;
}

module producer_consumer {
    rand_gen rand_a, rand_b;

    reg init_reg[2] = 0b01;

    reg s_flip = 0b0;

    /* $channel_self(chan, 1) */
    func_self ch_chan_send();
    func_self ch_chan_recv();
    func_self ch_chan_estab();
    wire ch_chan_dat[1];

    func_self p_Main_req();
    func_self p_Main_sub0();
    func_self p_Main_sub1();

    func_self p_Sender_req();
    func_self p_Sender_ack();

    func_self p_Receiver_req();
    func_self p_Receiver_ack();

    any {
        0b1 : init_reg := {init_reg[0], 0b0};
        init_reg[1] : {
            p_Main_req();
        }

        (ch_chan_send & ch_chan_recv) : {
            ch_chan_estab();
        }
    }

    /* $process(Main) $par {
        $start(Sender);
        $start(Receiver);
    } */
    func p_Main_req {
        p_Main_sub0();
        p_Main_sub1();
    }
    func p_Main_sub0 seq {
        p_Sender_req();
    }
    func p_Main_sub1 seq {
        p_Receiver_req();
    }

    /* $process(Sender)
        $send(chan, s_flip) -> $start(Sender) */
    func p_Sender_req seq {
        label_name s0, s1;

        s0 : any {
            0b1 : ch_chan_send();
            ~ch_chan_estab : goto s0;
            ch_chan_estab : {
                p_Sender_ack();
                ch_chan_dat = s_flip;
                s_flip := ~s_flip;
                if (rand_a.get_rand()) goto s1;
            }
        }

        while (rand_a.get_rand()) {
            /* NOP */;
        }

        s1 : any {
            0b1 : p_Sender_req();
            ~p_Sender_ack : goto s1;
        }
    }

    /* $process(Receiver)
        $recv(chan, "o = ") -> $start(Receiver) */
    func p_Receiver_req seq {
        s0 : any {
            0b1 : ch_chan_recv();
            ~ch_chan_estab : goto s0;
            ch_chan_estab : {
                p_Receiver_ack();
                o = ch_chan_dat;
                if (rand_b.get_rand()) goto s1;
            }
        }

        while (rand_b.get_rand()) {
            /* NOP */;
        }

        s1 : any {
            0b1 : p_Receiver_req();
            ~p_Receiver_ack : goto s1;
        }
    }
}

プロセスのシーケンシャルな動作をNSLで実装するためにseqを使っています。また、信号線として func_self による信号線を多用していますが、これは「特段に記述のない状態では Low になる」という特性が必要なためで func らしい機能を必要としているためではありません。

まず、元の記述では $start で表現しているプロセスの動作開始は *_req という信号線のアサートで要求され、実際に動作開始したら _ack がアサートされます。

チャネル通信ではもう少し込み入った動作が必要になります。

送信側は ch_*_send 、受信側は ch_*_recv という信号線をアサートし、両者が同時にアサートされていると ch_*_estab という信号がアサートされるので、送信側・受信側ともに、それを見て送信・受信の動作をし、シーケンスを次に進めます。

(CSPをご存知の方には、そんな単純なアービトレーションでは、(ガードが実現できないのは当然としても)外部選択がある場合に困るのではないか? という疑問があるでしょう。私としては、ハードウェア記述言語に非決定的な記述を入れるのはどうかと思ったため、外部選択を「左側が可能なら左側を、ダメなら右側を」という意味に再解釈し(CFGとPEGのようなイメージです)、少し複雑な例で実験して、「依存関係に循環があると破綻する」という結果を得ています)

最後に、残っている課題ですが、

  • CSP的に正しいかどうかの確認(正しくないとCSPを使う意味がありません)
  • チャネルだけでなくプロセスの動作開始にも調停を入れる(?)
  • 実際にマクロ命令を元に、アービトレーション等の記述を生成するような実装の作成

という感じになるでしょうか(なお、今のところ予定しているわけではありません)。

Common Lispで実装する非再帰eval

この記事はLisp Advent Calendar 2015( http://qiita.com/advent-calendar/2015/lisp )の記事です。

まずそこそこの分量がありますが、コード全体を示します。

タイミングが合えばShibuya.lispで発表しようかと思っていたのですが、色々あってそのままになっていたのでここで公開します。というわけで以下はトークのノリでだらだらと紹介します。

まず、これはどういうものか、ということについてですが、Common Lispで実装したSchemeです。Common Lispを使っていて不意にSchemeの構文で書きたくなった時などに有用かと思います(実際のところは、他の言語でSchemeを実装するためのプロトタイプとして作りました)。Three Implementation Models for Schemeの影響もなんとなく受けている感じの実装になっていると思います。

実装していない(できていない)ものとして、

  • proper tail call
  • 特殊形式多数
  • ライブラリ的関数多数
  • Scheme的(衛生的)マクロ

があります。

データ構造には、consでスタックを実装したものを使っています。変数をレジスタに見立てていて、最初のほうで定義してある push-r と pop-r というマクロで仮想機械の命令風に操作しています。

(defmacro set-r (reg-name v) `(setq ,reg-name ,v))
(defmacro push-r (reg-name v) `(setq ,reg-name (cons ,v ,reg-name)))
(defmacro pop-r (reg-name)
  `(prog1 (car ,reg-name)
     (setq ,reg-name (cdr ,reg-name))))

また、クロージャ(関数オブジェクト)は car が 'closure となっているリスト、マクロは car が 'macro となっているリスト、で表しています。このへんも定番の手法という感じでしょう。マクロは伝統的なマクロにのみ対応しています。

my-eval が eval 本体です。そのままでは少し大きくて見通しが悪いので、以下に骨組を示します。

(defun my-eval (acc env)
  (let ((stck '(ret))
        (args ()))
    (tagbody
     eval-expr
       (cond
         ((symbolp acc)
          (set-r acc (get-var acc env))
          (go handle-val))
         ((atom acc) ; other atoms
          (go handle-val))
         ((consp acc)
          (let ((a (car acc))
                (d (cdr acc)))
            (case a
              (quote
               (cond
                 ((and (consp d) (null (cdr d)))
                  (set-r acc (car d))
                  (go handle-val)))
               (error "my-eval: quote: syntax-error"))
        ...
              (otherwise ; other application form
               (push-r stck d)
               (push-r stck 'pre-apply)
               (set-r acc a)
               (go eval-expr))))))
       (error "ERROR 1")
     handle-val
       (case (pop-r stck)
         (ret
          (return-from my-eval acc))
         (post-def
          (let ((sym (pop-r stck)))
            (rplaca env (cons (cons sym acc) (car env)))
            (set-r acc sym))
          (go handle-val))
         (arg
          (push-r args acc)
          (set-r acc (pop-r stck))
          (go eval-expr))
        ...
         (post-get
          (set-r acc (get-var acc env))
          (go handle-val)))
       (error "ERROR 2"))))

envは環境のチェイン、stckには「accにある式が値になった後にすべきこと」が積まれます。argsは実引数のリストで (f a b c d) のような関数適用の式の、引数 a b c d を順番に評価している時に、すでに評価された引数の値が残されていって、全ての引数の評価が終わると f に適用されます。

accという変数には、「これから評価しようとしている式」あるいは「その式が評価された値」が入ります。巨大な tagbody になっていて、前半側には go eval-expr で、後半側には go handle-val で飛ぶようになっているわけですが、acc に式を入れたら go eval-expr して、その式の値が求まって acc に値が入っている状態なら go handle-val するわけです。次に、eval-expr と handle-val の、それぞれでの動作を見ていきます。

その前にまず (f a b c d) のようなフォームの評価順について説明しておきます。f が特殊形式やマクロ名だった場合は引数の評価を始めてはいけないわけですから、まず f についてそのチェックをする必要があります(設計によっては、そのまま f を評価してしまっても良いわけですが、この実装ではそのようにはしていません)。特殊形式でもマクロ名でもなかった場合は、普通の関数適用として引数を評価し(引数の評価順は左から右としました)最後に関数位置にある f を評価して(値は関数オブジェクトになるはず)、apply、というような感じになります。

     eval-expr
       (cond
         ((symbolp acc)
          (set-r acc (get-var acc env))
          (go handle-val))
         ((atom acc) ; other atoms
          (go handle-val))
         ((consp acc)
          (let ((a (car acc))
                (d (cdr acc)))
            (case a
              (quote
               ...

では、eval-expr の動作を細かく見ていきます。まず、acc の値がシンボルであれば名前解決を行い、それ以外の atom であれば自己評価型としてそのまま handle-val に移ります。どちらでもなければ(一応 consp でチェックして)特殊形式あるいはマクロであればその処理、それでなければ関数適用のための処理、という感じになります。

ここで、たとえば if の処理であれば (push-r stck 'post-ifthen) のようにスタックに何か積んでいるものが多いですが、これはどういうことかというと、if であればまず (if c a b) の c の部分の式を acc に設定し、それを評価するわけですが、その値が得られた後に handle-val でその得られた値を元にどうにかする、という感じになるわけで、それをコードに実装するとこういう感じになります。

acc の式を評価して値が得られた場合(たとえば変数名だったので名前解決がされた、など)には go handle-val となって、my-eval の下側半分にあるコードが実行されます。

具体的には、

     handle-val
       (case (pop-r stck)
         (ret
          (return-from my-eval acc))
         (post-def
          ...

のように、スタックから先頭を取り出して、その内容に応じてcaseで多分岐して、といったようになっているわけです。先ほどの if の続きを見てみます。

         (post-ifthen
          (let ((then-clause (pop-r stck)))
            (cond
              (acc
               (set-r acc then-clause)
               (go eval-expr))
              (t
               (set-r acc ())
               (go handle-val)))))

if が現れたフォームを調べた段階で、else 節があるかないかはチェックしてあり、それに合わせて振り分けられています。こちらは else 節が無い場合です。

(if 条件 expr) のようなフォームの「条件」の部分を評価した値が acc に入っていますから、それを実装言語の cond に掛けて振り分けています。被実装言語の(準)真偽値として実装言語のそれがそのまま使われるようなコードになっていますが、もし変えたい場合はこのあたりを適当に書き換えればいいわけです。真っぽい値の場合はスタックに積んであったthen節の式を acc に入れて、また式の評価に戻るので go eval-expr しています。一方、偽っぽい値の場合は acc に空リスト(nil)を入れて handle-val の操作を続けます。

スタックの底には、最初に ret というシンボルを入れているので、

(defun my-eval (acc env)
  (let ((stck '(ret))
        (args ()))
    (tagbody
     ...

「残りのすべきこと」が全て無くなるとこれが取り出されて、

     handle-val
       (case (pop-r stck)
         (ret
          (return-from my-eval acc))

この先頭部分のパターンによって return-from で関数 my-eval を抜けます。

最後にcallccについてです。

SchemeSchemeを実装する超循環評価器であれば、call/ccでcall/ccを実装するという飛び道具が使えるわけですが(『プログラミング言語SCHEME』にコード全体が載っている実例があります)、ここではそれは使えませんので(というのが非再帰型で実装している理由の一つです)Three Implementation Models for Schemeなどを参考にした感じでスタックを保存するようにした実装をしています。

まず call/cc は 'conti というシンボルに評価され、関数位置がそのようなシンボルだった場合は特別扱いするような仕掛けがあります。

  (my-eval '(define call/cc (quote conti)) env) ; Q&D hack!

次の段階は handle-val の中で、関数適用などを振り分けている post-apply の中にあって、

         (post-apply
          (push-r args acc)
          (set-r acc (pop-r stck))
          (cond
            ...etc...
            ((eq acc 'conti) ; special case (top half of call/cc)
             (set-r acc (car args)) ; (car args) に call/cc の引数が入っている
             (push-r stck env) ; env は継続のために保存しておく必要がある(argsはこの外側で保存されているはず)
             (push-r stck 'pop-env) ; 再開したらenvを復元するようスタックに積む
             (set-r args (cons (cons 'nuate stck) ())) ; `(nuate stck) という継続オブジェクトが先頭に入った引数リストを作る。cdrにスタックを保存
             (push-r stck 'apply) ; 以上の準備を元に apply を実行する
             (go handle-val))

関数位置の値が 'conti ということは call/cc ですから、この時点での継続をオブジェクトにして、引数の手続きオブジェクトにそれを渡す、ということをしています。

次は、このようにして作った継続オブジェクトが実行される場合です。コードとしてはこの続きに、

            ((and (consp acc) (eq (car acc) 'nuate)) ; ditto (bottom half of call/cc)
             (set-r stck (cdr acc))
             (set-r acc (car args))
             (go handle-val)))

とあります。やはり関数位置の値が '(nuate ...) の場合を特別扱いしているという感じになります。cdr にスタックが保存されてますからそれをスタックにセットし、引数の値をaccに入れて、継続が再開されます。

『日本沈没』に見られる科学用語の濫用

およそ学術においては、自らの分野の専門用語を正確に使うことと同様に、慣れない他分野の専門用語を間違えて使わない注意は重要であろう。コンピュータ科学においても、近年の「学際共同」とやらで他分野にご迷惑をお掛けしていることも多々ありそうに想像する。もし問題があったら、ご指摘・ご鞭撻をお願いしたい、と頭を下げる他無い。

さて、『日本沈没』についてである。SFにおいても、「と学会」などで他所様にオフェンシブな姿勢を見せたりした以上、自らについても襟を正す必要はあるだろう。もっとも、今さら私が少々の瑕疵を上げてみたところで騒ぎになりそうにない作品を選んでいる点では惰弱と言われてもしょうがないかもしれないが。

日本沈没』におけるSFの基本的な手法すなわち「大胆な外挿」には何の問題もない。作中(以下、カッパノベルス版のページを示す*1)たとえば「トンネル効果」を持ち出している場面では(下巻 pp.89~90)別の登場人物がきちんと注意を入れているし、素粒子で起きる現象がそのまま起きていると言いたいわけじゃない、とフォローが続いている*2。あるいはほぼ架空と思われる「ナカタ過程」(小説では暗示にとどまっているが、他メディア版では「日本沈没」を説明できる理論と明にあるものもある。あと「マルコフ過程」のような呼び方を、提案者に敬意を表したものではあるが「尊称」と言うかどうかは少し微妙かもしれない)についても特に問題は見受けられないように思う。

しかし、私の感覚で「これはダメだろう」と感じる点として以下に2個所を挙げる。これだけの力作でわずかこれだけというのはむしろ驚異的な少なさと言えるかもしれないが、それでも、過去に指摘されているのを見たことは無いように思う。

問題がある点の一つめは上巻 p.263

カントールが「集合」を考えつめて自殺し、テューリングが「万能テューリング機械」の理論的可能性を証明して自殺したように……

カントールが集合を深く考えていたであろうことは確かであるし、自殺の主因は心を病んだことそのものだろうとは思うがそれはともかくとして、チューリングの方が問題である。チューリングの自殺前の時期の仕事は生物に関してであって、(万能)チューリング機械は戦前の若き日の仕事であるし、万能チューリング機械というのは、現代の言葉で言うなら、ある程度以上の機能を持ったコンピュータであれば、他のどんなコンピュータをも、速度などはともかく理論上はエミュレーションできる、ということをフォーマルに(形式的に)定義された一種のコンピュータと言える「チューリング機械」で示したもので(その理論的可能性を示すことそれ自体は)そう悩むようなものではない。*3

もう一つは、下巻 p.9、かなり長い「首相の内面描写」の最初のあたりに、

コンピューターがさらに高度に発達し、政治というものが、ゲーム理論選択公理を組み合わせた一種の自動装置になってしまう日が、いつかは来るにしても――

ここで「ゲーム理論」はまさしく政治(と経済)の理論であるから良いのだが、問題はそういった政治的決断とは全く関係のない数理論理の公理の「選択公理」である。言葉の響きから使ったもののように思われるし、執筆当時のフィクション作品では珍しくもないもののひとつではあろうと思うが、少なくとも狭義のハードSFであったなら(『日本沈没』はそれを狙った作品ではないが)避けたい記述だろう。直後の「ラプラスの魔」などその前後も少々きわどい(ラプラスの悪魔は、仮に、現在の状態を「全て」知る存在があったとしたら、未来も全て知っているのと同じことだ、という思考実験であり、当該の部分にあるように、未来に予測不可能なものがあることを示したものではない)が、「選択公理」ほどにまずいものは見当たらないように思う。

*1:手元にあるのは近年の増刷版だが、ページ位置の移動は無いものと思う。詳細には未調査なのだが、いくつかの文庫版とノベルス版で『日本沈没』には冒頭部などにいくつかの差異を確認している。

*2:この部分にある氷河の話はきちんと元ネタの論文はあるらしいが、それでもこの部分が完全にありえないことか、実際に地殻で起きる可能性があることかは興味がある、というようなことを確か堀先生が書かれていたと思う(探し出せなかった)。

*3:あと、すこし細かいことになるが、万能チューリングマシンは、どちらかといえば具体的・構成的に示されたもので「理論的可能性」というのも少し違和感があるかもしれない(この分野で「理論的可能性」という表現では、単に「存在する」としただけの証明だったりすることがある)。

Mechanizeを使うサンプル


こういうツイートを見掛けたので、Mechanizeを使うサンプルを作りました。こんな感じになります

Rubyの多重代入をモデル&コード化する

魔境と言われることもあるRubyの多重代入ですが、再帰的に記述すればそんなにややこしくもないのではないか、という気がしていたので、コードを書き下ろしました。

そんなに徹底的に実インタプリタの挙動をチェックしてはいないので、抜けがある可能性もあります(コメント歓迎します)。

縮小された影

このようなツイートがあったのですが、


影は基本的に実物よりも小さくはならない、という大前提に照らしておかしい、というのはさておき、10mに縮小されていたとして、それが100mを3秒だとしたら、スケールスピード的にどうなのか、を考えてみる。

747だとして、全長70mだから 1/7 、それを元にスケールスピードで考えると 700mを3秒、時速840kmということになるので、同機の巡航速度の時速900kmに対し、そこそこそれっぽい結果ということになる(四戸さんが意図的にあるいは無意識で整合させたものかもしれない)。

次に、1/7 ではキリが悪いので 1/8 として、1/8 倍になる投影とはどのようなものかというのを考えてみる。影というものは、投影面(ここまでの議論では地面)と光源との間に対象物(飛行機)があることで出来るわけだが、コンピュータグラフィックをやっていると、光源から見て対象物の反対側に影を作ってしまったりすることがある。この場合「反対側」ではないが、地中に光源があって、対象物から本来の影とは逆方向の「光源に向かう影」が伸びているとすると、そんな「縮小された影」が出来ることになる。

1/8 の大きさにするためには、飛行機の高度の 1/8 の深さの地中に光源があることになる。あるいは、そのような影をもし実際に作るならば、平行交線のさらに逆の「縮小光線」とでもいうような光線(レンズ等の光学系で実際に作れないこともない)の収束点をその位置にもっていけば、実際に作ることができる。

以下は私の妄想という感じになるが、ヒトは飛行機を見上げている時に無意識になんとなく、そのような「飛行機の向こう側に凹面状に広がる、なぞの縮小光線源」が存在するような感覚があるのかもしれない、とするのはどうだろうか?

学校の階段

このようなツイートがあったのですが、


よく見てみると、騙し絵になっているわけではなくて、たまに見るぐらいには見られるような構造の階段です。階段の幅を狭くして、わかりやすい角度から透視図的に見るとこんな感じの構造です(あ、後から気付いたけど上り下りが逆だ)。

記憶ではラジ館(旧)のビルの階段がこんなだったような記憶があるのですが、記憶違いかもしれません。
ただ、イラストの校舎の構造はやはり少し謎で、廊下が横方向に伸びていて階段の向こうにも廊下が見えていますから、下の図解で赤く印を付けたような感じで廊下がある、ということになります。2棟の校舎と廊下があって、その2棟にまたがるように階段がある、という構造ということになりそうですから、そうして見てみると、やはりかなり謎な構造の校舎でした……。