Egisonプログラミング実例研究： pattern functionとmatcherの活用例
これは Egison Advent Calendar 2013 ２日目の記事です。
「パターンマッチ指向プログラミング」を謳うEgisonでプログラミングすることにおいては当然「パターンをどのように記述するか」ということが最重要課題になってきます。
関数型プログラミングにおいて、大きな関数はより小さな単位の関数の組合せで表わされるように、Egisonではパターンをより柔軟に記述するためにパターンを再利用可能な形でモジュール化(modularization)する pattern-function や、同じデータ型に対する「パターンマッチングによる分解の仕方」を記述する matcher の仕組みが備わっています。これらは全て、「パターンマッチにより値を分解してデータを得る」という操作を、既存のどんな言語より柔軟に行う為のEgison独自の機能です。
ここではこれらのシンタクスや意味論を述べたりすることは目的としません。後に述べるようにpattern-functionは難しいものではありませんし、matcherについては公式か、手前味噌ですが私が書いた Egisonのmatcherの定義（基本編） - claustrophobia を参照してくれればわかると思います。そうではなく、この記事はpatternのモジュール化機能やmatcherによって、パターンマッチングの記述力が如何に豊かなものとなるかを実例を通して見ていくことを目標にしています。
・型無しλ計算（+整数リテラル、オペレータ）のevalの実装
型無しλ計算のeval、すなわち簡約を実装するときには、λ項をパターンマッチングによって分解していくことになります。つまり対象のλ項を分解し、β基を見付けたらβ簡約すればいいわけです。
（λ項 t := x(変数) | λx.t（λ抽象*1）| t1 t2（適用））
(λx. (λy. x y)) (λz. z z)
↓ β簡約（xに(λz. z z)を代入）
(λy. (λz. z z) y)
ここでは純粋なλ計算をちょっと複雑にして、型無しλ項に整数・整数の加算・整数の乗算をプリミティヴとして加えた体系を考えてみます。まずはλ項を表すalgebraic data matcher: termを定義します。
(define $operator (algebraic-data-matcher {<plus> <mult>}))
(define $term
(algebraic-data-matcher
{<var string>
<int integer>
<op operator term term>
<lam string term>
<app term term>}))
整数とその演算を加えたので、evalに際しては先に見たβ簡約の他に、"1+1"のような式を見つけたら"2"に簡約するという操作も考えることになります。
演算子のmatcherも作ったので、この「演算」は次のように「演算子を渡して「整数をその演算子で計算する関数」を返す関数」を書いて実装することにします。
(define $op-reduce
(match-lambda operator
{[<plus> (match-lambda [term term]
{[[<int $i1> <int $i2>] <Int (+ i1 i2)>]})]
[<mult> (match-lambda [term term]
{[[<int $i1> <int $i2>] <Int (* i1 i2)>]})]}))
代入は次のように定義されます。"^,x"というパターンはEgison独自*2のもので、NOTパターン"^(pattern)"は「(pattern)にマッチしない」、Valueパターン",(expr)"は「(expr)を評価した値にマッチ」を意味します。つまり"^,x"で「変数xの値にマッチしない値にマッチ」となり、λ抽象によるshadowingをうまく表現しています。
ただし、この代入関数で自由変数を含む項を代入しようとすると変数の捕獲が起きる可能性があります。が、ここでは閉じた項に関する代入しか起こらないと仮定します。実際、これから書く例では問題なく動作します。
(define $subst
(lambda [$x $t]
(letrec {[$go
(match-lambda term
{[<var ,x> t]
[<op $ope $t1 $t2> <Op ope (go t1) (go t2)>]
[<lam (& $y ^,x) $t1> <Lam y (go t1)>]
[<app $t1 $t2> <App (go t1) (go t2)>]
[$t t]})]} go)))
Egisonで１ステップのevalを実装してみます。まず「値呼び戦略(call-by-value)」すなわち次の規則に従って（1ステップの）簡約が進むevalを考えます。
Case 1. e1 + e2：e1もe2も値であるなら足した結果の整数を返す。そうでなければe1(or e2)の簡約を1ステップ進める。
Case 2. e1 * e2 ： Case 1と同様
Case 3. e1 e2(関数適用)：e1=λx.eでe2も値ならβ簡約。そうでなければe1(or e2)の簡約を1ステップ進める。
この場合分けをパターンマッチで書けばいいだけです
・pattern functionによる「よく使うパターン」のモジュール化
ここで問題になってくるのが「e1 + e2でe1もe2も値だったとき」のような状況の判定です。このケースに限らず、値にマッチするパターンを簡潔に書きたいところです。
Egisonでは、こうした再利用性のあるパターンをpattern functionによってモジュール化できます。
(define $value
(pattern-function [$p] (& (| <var _> <int _> <lam _ _>) p)))
このvalueは1引数のpattern functionであり、(value p)は「値pにマッチする」という意味のパターンです。これを利用すれば、先の「e1 + e2でe1もe2も値だったとき」と「e1 + e2でe1が値、e2が値でない」は次のように書きわけられます。
[<op $ope (value $v1) (value $v2)> ((op-reduce ope) v1 v2)]
[<op $ope (value $v) $t> <Op ope v (beta-reduce-cbv-naive t)>]
これなら、ガードを使ってパターンに補助的な述語を付けるより直接的にパターンに「値にマッチする」情報を書けて直感的です。*3
値呼び戦略の１ステップ簡約は次のようになります。マッチ先における分岐が一切ないように定義することができていますね。
(define $beta-reduce-cbv-naive
(match-lambda term
{[<app <lam $x $t> (value $v)> ((subst x v) t)]
[<op $ope (value $v1) (value $v2)> ((op-reduce ope) v1 v2)]
[<op $ope (value $v) $t> <Op ope v (beta-reduce-cbv-naive t)>]
[<op $ope $t1 $t2> <Op ope (beta-reduce-cbv-naive t1) t2>]
[<app (value $v) $t> <App v (beta-reduce-cbv-naive t)>]
[<app $t1 $t2> <App (beta-reduce-cbv-naive t1) t2>]
[$v v]}))
これでevalの完成です。折角なので関数fで項tをnステップ簡約する関数"n-step"を
(define $n-step
(lambda [$f $t $n]
(if (lte? n 0)
t
(n-step f (f t) (- n 1)))))
と定義して次のexpl
(define $identity <Lam "me" <Var "me">>)
(define $onetwo <Op <Plus> <Int 1> <Int 2>>)
(define $expl <App identity onetwo>)
を簡約してみると
> (n-step beta-reduce-cbv-naive expl 1)
<App <Lam me <Var me>> <Int 3>>
> (n-step beta-reduce-cbv-naive expl 2)
<Int 3>
ちゃんと動いていますね。
・matcherによる評価文脈の分離
私たちはここで、別の評価戦略を考えることもできます。
名前呼び戦略(call-by-name)はいわゆる遅延評価の一つで、次のような規則に従って簡約が進みます。
Case 1. e1 + e2：e1もe2も値であるなら足した結果の整数を返す。そうでなければe1(or e2)の簡約を1ステップ進める。
Case 2. e1 * e2 ： Case 1と同様
Case 3. e1 e2(関数適用)：e1=λx.eならβ簡約。そうでなければe1の簡約を1ステップ進める。
つまり、関数適用の際に引数を評価しないということです。これも先の値呼びと同じく次のように書くことができます。
(define $beta-reduce-cbn-naive
(match-lambda term
{[<app <lam $x $t1> $t2> ((subst x t2) t1)]
[<op $ope (value $v1) (value $v2)> ((op-reduce ope) v1 v2)]
[<op $ope (value $v) $t> <Op ope v (beta-reduce-cbn-naive t)>]
[<op $ope $t1 $t2> <Op ope (beta-reduce-cbn-naive t1) t2>]
[<app $t1 $t2> <App (beta-reduce-cbn-naive t1) t2>]
[$v v]}))
> (n-step beta-reduce-cbn-naive expl 1)
<Op <Plus> <Int 1> <Int 2>>
> (n-step beta-reduce-cbn-naive expl 2)
<Int 3>
さてこれらのコードを見ると、ほとんど同じ書き方で書いているような気がします。そこで、評価戦略の違いをうまく吸収した統一的なbeta-reduce関数を書けないかと考えてみます。つまり、評価文脈を何らかの形で与えてやって、それによってcall-by-valueのevalにもcall-by-nameのevalにもできるような関数です。
簡約というのは一般に、次のように「簡約できる場所 E」*4にある「簡約できる項 t」を評価するということです。
・([(λx.x + 1) 3]) + 5 → ([3 + 1]) + 5 → [4 + 5] → 9
・([(λx.x x) (λy.y)]) (λz.z) → ([(λy.y) (λy.y)]) (λz.z) → [(λy.y) (λz.z)] → (λz.z)
よって、次のような抽象化を考えられます。λ項をパターンマッチにより「簡約できる場所 E」「簡約できる項 t」に分解するようなmatcherを引数に取り、
(define $beta-reduce
(lambda [$strategy]
(match-lambda strategy
{[<context $e <app <lam $x $t1> $t2>> (e ((subst x t2) t1))]
[<context $e <op $ope (value $v1) (value $v2)>> (e ((op-reduce ope) v1 v2))]
[$v v]})))
のような関数を書けば２つの評価戦略を統一できます。（ここでeは項tを受け取って「簡約できる場所」に再び埋めこむ関数）
このmatcherはちゃんと定義でき、例えばcall-by-valueなら次のようになります。
(define $call-by-value
(matcher
{[<context $ $> [something term]
{[<App $t1 $t2> (match [t1 t2] [term term]
{[[(value _) (value _)] {[(lambda [$t] t) <App t1 t2>]}]
[[(value _) _]
(match t2 call-by-value
{[<context $e $t> {[(lambda [$nt] <App t1 (e nt)>) t]}]
[_ {}]})]
[[_ _]
(match t1 call-by-value
{[<context $e $t> {[(lambda [$nt] <App (e nt) t2>) t]}]
[_ {}]})]})]
[<Op $ope $t1 $t2> (match [t1 t2] [term term]
{[[(value _) (value _)] {[(lambda [$t] t) <Op ope t1 t2>]}]
[[(value _) _]
(match t2 call-by-value
{[<context $e $t> {[(lambda [$nt] <Ope ope t1 (e nt)>) t]}]
[_ {}]})]
[[_ _]
(match t1 call-by-value
{[<context $e $t> {[(lambda [$nt] <Ope ope (e nt) t2>) t]}]
[_ {}]})]})]
[_ {}]}]
[$ term {[$t {t}]}]}))
ちょっと複雑ですが、結局再帰的にcall-by-valueにマッチさせてその結果をもとに組み立てる、ということを繰り返しています。call-by-nameも同様に書けます。
こんな風に私たちは同じデータ表現に対して２つ以上のmatcherを定義することで、パターンマッチの仕方を柔軟に切り換えることができます。このように「データの取り出し方は違うが、取り出したデータの組み立て・変換は共通」のようなアルゴリズムがあったとき、matcherはそこから「データの取り出し方」を分離する役目を担うことができます。
・recursive pattern functionの威力
さて、今まで私たちはevalで評価する項は閉じた項であると仮定してきました。つまり、evalで評価する項が自由変数を持っていてはいけません。
では、「自由変数を持った項」はどのように判定すればよいでしょうか？よくある方法が、「自由変数の集合」を求めてみてそれが空であることを判定する方法です。
しかしEgisonでは「閉じた項にマッチするパターン」をpattern functionによって書くことができます。
(define $closed-term
(pattern-function [$p]
(& (freevar-check ^_) p)))
(define $freevar-check
(pattern-function [$bound-vars]
(| <var bound-vars>
<int _>
<op _ (freevar-check bound-vars) (freevar-check bound-vars)>
<lam $x (freevar-check (| bound-vars ,x))>
<app (freevar-check bound-vars) (freevar-check bound-vars)>)))
(closed-term p)が「閉じた項pにマッチする」パターンを表し、(freevar-check p)は「自由変数がpにマッチする項にマッチする」パターンを表します。"^_"はワイルドカードの否定で何に対してもマッチが失敗するので、つまり(closed-term p)とは「自由変数が何にもマッチしない（＝自由変数などない）項pにマッチ」という意味になります。
> (match identity term {[(closed-term $t) t] [_ <ThereAreFreeVars>]})
<Lam me <Var me>>
> (match <App identity <Var "u">> term {[(closed-term $t) t] [_ <ThereAreFreeVars>]})
<ThereAreFreeVars>
ここで注目すべきは、pattern function freevar-checkは再帰関数であるということです。つまりpattern functionは再帰的定義を許します。これは、pattern functionが無限のパターン表現を表すことができるということを意味します。再帰的なpattern functionを使うことでより柔軟なパターンの記述力を得ることができます。
・部品となるpattern functionの組み立て
関数型プログラミングにおいては、部品となる関数を組み立てることでより大きく複雑な関数を定義します。パターンマッチ指向型言語であるEgisonでは、patternを組合せてより複雑なパターンを記述することが可能です。
λ項は帰納的に定義されています。つまり、λ抽象は「λx.(λ項)」という形をしていますし、適用は「(λ項) (λ項)」という形をしています。つまり、λ項は演算型の項・λ抽象・適用をノードとして変数・整数を葉とする木に見立てることができます。そこで、λ項の子ノードにマッチするようなpattern-function "children"を定義できます。
(define $children
(pattern-function [$t]
(| <lam _ t>
<op _ t _> <op _ _ t>
<app t _> <app _ t>)))
さらに、このchildrenを用い、λ項のsubtree全てにマッチするようなpattern function "subtree"を定義できます。
(define $subtree
(pattern-function [$t]
(| t (children (subtree t)))))
さらにさらに、このsubtreeと、先に出てきたfreevar-checkを組合せることで、λ項に表れる全てのμ基: 「λx.M x(ただしMの中に自由なxは出てこない)」にマッチするpattern function "myu-redex"を作れます。
(define $myu-redex
(pattern-function [$x $t]
(subtree <lam x <app (& t (freevar-check ^x)) <var x>>>)))
> (match-all <App <Lam "x" <App identity <Var "x">>> <Int 0>> term [(children $t) t])
{<Lam x <App <Lam me <Var me>> <Var x>>> <Int 0>}
> (match-all <App <Lam "x" <App identity <Var "x">>> <Int 0>> term [(subtree $t) t])
{<App <Lam x <App <Lam me <Var me>> <Var x>>> <Int 0>> <Lam x <App <Lam me <Var me>> <Var x>>> <Int 0> <App <Lam me <Var me>> <Var x>> <Lam me <Var me>> <Var x> <Var me>}
> (match-all <App <Lam "x" <App identity <Var "x">>> <Int 0>> term [(myu-redex $x $t) [x t]])
{[x <Lam me <Var me>>]}
このようにして、どう書いていいかわからない複雑なパターンも、小さい部品のパターンの組み合わせで作り出すことができるようになるのです。
・まとめ
今回主題にするつもりだったのはpattern functionで、matcherについては正直な話「やりたいだけ」でした。というより、以前からこういう形でのevalの定義、つまり評価文脈と簡約基を使ったβ簡約の定義*5を直接コードに落とせないかと思っていて、実際に実現できたので書いてみたというわけです。
しかし、上にも書きましたがmatcherを自分で書くとコードが煩雑になりやすいです。なので、今回Egisonのもう一つの革新的な機能であるpattern functionに焦点を当ててみました。既に見たとおりこちらはかなり簡潔に書けます。というより普通に関数を定義するのと同じ感じです。これは逆に、関数で値を操作するのと同じぐらい柔軟にパターンを操作できるということでもあります。
ちょっとでも面白い・便利そうだと感じたなら、是非、パターンが柔軟に扱える世界でのプログラミングを試してみてください。すると、実は今まで「データを取り出し」「データの性質によって処理を変える」というただそれだけのことに、極めて冗長で退屈な方法を取らされていたことに気付くと思います。
