2013/05/20

プログラム運算

(2015/01/07修正)

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

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

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

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

 基本的に手作業に勝るプログラム運算はありませんが, 自動化するシステムもいくつか開発されているようです. 日本語で読める書籍としては, 少なくとも以下の二冊があります(他にもあるかもしれませんが).
  • 関数プログラミングの楽しみ, Jeremy Gibbons & Oege de Moor(編集), 山下 伸夫 (翻訳)
  • 関数プログラミング入門 ―Haskellで学ぶ原理と技法―, Richard Bird (著), 山下伸夫 (翻訳)
 『関数プログラミング入門』については, 自動運算器の解説があります. 『関数プログラミングの楽しみ』でも, 同様に運算(融合変換)の自動化とその実装例であるMAGシステムの説明がありました.

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

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

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

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

  • 構成的アルゴリズム論
  • 2013/05/18

    ラムダ計算の使い方

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

     ちなみに
    β→はβ簡約、
    λ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がapplyされるかで、数値を表します。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をmに置き換えています。これにより、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を要素に持つリストが帰ってきていますが、別に要素を返しても問題ありません。(注:イコールは同値関係を表しています。)
     ラムダ計算で上記3つのオペレータを表現するわけですが、実に可愛いものです。

    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のようなか動的型付け言語でも、再帰を扱う為には、不動点コンビネータの多相性を保証するようなテクニックが必要で、そのままラムダ式で直接記述できるわけではありません。)
     

    参考文献