読んでいて面白かったのは, 2章, 7章, 8章, 9章でした.
※以下のメモは, 各章に関する内容をまとめたものではなく, 各章を読んでいて, 気づいたこと/思ったこと/思い出したことをメモした内容です.
1章. Ruby
触ったことなかったけど, Rubyの無名関数は,
と書くらしい. 中括弧で関数本体を囲むのはともかくとして, なんで -> arguments なんだろう. Haskellでは, \arguments->bodyとかくけど関係があるのか......?
Rubyの*演算子はapply関数相当 ... 準クォートのような文字列の式展開.
->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の定義なのだそうです.
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)を使った場合, データ構造としては, こんな感じのはずですが,
それで, UNSHIFTというオペレータで, 次のように構築しています.
リストの各要素の手前にあるtrue/falseは, リストが空かどうかを判定するために用いられていました. この辺りがちょっと独特です.
ちょっと特徴的だったのが, リストの扱いでした. ラムダ計算では, λ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により構成されますが, 少し構造が違います.
リストの各要素の手前にあるtrue/falseは, リストが空かどうかを判定するために用いられていました. この辺りがちょっと独特です.
7章. 至るところにある万能性
このセクションは, チューリング完全な(計算)システムのコレクションです. 前半には, ラムダ計算, SKIコンビネータ, ι(イオタ)コンビネータ, 部分再帰関数のチューリング完全性についての説明があります.
ラムダ計算で, チューリングマシンのエミュレータを書いて, SKIコンビネータで, ラムダ計算をエミュレートして, SKIコンビネータをιコンビネータでエミュレートして, という作業を繰り返すと, この３つがチューリング完全だという話でした.
ところが, 中盤に, 普通の「形式言語」の教科書ではあまり扱われないタグシステムというのが登場します. 私にとっては, チューリングマシンやラムダ計算に比べると地味な存在でした. しかし, タグシステムに修正を加えた(同じようにチューリング完全な)循環タグシステムが, 「コンウェイのライフゲーム」や, 「ウルフラムの2, 3のチューリングマシン」がチューリング完全であることの証明に使われているという話があり, 面白いと感じました.
余談ですが, このセクションで挙げられたもの以外では, 「マルコフアルゴリズム」なんかもチューリング完全です.
ラムダ計算で, チューリングマシンのエミュレータを書いて, 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といったふうに計算します.) 上記のプログラムは, ゼロ除算が起きないことを, (抽象解釈の世界にいながらにして), 知ることができます. 同じように網羅的に調べているだけですが, 抽象化おかげで計算量が格段に減っています.
もっとも, 現実の問題がここまでうまくいく筈もありませんが, 少なくともこのようなケースが存在することは, 抽象解釈のアプローチが, ある種の問題に対して, 有効であることを示唆していると思います.
0 件のコメント :
コメントを投稿