アンダースタンディング・コンピューテーション, メモと感想

 いつの間にか, 大学の図書館に『アンダースタンディング・コンピューテーション 単純な機会から不可能なプログラムまで』(Tom Stuart(著), 笹田耕一(監訳), 笹井崇司(訳), オライリー・ジャパン)があったので, 読みながらのメモと感想.

 読んでいて面白かったのは, 2章, 7章, 8章, 9章でした.

※以下のメモは, 各章に関する内容をまとめたものではなく, 各章を読んでいて, 気づいたこと/思ったこと/思い出したことをメモした内容です.

1章. Ruby

 触ったことなかったけど, Rubyの無名関数は,

 ->arguments { body }

 と書くらしい. 中括弧で関数本体を囲むのはともかくとして, なんで -> arguments なんだろう. Haskellでは, \arguments->bodyとかくけど関係があるのか......?

 Rubyの*演算子はapply関数相当 ... 準クォートのような文字列の式展開.

2章. プログラムの意味

 あやふやになりがちな, Big Step Semantics ↔ Small Step Semantics, 操作的意味論 ↔ 表示的意味論についての説明. 操作的意味論は, インタプリタ的な解釈で, 表示的意味論はコンパイラ的な解釈という感じでしょうか.

Small Step Semantics

 = プログラムの解釈の過程(計算過程)まで定義した反復的(iterative)な意味の定義.

 SchemeのR6RSの意味の定義は, Small Step Semantics. Schemeでも, R5RSやR7RSの定義は, Denotational Semanticsで, R7RSになって, 元に戻された感じ(戻されたといっても内容は違いますが).

Big Step Semantics

 = プログラムの意味を一度に表すための. 再帰的な定義.

以下は, Big Step Semanticsを使った例. Standard MLの定義なのだそうです.

 http://www.lfcs.inf.ed.ac.uk/reports/87/ECS-LFCS-87-36/

3章 & 4章, 5章. 最も単純なコンピュータ & 能力を高める, 究極の機械

 いわゆるオートマトン(DFA, NFA, 正規表現, PDA, 構文解析など)の章. ここ最近, 形式言語関連はうんざりする程付き合ってきたので, ほとんど読み飛ばしてしまいました. 「形式言語とオートマトン」の教科書の内容が噛み砕いて解説されている印象. 学部生の頃に出会いたかったかな. 

 当然のように, (非)決定性オートマトン→正規表現→プッシュダウンオートマトン→構文解析→チューリングマシンという流れでした. 5章は, 究極の機械というタイトルですが, 内容はただのチューリングマシンです.

6章. 無からのプログラミング

 ここで遂に型なしラムダ計算が登場します. Rubyの無名関数, ->arguments { body }を使って, ラムダ計算をエミュレートします. pp.188-191にかけてのFizz Buzzは圧巻です.

 ちょっと特徴的だったのが, リストの扱いでした. ラムダ計算では, λxyf. f x yに相当する(Lispでいうところの)consは, PAIRと, car/cdrに相当する関数がLEFT/RIGHTと名付けられていました.

 これだけだと, 単に名前を変えただけなのですが, リストとconsセルを区別するために, 独自のリスト構造を定義しています. 初めて見る定義だったのですが, UNSHIFTというオペレータでリストを構築し, FIRST/RESTで要素を取り出します.

 UNSHIFTは, ほぼconsと機能的には同等のもので, UNSHIFTは, Rubyのunshiftメソッドに由来しているようです. Rubyのプログラムをそのままラムダ計算でエミュレートする流れであったため, リストのconsingは, UNSHIFTで行うということなのでしょう.

 例えば, (1 2)のようなリストは素朴なconsセル(この場合PAIR)を使った場合, データ構造としては, こんな感じのはずですが,

 本書では, 同じ (1 2)のリストは, 次のような構造になります. 素朴なconsセルのケースと同様に, PAIRにより構成されますが, 少し構造が違います.

  それで, UNSHIFTというオペレータで, 次のように構築しています.

 リストの各要素の手前にあるtrue/falseは, リストが空かどうかを判定するために用いられていました. この辺りがちょっと独特です.

7章. 至るところにある万能性

 このセクションは, チューリング完全な(計算)システムのコレクションです. 前半には, ラムダ計算, SKIコンビネータ, ι(イオタ)コンビネータ, 部分再帰関数のチューリング完全性についての説明があります.

 ラムダ計算で, チューリングマシンのエミュレータを書いて, SKIコンビネータで, ラムダ計算をエミュレートして, SKIコンビネータをιコンビネータでエミュレートして, という作業を繰り返すと, この３つがチューリング完全だという話でした.

 ところが, 中盤に, 普通の「形式言語」の教科書ではあまり扱われないタグシステムというのが登場します. 私にとっては, チューリングマシンやラムダ計算に比べると地味な存在でした. しかし, タグシステムに修正を加えた(同じようにチューリング完全な)循環タグシステムが, 「コンウェイのライフゲーム」や, 「ウルフラムの2, 3のチューリングマシン」がチューリング完全であることの証明に使われているという話があり, 面白いと感じました.

 余談ですが, このセクションで挙げられたもの以外では, 「マルコフアルゴリズム」なんかもチューリング完全です.

8章. 不可能なプログラム

 いわゆる停止性問題.

9章. おもちゃの国のプログラミング

 割りとふざけたタイトルに思えますが, 9章は, 抽象解釈(Abstract Interpretation)についての非形式的な説明が載っています. 「おもちゃの国」というのは, 要するに「抽象的なプログラムの世界」という意味なのでしょう.

 抽象解釈とは, プログラムの抽象的/近似的な実行(または解釈)のことです. あるプログラム(関数)が正しい結果を返すのかについて調べるために, そのプログラムへの入力をすべて試すというのは無理なので, よりシンプルな領域へ抽象化して, 抽象化された世界での結果を調べるという手法です.

 本書では, 掛け算における整数の符号の例の説明がありますが, 例えば, ある整数の元(z ∈ Z)同士の積は, 表で表すと, いわゆる無限に続く掛け算の九九のような形になります. それを正の数 : Pos, 負の数 : Neg, ゼロ : 0 からなる領域S = {0, Pos, Neg}で抽象的な表すと次のような表に収まりました. これが抽象解釈における抽象化です.

 で, 例えば, 1×-2 = -2のような計算が抽象化されて, Pos×Neg = Negのような計算(解釈)の世界が得られます.

 この時, 

f(x, y) = 1÷(if x * y < 0 then x else 2)

 というプログラムがあった時, この関数がゼロ除算のエラーを出さないことを調べたいとします.

 x, yがInteger型なら, Integer型の変数のペアの範囲すべてについて網羅的に計算すれば(とりあえず)OKです. つまり, こんな簡単なプログラムに, Integer.MAX_VALUE * Integer.MAX_VALUE回も実行する必要があり, 現実的ではありません.

 しかし, 抽象解釈なら, 上の領域S = {0, Pos, Neg}について, 3 * 3の9通りについて調べればよく, (f(0, 0) = Posとか, f(Neg, Pos) = Negといったふうに計算します.) 上記のプログラムは, ゼロ除算が起きないことを, (抽象解釈の世界にいながらにして), 知ることができます. 同じように網羅的に調べているだけですが, 抽象化おかげで計算量が格段に減っています.

 もっとも, 現実の問題がここまでうまくいく筈もありませんが, 少なくともこのようなケースが存在することは, 抽象解釈のアプローチが, ある種の問題に対して, 有効であることを示唆していると思います.

Hy(lang), Lisp風味のPythonを使ってみた

 hy(lang)は, Lispです.

hylang/hy ･ GitHub

Welcome to Hy’s documentation!

 公式にあるように, pipから簡単にトライできます.

Quickstart - hy 0.10.1 documentation

 以下の記事は, hyのversion 0.10.1についての内容です.

 シンタックスは, 見た目, ほぼClojureにそっくりですが, cond, let式などをはじめとして, 微妙に異なる部分があるのと(どちらかといえばSchemeやRacketに近い), Python風の構文がいくつか含まれているなど, yet-another Clojureだと思ってプログラムを書こうとすると, 結構嵌まりました.

 ClojureからNumpyとか使ってみたい気もしますが, ベースがPythonであることもあり, hylangは, Clojureとは別の道を歩もうとしているようです.

 何回も使いまわしていますが, 8Queen問題の解法のプログラムを, Clojureで,書くと以下のような感じになるところを,

;; slove the 8 queen problem
(defn conflict? [x y others]
  (and (not (empty? others))
       (let [x1 (ffirst others) y1 (second (first others))]
         (or (= x x1) (= y y1)
             (= (- x x1) (- y y1)) (= (- x x1) (- y1 y))
             (conflict? x y (rest others))))))

(defn put-a-queen [x y others]
  (cond
   (< 7 x) false
   (not (conflict? x y others)) [x y]
   :else (put-a-queen (inc x) y others)))

(defn solve [x1 y1 answer1]
  (loop [x x1 y y1 answer answer1]
    (let [rests (rest answer)]
      (cond
       (and (< 7 x) (= 0 y))
       nil
       (< 7 y)
       (cons answer (solve (inc (ffirst answer)) (dec y) rests))
       :else
       (if-let [xy (put-a-queen x y answer)]
         (recur 0 (inc y) (cons xy answer))
         (recur (inc (ffirst answer)) (dec y) rests))))))

;; make the list of solutions
(def solutions (solve 0 0 []))

 hyで書くと, 次のようになりました.

;; slove the 8 queen problem
(require hy.contrib.loop)
(require hy.contrib.anaphoric)

(defn conflict? [x y others]
  (and (not (empty? others))
       (let [[x1 (car (car others))] [y1 (car (cdr (car others)))]]
          (or (= x x1) (= y y1)
              (= (- x x1) (- y y1)) (= (- x x1) (- y1 y))
              (conflict? x y (cdr others))))))

(defn put-a-queen [x y others]
  (cond
   [(< 7 x) false]
   [(not (conflict? x y others)) [x y]]
   [:else (put-a-queen (inc x) y others)]))

(defn solve [x1 y1 answer1]
  (loop [[x x1] [y y1] [answer answer1]]
    (let [[rests (cdr answer)]]
      (cond
        [(and (< 7 x) (= 0 y))
         nil]
        [(< 7 y)
         (cons answer (solve (inc (car (car answer))) (dec y) rests))]
        [:else
         (ap-if (put-a-queen x y answer)
           (recur 0 (inc y) (cons it answer))
           (recur (inc (car (car answer))) (dec y) rests))]))))

;; make the list of solutions
(def solutions (solve 0 0 []))

 ぱっと見は, Clojureとそっくりに書けることがわかります. もちろん, この書き方がhyの標準的なスタイルかどうかは分かりませんが. def/defnの記法は, Clojureと同じで, 大括弧([])を多様する書き方が, 全体をClojureっぽく見せているのだと思われます.

 condとlet式の部分は, 要素を偶数個並べる書き方ではありません. condは, 条件式とそれに対応する節のペアを括弧で囲います. letも, 変数を表すシンボルと, 割り当てる値を計算する式をリストで組にしたものを並べます(この辺は, Clojure感覚で書いていると, エラーが続出して, 結構嵌まりました).
 true/falseも, #t/#fではなく, true/falseのキーワードで表します. (Schemeと混同してました. 2015/02/02)

(defn put-a-queen [x y others]
  (cond
   [(< 7 x) false]
   [(not (conflict? x y others)) [x y]]
   [:else (put-a-queen (inc x) y others)]))

 さらに, car/cdrが復活しています(ただし, first/restも使えます).  loop/recurスペシャルフォームが使えますが, デフォルトでは使えません. contribからロードする必要があります.

(require hy.contrib.loop)

 こんな感じで, 割と表記上の問題は解決出来たのですが, リスト操作が不可解で, 結構難しかった印象です.

 一つは, empty?の特殊さで, これはリストの長さを計るのですが, (= (len ls) 0)の結果を返します. リストにrestをかけるとitertools.isliceというオブジェクトが生成されますが, このitertools.isliceオブジェクト, countableではないようで, (empty? (rest [1 2]))などと書くとエラーが出ます. そもそもempty?は, リストの長さを数える必要がないのですが, この辺はまだ, 実装途中といった感じなのかもしれません.

=> (rest [1 2])
<itertools.islice object at 0x271d208>
=> (empty? (rest [1 2]))
Traceback (most recent call last):
  File "<input>", line 1, in <module>
  File "/home/uks/Dropbox/langs/lisps/hy/example/env/local/lib/python2.7/site-packages/hy/core/language.hy", line 124, in is_empty
    (= 0 (len coll)))
TypeError: object of type 'itertools.islice' has no len()
=> (cdr [1 2])
[2L]

 ちなみにcdrが返すのはitertools.isliceではないようです.

 さらに, (憶測ですが)nil = Noneだったり, car ≠ first, cdr ≠ restだったり, 各関数がどのような内部クラスやオブジェクトの操作に対応しているのか知らないと, 嵌まるポイントがいくつかありました.

=> (first (rest (cons 1 None)))
=> (car (cdr (cons 1 None)))
Traceback (most recent call last):
  File "<input>", line 1, in <module>
  File "/home/uks/Dropbox/langs/lisps/hy/example/env/local/lib/python2.7/site-packages/hy/models/list.py", line 43, in __getitem__
    ret = super(HyList, self).__getitem__(item)
IndexError: list index out of range

 ネガティブなコメントが多くなってしまいましたが, 個人的には, Syntaxの観点から見ると, Clojureの書きにくかった部分が書きやすくなってるなーという印象です. Clojureは括弧の数を減らそうとしている箇所(cond, letなど)が多数見受けられますが, 逆にそこが仇となっている感じでしたがhylangでは元に戻っていました. リスト内包記法なんかも, Clojureのforとは比べ物にならないほど読みやすいです. リーダマクロも使い放題ですし.

 同じ機能を持つ関数やスペシャルフォームが, 複数名前があることが多いです. 例えば, 前述したcar/firstやdefn/defun, do/prognなどがあります.

 アナフォリックマクロが大量に定義されていて, contribをロードすると, 使えるようになります. anaphoricなのでapが頭につくみたいですね. ap-ifで, itに条件式の結果をbindします.

=> (require hy.contrib.anaphoric)
=> (ap-if true it false)
True