Go to the first, previous, next, last section, table of contents.


書替え規則の代数的性質

書替え機構は `+'`*' などの代数的性質を理解します。 特に、パターンマッチングは下記の関数の結合則や交換則を考慮に入れて機能します。

+ - *  = !=  && ||  and or xor  vint vunion vxor  gcd lcm  max min  beta

例えば、次の書替え規則

a x + b x  :=  (a + b) x

は、次のような式にマッチします。

a x + b x,  x a + x b,  a x + x b,  x a + b x

また書替えエンジンは `+'`-' の関係も理解しています。 上記の書替え規則は、 ターゲット式中の `-b' にパターンの `b' をマッチさせることで、 次のような式にもマッチします。

a x - b x,  x a - x b,  a x - x b,  x a - b x

このパターンを多数項の和に適用すると、 各項の全ての組合せのマッチング可能性をチェックします。 書替えはどれでも先に発見された組合せから実施されます。

一般に、`a + b' のような結合可能な演算子を使ったパターンは、 n 個の項からなる(`x + y + z - w'のような)和をターゲットとした場合、 2 n とおりの組合せを試します。 まず、`a'`x', `y', `z', `-w' のそれぞれに 順番にマッチしつつ、 `b' がその残り部分 `y + z - w', `x + z - w', ... に マッチングを試みます。 どれも成功しなければ、次に `b' が4つの項にマッチしつつ、 `a' が残り部分にマッチングを試みます。 `(x + y) + (z - w)' のような、半分ずつマッチングする試みは採られません。

`*' は行列については交換則が成立しませんが、 書替え規則は「成立する前提で」振舞うことに注意してください。 m v とタイプして行列モード(行列モードとスカラ・モード 参照 )にすれば、 書替え規則は通常の交換則を「成立しない前提で」 正しく `*' にマッチするようになります。 (現在の実装では、結合則も一緒に消滅します。 ---まるでパターンが plain マーカーに囲まれているかのように;後述) 行列式に書替えを適用するなら、まず行列モードにして、 代数的に正しくない書替えを防止してください。

`-x' というパターンは、事実上どんな式にもマッチしてしまいます。 例えば次の規則

f(-x)  :=  -f(x)

これは、`f(a)'`-f(-a)' に書替えてしまいます。 これを防止するには、後述の plain マーカーを使うか、 `negative(x)' 条件を加えてください。 negative(x) 関数は、引数が負に「見える」場合、 例えば負の数値とか `-x' のような式の場合に真です。 この条件を使った規則は次のとおりです。

f(x)  :=  -f(-x)  :: negative(x)    または
f(-x)  :=  -f(x)  :: negative(-x)   同等の規則

同様に、パターン `y'`-b' にマッチするので、 パターン `x - y'`a + b' にマッチします。

またパターン `a b' は 式 `x/y' にもマッチします(`y' が数値の場合)。 従って、規則 `a x + b x := (a+b) x'`a x + x / 2' も変換して `(a + 0.5) x' (分数モードの状態によっては `(a + 1:2) x') を生成します。

Calc は `*', `/', `^' についてこれ以外の解釈を採りません。 例えば、パターン `f(a b)'`f(x^2)' にマッチしませんし、 `f(a + b)'`f(2 x)' にマッチしません。 おそらくは `a = b = x' という具合にマッチできたのでしょうが。 また、`y' が定数でなければ `f(a b)'`f(x / y)' にマッチしません (`a = x', `b = 1/y' と見ればマッチできそうですが)。 理由のひとつは効率のためで、 別の理由は、加算と減算は数学的にほとんど同じ演算であるのに対し、 乗算, 除算, 整数べき乗を別々に取扱うことがしばしば好ましいからです。

さらに微妙なのが規則集合です。

[ f(a) + f(b) := f(a + b),  -f(a) := f(-a) ]

これを `f(x) - f(y)' にマッチさせるとします。 あなたは、Calc がこの減算を `f(x) + (-f(y))' と見なして、 そして上記の2つの規則を次々に適用すると考えるかも知れませんが、 実際はそうなりません。 なぜなら、Calc は(第1の規則のような) `+' に関する規則を考察をするとき、 他のことは考えられないからです。 それで Calc は、 `f(x) + (-f(y))' はメタ変数をどう割当てても `f(a) + f(b)' に マッチしない事を確かめた後、 次に `f(x) - f(y)' はどうしても `-f(a)' にマッチしないと 知ることになります。 Calc は一度にひとつの規則しか適用できないので、 この規則集合では `f(x) - f(y)' を書替えることができません。 明示的に `f(a) - f(b)' の規則を追加してやらねばなりません。

他にもパターンができないこととして、複素数の分解があります。 パターン `myconj(a + b i) := a - b i' は、 特別な定数 `i' を含む式(例えば `3 - 4 i')としては正しいのですが、 `(3, -4)' のような現実の複素数にはマッチしません。 上記の複素数向け規則は例えば次のように書きます。

myconj(a)  :=  re(a) - im(a) (0,1)  :: im(a) != 0

(reim 関数は特殊定数 `i' の性質を判っているので、 この規則は `3 - 4 i' にも作用します。 実際、この規則は `im(a) != 0' 条件が付いていない方が良いでしょう。 もし `im(a) = 0' であっても、 規則の右辺は実数の共役として正しい答を与えるからです。)

パターン中でオプショナル引数(任意に省略可能な引数)を指定することもできます。 次の規則

opt(a) x + opt(b) (x^opt(c) + opt(d))  :=  f(a, b, c, d)

は、次の式にマッチします。

5 (x^2 - 4) + 3 x

上の例はかなり直接的ですが、次のような項の少ない式にもマッチします。

x + x^2,    2(x + 1) - x,    x + x

結果はそれぞれ次のとおりです。

f(1, 1, 2, 0),   f(-1, 2, 1, 1),   f(1, 1, 1, 0)

(あとの2例は、 m O によってデフォルト簡単化を止めておかないと入力できません。)

和を構成するオプション項のデフォルト値はゼロです。 乗算, べき乗, 分母などのオプション項のデフォルト値は1です。 また、`-x'`a = -1' として `opt(a) b' にマッチします。

特に、分配法則は

opt(a) x + opt(b) x  :=  (a + b) x

このように洗練されると、 例えば `a x - x'`(a - 1) x' に変換できるようになります。

パターン `opt(a) + opt(b) x' は、 `x' について線形な式のほとんどにマッチします。 linislin 関数も、 書替え条件として線型性をテストするのに使えます。論理演算 参照 。 これらの関数は、書替え規則中で使うにはあまり便利ではありませんが、 それらはより多くの種類の式を線形であると認識します。 lin`x/z'b = 1/z の状態の線形と見なしますが、 これは先のパターンにはマッチしません。先のパターンは割り算ではなく、 掛け算を呼出すからです。

もうひとつの例として、 `sin(x)^2 + cos(x)^2' を 1 に置換える明白な規則を考えます。

sin(x)^2 + cos(x)^2  :=  1

これでは、サインとコサインに同じ係数が掛けられた場合に見逃してしまいます。 次のは、もっと成功した例です。

opt(a) sin(x)^2 + opt(a) cos(x)^2  :=  a

注意: この規則は `sin(x)^2 + 6 cos(x)^2' にはマッチしません。 なぜなら、ひとつの a が 1 にマッチし、 もうひとつは 6 にマッチすることになってしまうので 実際にはマッチしません。

Calc は次のように、自動的に規則を変換します。

f(x-1, x)  :=  g(x)

は、次のように変換されます。

f(temp, x)  :=  g(x)  :: temp = x-1

(ここで temp は新しく考案されたメタ変数で、実際には名前を持ちません)。 この修正された規則は、`6' が見かけ上 `x-1' と似ていなくとも、 `f(6, 7)' にうまくマッチします。 `temp'`x' をそれぞれ 6 と 7 に関連づけ、 次に、それらが 1 だけ違うことを確認します。

しかしながら、Calc は規則を解釈するときに(xについて)式を解くことはできません。 次の規則を見てください。

f(x-1, x+1)  :=  g(x)

この規則はうまく働きません。 というのは、 `f(a - 1 + b, a + 1 + b)' にはマッチするけれども、 `f(6, 8)' にはマッチしません。 少なくとも1個のメタ変数が文字的マッチングによって見つからなければ、 Calc には解釈できません。 変数が「単独で(1カ所に)」出現する場合、 Calc は文字マッチングを使ってうまく解釈できるのですが、この例は違います。 この例では、calc は仕方なく規則を修正して `f(x-1, temp) := g(x) :: temp = x+1' としますが、 `x-1' 項が対応するためには ターゲット式中に実際の「何か - 1」が無ければなりません。

うまい書き方は `f(x, x+2) := g(x+1)' です。 次節で説明する let 表記を使うと、これをもっとオリジナルに似せて書けます。

f(xm1, x+1)  :=  g(x)  :: let(x := xm1+1)

Calc はこの書替えや条件付けを、 「@定数か既にマッチしたメタ変数だけに対して A下記リストに挙げる関数群だけが作用しているサブパターン」 のすべてに対して実施します。 関数呼出しを見つけたら、Calc は注意深くその引数をマッチングします。 関数呼出しがネストされた引数よりも、 単なる変数からなる引数を優先してマッチングするので、 `f(x-1, x)' のような、 孤立した `x' より前に `x-1' がくるパターンであっても 条件付けできます。

+ - * / \ % ^  abs sign  round rounde roundu trunc floor ceil
max min  re im conj arg

関数呼出しの周りを plain マーカーで囲むことによって、 本節で解説した全ての特殊処理を抑制できます。 このマーカーは、その引数となる文字的マッチした関数の 交換性、結合性、否定、条件付けを考慮の対象から外します。 plain を使うと、ターゲット式の「ウラ構造」が垣間見えます。 次の例を見てください。

plain(a - a b)  :=  f(a, b)

これは文字上の引き算にしかマッチしません。 しかしながら、plain マーカーはその引数の引数には影響しません。 この例では、`a b' サブパターンがマッチングするとき、 交換性や結合性は依然として考慮されますから、上の規則は `x - x y' と同じく `x - y x' にもマッチします。 さらになお、

plain(a - plain(a b))  :=  f(a, b)

ここまでやると、完全に厳密なパターンマッチングを行います。

これに対して、quote マーカーは 「関数名だけでなく引数も文字通りに同じでなければならない」ことを意味します。 上のパターンは `x - x y' にマッチしますが、

quote(a - a b)  :=  f(a, b)

これは唯一 `a - a b' にしかマッチしません。しかも、

quote(a - quote(a b))  :=  f(a, b)

としてしまったら、 これは `a - quote(a b)' にしかマッチしませんからご注意を!

メタ変数を規則の右辺に書替える際、相当量の代数演算が行われます。 例えば、

a + f(b)  :=  f(a + b)

これは `f(x) - y' にマッチングして、 文字上は `f((-y) + x)' を生成しますが、 書替え機構がこの右辺を自動的に簡単化して `f(x - y)' とします。 (もちろん、デフォルト簡単化機構が同じ事を実行しますから、 デフォルト簡単化を切っていなければこの特別な簡単化は気付きません。) この書替えは、メタ変数が「負に見える」式に展開した場合にのみ行われます。 この簡単化が望ましくなければ、右辺に plain マーカーを使うことができます。

a + f(b)  :=  f(plain(a + b))

この例では、依然としてパターンマッチエンジンが知りうる限りの代数を 使うことを許していますが、右辺は常に `f((-y) + x)' のような 文字上の足し算に簡単化されます。


Go to the first, previous, next, last section, table of contents.     利用度数