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

 いつの間にか, 大学の図書館に『アンダースタンディング・コンピューテーション 単純な機会から不可能なプログラムまで』(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といったふうに計算します.) 上記のプログラムは, ゼロ除算が起きないことを, (抽象解釈の世界にいながらにして), 知ることができます. 同じように網羅的に調べているだけですが, 抽象化おかげで計算量が格段に減っています.

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

プログラム運算

(2015/01/07修正)

　プログラム運算というのがあるらしい。
最初に見た時は、演算のtypoかと思ったけど、それとは違うらしい。
英語では、「calculational programming」というらしい。
プログラムの最適化手法の一種で、あるプログラムをプログラムの意味を変えずに、変換していくことでより効率的なプログラムに書き換える手法なのだそうです。この手法とコンパイラにおける最適化との違いは、アルゴリズム(抽象)レベルで最適化するか、変換後のコードを最適化するかという違いのようです。

エレガントで綺麗なコード(ただし遅い) → 高速なコード(ただし、汚く読みにくい)

「→」は「数学的理論(プログラム意味論)に基づいた変換」です。
速度的な面から見た、プログラム/アルゴリズムのリファクタリングってことなのかな？

例えば、関数型言語で記述された(速度を考慮していない)フィボナッチ数列を返す関数は、数学的な表現をそのまま表すこができ、非常に綺麗ですが、重たいです。それを、プログラムの意味を数学的な表現に落とし込み、数学的に変形する(もちろん、高速化されることは大前提という)ことで、数学的な等価性から、プログラムの等価性を証明するってことのようです。 (フィボナッチ数列の計算が運算によって高速化できるのかはわかりません.)
最適化すると同時に、その最適化が適切であることを証明する(保証する)ことができると。
　ちなみに、この変換自体は、基本的に人が手で行う模様…… 
(以下, 2015/01/07追記)
 ある意味では, 関数型言語の実行速度のチューニングの一種と言えるのかもしれませんね.

 基本的に手作業に勝るプログラム運算はありませんが, 自動化するシステムもいくつか開発されているようです. 日本語で読める書籍としては, 少なくとも以下の二冊があります(他にもあるかもしれませんが).

• 関数プログラミングの楽しみ, Jeremy Gibbons & Oege de Moor(編集), 山下 伸夫 (翻訳)
• 関数プログラミング入門 ―Haskellで学ぶ原理と技法―, Richard Bird (著), 山下伸夫 (翻訳)

 『関数プログラミング入門』については, 自動運算器の解説があります. 『関数プログラミングの楽しみ』でも, 同様に運算(融合変換)の自動化とその実装例であるMAGシステムの説明がありました.

 手作業で出来る簡単な例として, このブログでは, map分配則と, hylomorphismについて紹介しています.

　以下の文献が見つかりました。まだ、読んでないのですが。
参考文献

定理証明支援系 Coq を用いたプログラム運算

融合変換による関数プログラムの最適化

構成的アルゴリズム論

ラムダ計算の使い方

　ラムダ計算の公理とかはすっ飛ばして、ラムダ計算で実際にどうプログラムを組めるのかをまとめてみました。ラムダ計算による数値の扱い、条件分岐、論理式、ループ構造、そしてリスト構造の作り方について説明します。

　ちなみに
β→はβ簡約、
λx.xはラムダ抽象、
M Nは、式の適用です。
=は、ここでは、同値を表す表現とします。
適宜applyの優先順位を表す為に括弧を用います。
例えば、λabc. x y zなど、ラムダ抽象は簡単のため、カリー化される前のた式として表します。(訂正 2016/05/02, λabc. x y z = λa.(λb.(λc. x y z))という意味です。)

1.チャーチ数

　まず、最初は数値です。チャーチ数とは、ラムダ式で自然数を表現する方法です。ラムダ計算は、数値を扱うことができないように見えますが、ちゃんとした（？）数値計算を自身の計算体系のみで表現することができます。

　まずは、数値の定義方法から紹介します。

　0と1は、次のようにして定義します。

0 = λfx. x

1 = λfx. f x

　ラムダ抽象の中で何回fがapplｙされるかで、数値を表します。2以降は、

2 = λfx. f (f x)

3 = λfx. f (f (f x))

4 = λfx. f (f (f (f x)))

n = λfx. f ( ... (f x) ...)  (fがn個)

........

　以上のようにして表現します。これだけだと表現しているだけですね。なぜ、このように表現するのか、必然性が無いと感じられるかも知れません。

　しかし、これに数値計算方法を組み合わせると面白くなってきます。

　加算は、次のように表します。

plus = λmnfx. m f (n f x)

　なんとなくイメージがつかめると思います。mとnが足し合わせる値です。mの内側にnを突っ込むようなイメージです。元の数値表現に戻ることが確認できるかと思います。
　こんな感じです。

意味 : 1+2

(plus 1 2)
β→  (λmnfx. m f (n f x)) (λfx. f x) (λfx. f (f x))

β→  (λnfx. (λfx. f x) f (n f x)) (λfx. f (f x))

β→  (λfx. (λfx. f x) f ((λfx. f (f x)) f x))

β→  (λfx. (λx. f x) ((λfx. f (f x)) f x))

β→  (λfx. f ((λfx. f (f x)) f x)))

β→  (λfx. f ((λx. f (f x)) x)))

β→  (λfx. f (f (f x)))

=3となります。

　乗算も簡単です。

mult = λmn. m (plus n) 0

　ラムダ抽象mが囲っているそれぞれのfに対して、plus nを適用して展開させます。
　最後に指数です。mのn乗とは次のように記述します。

exp = λmn. m (mult n) 1

　乗算と同じ考え方で、指数も表現出来ました。

　次に、定番なので、インクリメントを表す関数とデクリメントを表す関数を書いてみます。
　インクリメントを表す関数succは、以下のように定義できます。succという名前はペアノの公理に由来します。

succ = λnfx. f(n f x)

　デクリメントを表す関数predは、以下のように定義できます。ちょっと複雑ですね、理解に苦しみます。

pred = λnfx. n (λgh. h (g f)) (λy. x) (λy. y)

意味 : 2 - 1

pred 2
β→  (λnfx. n (λgh. h (g f)) (λy. x) (λy. y))(λfx. f (f x))

β→  (λfx. (λfx. f (f x)) (λgh. h (g f)) (λy. x) (λy. y))

β→  (λfx. (λx. (λgh. h (g f)) ((λgh. h (g f)) x)) (λy. x) (λy. y))

β→  (λfx. (λx. (λh. h (((λgh. h (g f)) x) f))) (λy. x) (λy. y)

β→  (λfx. (λh. h (((λgh. h (g f))  (λy. x)) f)) (λy. y))

β→  (λfx. (λy. y)(((λgh. h (g f))  (λy. x)) f))

β→  (λfx. (((λgh. h (g f))  (λy. x)) f))

β→  (λfx. ((λh. h ((λy. x) f)) f))
β→  (λfx. f ((λy. x) f))

β→  (λfx. f (x))

　こんな感じでしょうか。括弧を調整しようとすると目がしょぼしょぼします。とりあえず、デクリメントの関数ができたので、これを使って減算ができます。

　減算は次の様になります。

sub = λmn. n pred m

　あっけないです。m-nを表す関数でした。λfx. f(...f(x)...)でネストしてるfをpredに置き換え、xをｍに置き換えています。これにより、predがn回mに対して適用される仕組みです。

 注意 : この方法だと, sub 1 2 を簡約すると0になります. 上記の定義では, 負の数は扱えません.(2015/01/30追記, アンダースタンディング・コンピューテーションより.)

　同様の仕組みで、加算も定義ができます。predのところをsuccに変えるだけです。

plus = λmn. n succ m

2.分岐構造

　いわゆるif-else文をラムダ計算で表すことができます。次のように記述します。

true = λxy. x

false = λxy. y

if = λcxy. c x y

　if は、一番目の式にtrue/falseを表す要素を受け取り、二番目にtrueだった場合の式を受け取り、三番目にfalseだった場合の式を受け取ります。trueは、2つ式を受け取り、受け取った式のうち、前の式を返します。逆にfalseは、後ろの式を返します。これでif-elseが成立しています。trueやfalseが適宜、ifに与えられた不要な式を切り捨てることでうまく表現することができるようになるのです。

if true A Bについて、次のように簡約されていきます。

(((λcxy. c x y) (λxy. x)) A B)

β→  (((λxy. (λxy. x) x y)) A B)

β→  (((λy. (λxy. x) A y)) B)

β→  ((λxy. x) A B)

β→  ((λy. A) B)

β→  A

正しくtrueの方が選択されていますね。

3.論理式

　if-else についてやると今度は、notやandとかorについてもやってみたくなるが人情だと思います(?)。そこで、ラムダ計算でnot, and, orを表してみます。

not = λx. x false true
and = λxy. x y false
or = λxy. x true y
xor = λxy. x (not y) y

　notは、if文と原理的には同じです。andは、第一引数がfalseならfalse、trueなら、第二引数の値を返します。orは、逆で、第一引数がtrueならtrue、falseなら、第二引数の値を返します。なかなか、うまく表現できています。xorは、and, not, orを使っても書けるので、特に必要無いような気もします。

4.数値判定

　数値判定、具体的には、iszero?やequals?について判定するようなプログラムもかけちゃいます。数値表現とtrue/fasleができるようになったので、ここで紹介します。

　まずは、与えられた数値が0かどうかを判定するiszero?から。

iszero? = λz. z (λx. false) true

iszero? 1

β→ (λz. z (λx. false) true) (λfx. f x)

β→ ((λfx. f x) (λx. false) true)

β→ ((λx.  (λx. false) x) true)

β→ ((λx. false) true)

β→ false

　こんな感じでfalseをちゃんと返してくれます。iszero? 0の場合は自明ですね。0は、二番目に与えられたラムダ式を返す式と考えれば良いので、二番目のラムダ式=trueが帰ってきます。

　次に、あんまり扱われることのないequal?について実装してみたいと思います。その前に、mはn以上であるということを判定するgreater than equalについて実装する必要があります。名前は長いので、gte?にしましょう。

gte? = λmn. iszero? (sub n m)

より、equals?は、

equals? = λmn. and (gte? m n) (gte? n m)

だとわかります。

5.ループ構造

　ラムダ計算における、代表的なループ構造は、Yコンビネータと呼ばれるものです。if式と比較して若干難しいかも知れませんが、気のせいです。

Y = λf. (λx. f (x x)) (λx. f (x x))) 

このように定義されるのですが、これに何か値を渡して、β簡約すると面白いことが起きます。

(λf. (λx. f(x x)) (λx. f(x x))) A

β→  (λx. A(x x)) (λx. A(x x)))

β→  A((λx. A(x x)) (λx. A(x x))))

β→  A(A((λx. A(x x)) (λx. A(x x)))))

β→  A(A(A((λx. A(x x)) (λx. A(x x))))))

β→  A(A(A(A((λx. A(x x)) (λx. A(x x)))))))

　一度目のβ簡約では、自由変数fを記号Aに置き換えただけです。しかし、二度目のβ簡約では、先頭のラムダ式のxを後続のラムダ式に置き換えると、何も変化させていないように見えるのですが、実はよく見ると元の形に戻っています。

　(x x)のxを (λx. A(x x))に置き換えています。

　上記のようにして、無限にAを適用出来るため、この形の式がループ構造として用いることができるのです。

　上記の式ではβ簡約をいくら続けても止まりません。無限ループってやつですね。

　一般にこのようなコンビネータを不動点コンビネータ(もしくは、フィックスなど)と呼びます。

　上記の例以外にも次の式もまた、不動点コンビネータです。

Θ = (λxy. y(xxy)) (λxy. y(xxy))

　このようにして、ラムダ計算では、ループを定義します。

　ここで一瞬、普通の再帰呼び出しでもループを定義できるのでは？　と思うかもしれませんが、気のせいです。通常のプログラミング言語の再帰呼び出しの場合、自分自身の参照を呼び出し時にスコープが捉えています。しかし、ラムダ計算では、自分自身に付けられた名前が参照できるのは、それ自身が引数として与えられたラムダ抽象の内側だけです。したがって、ラムダ計算では直接的な再帰呼び出しを使うことができないのです。残念ですね。
　例えば、以下の例で、

(λx. a b c ...) (λy. x y z ...)

　右側のラムダ抽象で再帰呼び出しを行う場合、自分自身の名前を参照したいのですが、参照できるのは、左側のラムダ抽象だけです。こんな感じの違いがあります。

6.素朴なリスト構造

　関数型プログラミングにリスト構造は必須です。というか、リスト構造があれば、他の構造はリスト構造でだいたい間に合います。唯一データ構造的に不可能なのは、ハッシュマップくらいでしょうか。

　Lispでは、car/cdrとconsセルにお世話になっていますが、ラムダ計算においても、基本的にそのスタイルは変わっていません。consで、リストを作って、carとcdrでリストの要素にアクセスするだけです。

　carは、与えられたリストの先頭の要素を取り出します。

　cdrは、与えられたリストの後続の要素を取り出します。

　consは、第一引数を第二引数で与えられたリストの先頭に付加します。

　例えば、ls = (cons 1 (cons 2 '())で、ls = (1 2)のリストが生成されます。これに対して、(car ls) = 1であり、(cdr ls) = (2)です。Lispでcdrは基本的にリストを返しますし、ここでも2を要素に持つリストが帰ってきていますが、別に要素を返しても問題ありません。(注：イコールは同値関係を表しています。)

　ラムダ計算で上記３つのオペレータを表現するわけですが、実に可愛いものです。

car = λx. x true

cdr = λx. x false

cons = λabf. f a b

　これだけで、原理は、if-else式と似ていますね。consでリストの先頭要素と後続要素をエンクロージングして、最後に、carかcdrを与えて要素を取り出します。

　例えば、次のconsとcdrを使うとこうなります。

意味 : (cdr (cons 1 2))

((λx. x false) ((λabf. f a b) 1 2))

β→  ((λx. x false) ((λbf. f 1 b) 2))

β→  ((λx. x false) (λf. f 1 2))

β→  ((λf. f 1 2) false)

β→  (false 1 2)

β→  2

　要素が取り出せていることが確認できるでしょうか。carの場合は、falseがtrueになるだけなので、根本的な違いはありません。

　ところで、このリストには、まだnilが足りません。リストの終端を表してくれる大事な記号です。
この記号と、この記号を判定する関数を用意しましょう。

nil = false
isnil? = λx. x (λabc. false) true

　こんなので本当にnilと判定してくれるのでしょうか……。とりあえず、isnil?に渡された値がnilであれば正確に判定してくれることは見ればわかります。

(isnil? (cons 1 nil))についてテストしてみましょう。

(isnil? (cons 1 nil))
β→  ((λx. x (λabc. false) true) (cons 1 nil))

β→  ((λx. x (λabc. false) true) ((λabf. f a b) 1 nil))
β→  ((λx. x (λabc. false) true) (λf. f  1 nil))

β→  ((λf. f  1 nil) (λabc. false) true)

β→  ((λabc. false)  1 nil true)
β→  false

　若干β簡約の適用順序に一貫性がないような気がしますが、そこは、チャーチ・ロッサー性ってことで勘弁してもらいましょう。isnil?の真ん中にあるラムダ抽象のabcとは、それぞれリストの先頭(car部)、リストの後続(cdr部)、trueを取り除く為のものだったことがわかります。

これでリストの扱いも完璧になりました。

　以上が　ラムダ計算のざっくりとした使い方の解説でした。本当はリストの扱い方の別パターンも書きたかったのですが、それを書いていると書き終わりそうにないので、ココらへんで終わります。

　ラムダ計算を試すのに専用の処理系(ラムダ計算のエミュレータみたいなもの)は、要りません。Scheme(Racket or Gauche)やその他レキシカルクロージャをサポートしている言語で、無名関数をラムダ関数に見立てれば、簡単にエミュレートできます。ただし、簡約のステップを表示させることはできませんが……
((間違いまたは適切な書き方でなかった為、訂正 2013/07/25)　まず、ラムダ計算には、型付きと型なしの2種類あり、型付きのラムダ計算では、上記のような引き算や繰返し構造をそのまま表現することはできません。上記の説明は、型なしのラムダ計算を前提としています。従って、レキシカルクロージャをサポートしていても、型推論をする、HaskellやOCamlのような言語では、直接記述できるのは、加算と乗算など一部の計算だけです。ループに関しては、再帰型を定義することで実装可能になるようです。また、Clojure、SchemeやPythonのようなか動的型付け言語でも、再帰を扱う為には、不動点コンビネータの多相性を保証するようなテクニックが必要で、そのままラムダ式で直接記述できるわけではありません。)
　

参考文献

• 日英のWikipediaのラムダ計算の項目
• ここで扱っている内容の大半はここにあります。
• http://palmstroem.blogspot.jp/2012/05/lambda-calculus-for-absolute-dummies.htm
• equals?の実装など。
• 横内寛文著 『プログラム意味論』、共立出版、1994年