10数式データの扱い

本章は，シンボリックな計算を扱うためのEgisonの機能を紹介する．

10.1数式データの内部表現

数式は組み込みデータ型としてEgison処理系内部でHaskellのデータ型を用いて直接実装されている．本節は，数式データを表現するこの内部のデータ構造について説明する．

数式データは，分母と分子の両方に積和標準形の多項式をとる分数として表現されている．そのため，たとえば，分母が多項式である分数同士の足し算の結果は，通分されて一つの分数にまとめられる．

declare symbol x, y, a, b, c

a / (b + 1) + x / (y + 1)
-- (b x + a y + x + a) / (b y + y + b + 1)

多項式は，項のリストからなるデータとして表現されている．そして，項は係数と，因子と冪指数の連想リストからなるデータとして表現されている．たとえば，3 * x^2 * sqrt 2という項は，係数として3，連想リストとして[(x, 2), (sqrt 2, 1)]をもつ．冪指数には負の整数もとることができる．つまり，Egisonの多項式は，ローラン多項式である．分母がひとつの項だけからなる分数は，分数としては保持されず，負の冪指数を使って項のなかに取り込まれる．

a / b + x / y -- x y^-1 + a b^-1

因子には，シンボルのほかに，9.2節で紹介したシンボリックな関数適用，10.2節で紹介するクオートされた式，第13章で解説する関数シンボルをとることができる．シンボルは，名前の文字列と添字のリストからなる．添字については，テンソルについて解説する第12章で説明する．

この内部構造は，Egisonライブラリで定義されているmathValueマッチャーを使ったパターンマッチで分解できる．たとえば，多項式を項のリストに分解できる．

match (x - sqrt 2) as mathValue with
  | poly $ts -> ts
-- [x, - 'sqrt 2]

数式に対するパターンは，10.6節で詳しく紹介する．また，同じ数式を複数の異なる内部構造（たとえば，平坦な多項式と入れ子の多項式）で表現し，型注釈でそれを選ぶこともできる．これについては第11章で解説する．

数は複雑なデータ型である．自然数までであれば代数的データ型としてエレガントに定義できる．しかし，自然数の足し算の逆関数引き算を考えると，負の数という概念が得られる．さらに足し算を繰り返すことによって得られる掛け算の逆を考えると，有理数という概念が得られる．さらに掛け算を繰り返すことによって得られるべき乗という操作の逆を考えると，平方根や虚数，それらを含む代数的数の概念が得られる．

10.2バッククオート（`）による式展開の制御

Egisonは数式を自動で積和標準形に展開すると9.1節で述べたが，この展開をバッククオート（`）により制御することができる．バッククオートに続く式は，ひとつのシンボルのように扱われる．

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

`(x + 1) + `(x + 1)
--  2 * `(x + 1)

`(x + 1) + (x + 1)
-- x + `(x + 1) + 1

バッククオートが役に立つのは，式を展開させたくないときである．多項式の分数の約分そのものは，9.3節で述べたように多項式GCDにより自動でおこなわれるが，入力も結果も積和標準形に展開される．

(x + 1)^2 / (x + 1) -- x + 1
(x^2 - y^2) / (x - y) -- y + x

バッククオートで因数分解された形を保っておけば，式は展開を経ずに約分され，結果も因数分解された形のまま得られる．

`(x + y)^2 / `(x + y) -- `(y + x)
`(x - y) * `(x + y) / `(x - y) -- `(y + x)

バッククオートによりクオートされた式は，Egison内部の数式データのなかで，シンボルと同列の因子として扱われる．上記の`(x + 1)^2が展開されずにひとつの因子の冪として保持されるのは，このためである．

10.3シングルクオート（`'`）による関数適用の制御

定義済みの関数の適用について，関数適用を評価せずに，シンボリックな結果を返したいことがある．たとえば，sqrt関数については9.2節でみたように以下のように動作してほしい．

declare symbol x, a

sqrt 4 -- 2
sqrt x -- 'sqrt x

このような動作を実現するために，Egisonには組み込み構文としてシングルクオート（'）が用意されている．シングルクオートには関数が続き，たとえその関数が定義済みであったとしても，その適用を評価せずシンボリックな関数適用として返す．

def f (x: MathValue) : MathValue := x + 1

f a -- a + 1
'f a -- 'f a

シンボリックな関数適用は，出力でも先頭にシングルクオートを付けて表示される．シングルクオートは，11.3節で紹介したdeclare apply文の本体で，これ以上簡約できない入力に対してシンボリックな値を返すために，sqrtや三角関数sin・cosなどの定義のなかで使われている．

10.4規則の適用を抑制するクオート（`'( )`）

シングルクオートを括弧で囲った式に前置すると，その式はdeclare ruleによる簡約規則（第11章11.1節）を適用せずに構築される．積和標準形への展開や同類項の整理といった構造的な正規化はおこなわれる．

declare symbol x, `$\theta$`

w^2 + w + 1 -- 0
'(w^2 + w + 1) -- w^2 + w + 1

(sin `$\theta$`)^2 + (cos `$\theta$`)^2 - 1 -- 0
'((sin `$\theta$`)^2 + (cos `$\theta$`)^2 - 1) -- 'sin `$\theta$`^2 + 'cos `$\theta$`^2 - 1

'(2 * x + x) -- 3 * x
'((x + 1)^2) -- x^2 + 2 * x + 1

このクオートが必要になる典型は，簡約規則の対象になる関係式そのものをデータとして扱いたいときである．たとえば第11章11.2節のpolyNFにイデアルの生成元を渡すとき，ピタゴラスの関係式を素の式で書くと，構築の時点で既存の自動規則により0に簡約されてしまう． '( )で囲えば，関係式は式のまま生き残る．

これで3種類のクオートが出そろった．バッククオート`は式を1つの原子に固めて展開を止め（10.2節），シングルクオート'fは関数適用の評価を止め（10.3節），'( )は簡約規則の適用を止める．それぞれ，数式の構造・関数適用・等式理論という異なる層を凍結するクオートである．

10.5`withSymbols`式によるローカルシンボルの宣言

declare symbol文で宣言されるシンボルは大域的である．一時的にシンボルを使いたいだけの場合のために，ローカルシンボルを宣言するための構文としてwithSymbols式がEgisonには用意されている． withSymbols式は，第一引数に変数のリストをとり，これらの変数は第二引数の式の評価時にシンボルとして扱われる．たとえその変数が定義済みであったとしても，withSymbols式の内部ではシンボルとして扱われる．

def k : Integer := 10

k -- 10
withSymbols [k] k -- k
k + withSymbols [k] k -- k + 10

withSymbols式で宣言されたローカルなシンボルは，declare symbol文で宣言されたグローバルなシンボルとは独立したシンボルとして処理される．以下の2つのjは同じ名前で表示されるが，別のシンボルであるため，2 * jのようにまとめられない．

declare symbol j

j + withSymbols [j] j -- j + j

10.6数式データに対するパターンマッチ

本節は，数式データに対して用意されているパターンを紹介する．数式に対するマッチャーmathValueはEgisonライブラリに実装されている． mathValueの定義はlib/math/expression.egiで確認できる．また数式に対するパターンを，より数式に近いかたちで記述するためにいくつかの糖衣構文が組み込みで実装されている．本節では，これらの糖衣構文も紹介する．数式に対するパターンマッチは，9.5節で実演されている．パターンの具体的な使用例として，9.5節のプログラムを参照してほしい．

10.6.1因子に対するパターンマッチ

因子に対するパターンコンストラクタには，symbol・apply1からapply4・quote・funcがある． symbolはシンボルに，apply1からapply4は9.2節で紹介したシンボリックな関数適用に，quoteは10.2節で紹介したバッククオートされた式に，funcは第13章で解説する関数シンボルと呼ばれるオブジェクトにパターンマッチするためのパターンコンストラクタである．

symbolパターンコンストラクタの第一引数はシンボルの名前の文字列に，第二引数は添字のリストにパターンマッチする．添字については，テンソルについて解説する第12章で改めて紹介する．

match x as mathValue with
  | symbol $s _ -> s
-- "x"

シンボルに対してはsymbolパターンコンストラクタを使ってパターンマッチすることもできるが，実際には値パターンを使ってパターンマッチすることが多い．

match x as mathValue with
  | #x -> "Matched"
  | _ -> "Not matched"
-- "Matched"

シンボリックな関数適用に対しては，引数の個数に応じてapply1からapply4のパターンコンストラクタを使う．第一引数は関数自身に，残りの引数はそれぞれの引数の数式にパターンマッチする．関数自身に対しては，#sqrtのような値パターンがよく使われる．

match (sqrt x) as mathValue with
  | apply1 #sqrt $g -> g
-- x

quoteパターンコンストラクタは引数に数式に対するパターンをとる．このパターンはmathValueマッチャーを使ってクオートの中身の式とパターンマッチされる．

match `(x + 1) as mathValue with
  | quote $e -> e
-- x + 1

10.6.2項に対するパターンマッチ

項に対するパターンマッチには，termパターンコンストラクタを使う． termパターンコンストラクタの第一引数は係数に，第二引数は因子と冪指数の連想リストにパターンマッチする．因子の連想リストのパターンマッチには，6.7節で紹介したassocMultisetマッチャーが使われる．

matchAll 3 * x^2 * y as mathValue with
  | term $a (($x, $n) :: $xs) -> (a, x, n, xs)
-- [(3, x, 2, [(y, 1)]), (3, y, 1, [(x, 2)])]

termパターンコンストラクタには，より数式に近いパターンを記述するための糖衣構文がある．以下の1つ目のパターンの$xは，x^2のように冪を含めた因子にマッチし，$xsは残りの因子の積にマッチする． 2つ目のパターンのように，冪指数に対するパターンを^に続けて書くこともできる．

matchAll 3 * x^2 * y as mathValue with
  | $a * $x * $xs -> (a, x, xs)
-- [(3, x^2, y), (3, y, x^2)]

matchAll 3 * x^2 * y as mathValue with
  | $a * $x^#2 * $xs -> (a, x, xs)
-- [(3, x, y)]

10.6.3多項式に対するパターンマッチ

多項式に対するパターンマッチには，polyパターンコンストラクタを使う． polyパターンコンストラクタは引数に項のリストにマッチするパターンをとる．

matchAll x + y + 1 as mathValue with
  | poly ($x :: $xs) -> (x, xs)
-- [(y, [x, 1]), (x, [y, 1]), (1, [y, x])]

polyパターンコンストラクタにも，より数式に近いパターンを記述するための糖衣構文がある．

matchAll x + y + 1 as mathValue with
  | $x + $xs -> (x, xs)
-- [(y, x + 1), (x, y + 1), (1, y + x)]

10.6.4有理式に対するパターンマッチ

有理式に対するパターンマッチには，fracパターンコンストラクタを使う． fracパターンコンストラクタの第一引数は分子の多項式に，第二引数は分母の多項式にパターンマッチする．

matchAll (a + b) / (c + 1) as mathValue with
  | frac $x $y -> (x, y)
-- [(b + a, c + 1)]

なお，10.1節で述べたように，分母がひとつの項だけからなる分数は負の冪をもつ項として表現されるため，fracパターンにはマッチしない．

fracパターンコンストラクタにも，より数式に近いパターンを記述するための糖衣構文がある．

matchAll (a + b) / (c + 1) as mathValue with
  | $x / $y -> (x, y)
-- [(b + a, c + 1)]