12テンソル計算
Egisonにはテンソル計算を便利に記述するために開発された機能が実装されている. 本章はこれらの機能を紹介していく.
12.1テンソルとは
テンソルとは,ベクトルや行列を一般化したものである. ベクトルは一階のテンソル,行列は二階のテンソルである. ベクトルは一次元配列,行列は二次元配列としてプログラムでは表現されることが多い. \(n\)階のテンソルは,\(n\)次元配列により表現される.
以下はそれぞれベクトル,行列,\(2\)階のテンソルの例を数式で表現したものである.
上記の数式はEgisonでは下記のように表現される. Egisonではテンソルの成分を[| |]で囲むことにより,テンソルを表現する. 行列はベクトルのベクトルとして,\(2\)階のテンソルは行列のベクトルとして表現される. これはC言語などの多次元配列の表記法に似ている.
[| a_1, a_2, a_3 |]
[| [| a_11, a_12, a_13 |],
[| a_21, a_22, a_23 |] |]
[| [| [| a_111, a_112, a_113 |],
[| a_121, a_122, a_123 |] |],
[| [| a_211, a_212, a_213 |],
[| a_221, a_222, a_223 |] |],
[| [| a_311, a_312, a_313 |],
[| a_321, a_322, a_323 |] |] |]
12.2テンソルの添字記法
テンソル計算は,ベクトルについてのテンソル積・アダマール積・内積の組み合わせでほとんど表現できる. テンソル積は,ベクトルのすべての成分の組み合わせからなる行列を返す. アダマール積は,対応する成分同士のみからなるベクトルを返す. 内積は,アダマール積の結果の成分を足し合わせた結果のスカラー値を返す.
たとえば,行列\(A\)と行列\(B\)の掛け算は,\(A\)の行と\(B\)の列についてはテンソル積,\(A\)の列と\(B\)の行については内積をとる演算と解釈できる.
ベクトルについては,掛け算の方法は,テンソル積・アダマール積・内積の3つだけだが,行列や行列よりさらに高階なテンソルとなると掛け算の方法が無数にある. これらの掛け算のすべてに名前をつけるのは大変である. そのため,数学者はシンボリックな添字をテンソルに付加し,その添字をパラメーターにしてこれらの掛け算を表現する. たとえば,それぞれのベクトルに異なるシンボルが付加されている場合はテンソル積に,それぞれのベクトルの同じ位置に同じシンボルが付加されている場合はアダマール積に,それぞれのベクトルの上下に同じシンボルが付加されている場合は内積になる. 添字には上添字と下添字の二種類がある. この位置関係によってアダマール積となるか内積となるか区別する. このようにシンボリックな添字を使って,テンソルのかけあわせ方を指定する記法は,添字記法と呼ばれている. 下記の数式はEgisonで9.6節で示したプログラムで表現できる.
行列のかけ算も添字記法をつかってうまく表現できる. 内積をとるAの列とBの行について,それぞれ上下を逆にし,同じシンボルにすれば,行列の掛け算は表現できる.
12.3添字記法をプログラミングに導入するためのアイデア
添字記法のプログラミングへの導入が難しい理由は,演算子ごとにシンボリックな添字のルールが異なることにある. 特にテンソルの足し算と掛け算では,添字のルールが異なる. 例を紹介する. \(u\)と\(v\)をそれぞれベクトルとする.
- \(u_{i} + v_{i}\)はベクトルを返す.対して,\(u_{i} v_{i}\)は無効な式である.
(\(u_{i} v_{i}\)は上下添字を自由に入れ替えることが可能なユークリッド空間では内積を返す.しかし,このような例外はここでは考えない.)
- \(u^{i} + v_{i}\)は無効である.対して,\(u^{i} v_{i}\)は内積を返す.
- \(u_{i} + v_{j}\)は無効である.対して,\(u_{i} v_{j}\)はテンソル積を返す.
このように演算子ごとに異なるシンボリックな添字のルールがある. そのため,テンソルを扱う関数を定義するたびに,シンボリックな添字のルールを指定する必要がある. これはわずらわしい作業である. それだけではなく,添字ルールを記述するための新しい構文が必要になる場合もある. このような新しい構文はプログラミング言語を複雑にする.
Egisonは,シンボリックな添字のルールを簡略化することによって,この問題を解決する. 添字のルールの簡略化によって,有効な数式の解釈は変わらない. ただし,無効であった数式が有効になる場合がある. 例えば,\(v_{i} + v_{j}\)は無効な式であったが,新しい添字ルールでは有効な式になる. テンソルの足し算についての簡略化された添字ルールを図12.3で示す. 添字ルールを緩めることによって,多くのテンソルについての演算をテンソルの足し算の変種として捉えることができるようになる. 例えば,テンソルの掛け算は,足し算と同じ形で成分を掛け合わせたあとに縮約(contraction)という追加の処理をする演算と捉えられる(図12.3). テンソルの縮約とは,同じシンボルの上添字と下添字があるときに,対角成分を足し合わせる操作のことをいう. このような見方をすると,テンソルについての関数を定義するときの添字ルールの記述をへらすことができる.
12.4スカラー仮引数とテンソル仮引数
テンソルの添字記法のプログラミングへの導入は,(i)型システムによるスカラー関数とテンソル関数の区別と,(ii)適切な添字の簡約ルールによってなされる. 本節からこれらの概念の解説を始める.
まず,型システムによるスカラー関数とテンソル関数の区別を説明する. Egisonでは,仮引数の型注釈により,関数がスカラー関数かテンソル関数かが決まる. 仮引数の型がTensor a型でない場合,その仮引数はスカラーとして扱われる. 仮引数の型がTensor a型である場合,その仮引数はテンソルとして扱われる. スカラーとして扱われる仮引数にテンソルが引数として与えられると,テンソルの成分ごとに関数の処理がマップされる. テンソルとして扱われる仮引数にテンソルが引数として与えられると,テンソルがそのまま仮引数に渡される. 以下の例では,型変数aがスカラー型と推論され,テンソルが渡されると成分ごとに処理がマップされる.
(\u v -> (u, v)) [| a, b |]_i [| x, y |]_j
-- [| [| (a, x), (a, y) |],
-- [| (b, x), (b, y) |] |]_i_j
一方,明示的にTensor型を指定した場合,テンソルがそのまま渡される.
(\(u: Tensor a) (v: Tensor a) -> (u, v)) [| a, b |]_i [| x, y |]_j
-- ([| a, b |]_i, [| x, y |]_j)
Egisonの型システムは,スカラー関数(scalar function)とテンソル関数(tensor function)という2種類の関数を区別する. スカラー関数は,テンソルを引数にとったとき,成分ごとに処理をマップする関数のことをいう. たとえば,“+”や,“-”,“*”,“/”,“\(\partial\)/\(\partial\)”はスカラー関数である. テンソル関数は,テンソルを引数にとったとき,テンソルをテンソルとしてそのまま処理する関数のことをいう. たとえば,行列式を計算する関数や,テンソル同士のかけ算のための関数は,テンソルの成分ごとに自動でマップされては記述できないため,テンソル関数として定義する必要がある. 関数がスカラー関数かテンソル関数かは型注釈によって決まる. 仮引数の型がTensor a型でない場合,テンソルが引数として渡されると自動的に成分ごとに処理がマップされる(スカラー関数). 仮引数の型がTensor a型である場合,テンソルはテンソルとしてそのまま渡される(テンソル関数). 図12.4と図12.4でスカラー関数とテンソル関数の定義の例を説明する.
def min (x: a) (y: a) : a := if x < y then x else y
min関数の定義(型注釈により,任意の比較可能な型aに対して動作することを示している)
\(min(\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i}, \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{j}) = \begin{pmatrix} min(1,10) & min(1,20) & min(1,30) \\ min(2,10) & min(2,20) & min(2,30) \\ min(3,10) & min(3,20) & min(3,30) \\ \end{pmatrix}_{ij} = \begin{pmatrix} 1 & 1 & 1 \\ 2 & 2 & 2 \\ 3 & 3 & 3 \\ \end{pmatrix}_{ij}\)
}
min関数の適用
\(min(\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i}, \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{i}) = \begin{pmatrix} min(1,10) & min(1,20) & min(1,30) \\ min(2,10) & min(2,20) & min(2,30) \\ min(3,10) & min(3,20) & min(3,30) \\ \end{pmatrix}_{ii} = \begin{pmatrix} min(1,10) \\ min(2,20) \\ min(3,30) \end{pmatrix}_{i} = \begin{pmatrix} 1 \\ 2 \\ 3 \end{pmatrix}_{i}\)
}
min関数の適用
min関数の定義と適用例
図12.4は,スカラー関数の例として,min関数の定義とその適用例を紹介している. 本体で<を使っているため仮引数の型は{Ord a}という制約つきの型変数と推論され,Tensor型はこの制約を満たせない(スカラー仮引数 — 正確な判定基準は12.10節). そのため,テンソルが引数として渡された場合,自動的に成分ごとに関数が適用される. 成分ごとに関数が適用された結果,図12.4のように関数はテンソル積と同じ形で適用される. テンソルの添字の簡約ルールはシンプルである. 図12.4のようにスカラー関数を適用した結果,同じシンボルの添字が2つ以上付加されたテンソルが生成された場合,その対角成分からなるテンソルに簡約されるというルールだけである. 添字簡約のルールの詳しい仕様は次節で論じる.
def (.) (t1: Tensor a) (t2: Tensor a) : Tensor a := contractWith (+) (t1 * t2)
.”関数の定義(型注釈により,テンソルを受け取りテンソルを返すことを示している)
\(\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}^{i} \cdot \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{i} = contractWith(+, \begin{pmatrix} 10 & 20 & 30 \\ 20 & 40 & 60 \\ 30 & 60 & 90 \\ \end{pmatrix}^{i}_{\;i}) = 10 + 40 + 90 = 140\)
\(\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i} \cdot \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{j} = contractWith(+, \begin{pmatrix} 10 & 20 & 30 \\ 20 & 40 & 60 \\ 30 & 60 & 90 \\ \end{pmatrix}_{ij})
= \begin{pmatrix} 10 & 20 & 30 \\ 20 & 40 & 60 \\ 30 & 60 & 90 \\ \end{pmatrix}_{ij}\)
}
.”関数の適用
.”関数の定義と適用例
図12.4は,テンソル関数の例として,テンソルのかけ算をする“.”関数の定義と適用例を紹介している. 仮引数の型がTensor a型であるため,テンソルが引数として渡された場合,テンソルとしてそのまま渡される. 図12.4のように,Egisonは上添字と下添字の両方を組み込みでサポートしている. 上添字と下添字で同じシンボルが使われていた場合は,関数contractWithを使って縮約することができる.
上添字は“~”,下添字は“_”を使ってプログラム上で表現される. たとえば,図12.4の一つ目の計算例は以下のようにEgisonで表現される.
[| 1, 2, 3 |]~i . [| 10, 20, 30 |]_i
-- 140
12.5三種類の添字
テンソルの添字記法を扱うためにEgisonには三種類の添字が導入されている. 最初の二つは前節で紹介した上添字と下添字で~と_で表現される. 三つ目は上下添字と呼ばれる添字で~_で表現される. 上下添字は,同一のシンボルをもつ上添字と下添字をもつテンソルに対してスカラー関数を適用した際に現れる.
[| 1 2 3 |]_i * [| 10 20 30 |]_i -- [| 10, 40, 90 |]_i
[| 1 2 3 |]~i * [| 10 20 30 |]~i -- [| 10, 40, 90 |]~i
[| 1 2 3 |]~i * [| 10 20 30 |]_i -- [| 10, 40, 90 |]~_i
前節でも登場したcontractWith関数は上下添字について対角成分をリストに変換し第一引数の関数で畳み込む.
contractWith (+) [| 10, 40, 90 |]_i -- [| 10, 40, 90 |]_i
contractWith (+) [| 10, 40, 90 |]~i -- [| 10, 40, 90 |]~i
contractWith (+) [| 10, 40, 90 |]~_i -- 130
contractWith関数は組み込み関数contractを使って定義されたライブラリ関数である. 組み込み関数contractは上下添字の付加されたスロットの成分のリストを返す.
contract [| 1, 2, 3 |]~_i -- [1, 2, 3]
contract [| [| 11, 12 |], [| 21, 22 |] |]~_i_j -- [[| 11, 12 |]_j, [| 21, 22 |]_j]
contract [| [| 11, 12 |], [| 21, 22 |] |]_i~_j -- [[| 11, 21 |]_j, [| 12, 22 |]_i]
contract [| [| 11, 12 |], [| 21, 22 |] |]~_i~_j -- [11, 12, 21, 22]
12.6添字の簡約規則
E({A, xs}) =
if e(xs) = [] then
{A, xs})
elsif e(xs) = [{k,j}, …] & p(k,xs) = p(j,xs) then
E({diag(k, j, A), remove(j, xs))
elsif e(xs) = [{k,j}, …] & p(k,xs) != p(j,xs) then
E({diag(k, j, A), update(k, 0, remove(j, xs)))
本節は,添字の簡約ルールを擬似コードを使って説明する. 12.4節で説明したように,テンソルをスカラー関数を適用したときは常にテンソル積のかたちで成分ごとに処理がマップされるため,ひとつのテンソルについての簡約ルールのみを定義すればよい.
図12.6は添字簡約をする擬似コードである. E(A,xs)は添字付きテンソルの簡約をする関数である. Aはテンソルの成分からなる配列であり,xsはAに付加されている添字のリストを表す. たとえば,E(A,xs)は添字として“~i_j_i”を持つテンソルに対して以下のように動作する. 上添字,下添字,上下添字を表すフラグとしてそれぞれ1,-1,0を使っている.
E({[|[|[|1,2|],[|3,4|]|]
,[|[|5,6|],[|7,8|]|]|]
,[{i,1}, {j,-1}, {i,-1}]}) =
{[|[|1,3|],[|6,8|]|], [{i,0}, {j,-1}]}
擬似コード中で使われている補助関数を説明する. e(xs)はxs中に現れる同一のシンボルからなる添字のペアを見つける関数である. diag(k, j, A)はk番目とj番目のスロットについてAの対角成分からなるテンソルを計算する関数である. remove(k, xs)はリストxsからk番目の要素を取りのぞく関数である. p(k, xs)は連想リストxsからk番目の値を取得する関数である. update(k, p, xs)は連想リストxsのk番目の値をpに更新する関数である. これらの補助関数は以下のように動作する.
e([{i, 1}, {j, -1}, {i, -1}]) = [{1,3}]
diag(1, 2, [|[|11,12|],[|21,22|]|]) = [|11,22|]
p(2, [{i, 1}, {j, -1}]) = -1
remove(2, [{i, 1}, {j, -1}]) = [{i, 1}]
update(2, 0, [{i, 1}, {j, -1}]) = [{i, 1}, {j, 0}]
12.7古典的な添字記法との違い — 統一された添字規則
古典的なテンソルの添字記法では,演算ごとに添字の使い方の正しさの条件が異なる. たとえば,\(u_i + v_i\)は正しいが\(u_i + v_j\)は不正であり, アインシュタインの縮約規約では\(u^i v_i\)は縮約を表すが,同じ変位が繰り返される\(u_i v_i\)は不正である. Egisonはこの規則を単純化して統一している. すべての演算をひとつの意味論 — 成分ごとのリフト(tensorMap挿入)と,そのあとの添字簡約 — で扱う. その結果,古典的な記法で正しい式の意味はそのまま保たれ,古典的には不正だった式にも一貫した意味が与えられる.
declare symbol i, j
[|1,2,3|]_i + [|10,20,30|]_j
-- [| [| 11, 21, 31 |], [| 12, 22, 32 |], [| 13, 23, 33 |] |]_i_j
[|1,2,3|]_i + [|10,20,30|]_i
-- [| 11, 22, 33 |]_i
[|1,2,3|]_i * [|10,20,30|]_j
-- [| [| 10, 20, 30 |], [| 20, 40, 60 |], [| 30, 60, 90 |] |]_i_j
[|1,2,3|]_i * [|10,20,30|]_i
-- [| 10, 40, 90 |]_i
[|1,2,3|]~i . [|10,20,30|]_i
-- 140
+と*が完全に同じ規則に従っていることに注目してほしい. 添字が異なれば結果はテンソル積のかたち(すべての組合せ)になり, 同じ下添字が繰り返されれば対角成分の抽出になる(*の場合はアダマール積に一致する). 古典記法で不正だった\(u_i + v_j\)は「和のすべての組合せ」という自然な意味をもつテンソルになる. 縮約は,上添字と下添字のペアが.のようなテンソル関数(12.8節)に渡されたときに起こる.
なお,同じ添字のケースでは,リフト直後にはすべての組合せをもつ正方配列が中間形として現れるが, 添字簡約(12.6節)が即座に対角を取り出すため,ユーザーが観察するのは簡約後の値だけである.
12.8テンソル関数の適用
添字付きのテンソルがテンソル関数に渡されるとき,そのテンソルの添字ごとテンソル関数に適用される. 図12.4で定義した“.”関数でこの挙動を確認する. 図12.4では,“.”関数を適用をしたときなされる展開が段階的に表示されている. contractWithの内側に添字付きのテンソルがあらわれるが,これはテンソルの添字ごとテンソル関数に渡されることで可能になっている. この挙動のおかげで以下のようにテンソル関数についてテンソルの添字記法を使って関数適用できるようになっている.
[|1,2,3|]~i . [|10,20,30|]_i -- 140
[|1,2,3|]_i . [|10,20,30|]_j -- [|[|10,20,30|],[|20,40,60|],[|30,60,90|]|]_i_j
[|1,2,3|]_i . [|10,20,30|]_i -- [|10,40,90|]_i
テンソル関数の中で引数として渡されたテンソルに追加で添字を付加したいことがある. 追加で新しい添字を付加するためには,以下のように...をテンソルと添字の間に挟めば良い. この機能は,12.14節で紹介するsubrefsとsuprefsという組み込み関数を使った糖衣構文として実装されている. この機能の使用例は第14章で紹介する.
A..._i_j
12.9省略された添字の補完
添字が省略されたテンソルが関数に適用された場合,Egisonは自動で添字を補完する. 本節はこの補完の規則を説明する.
以下,A,Bを\(2\)階のテンソル,つまり行列であるとする. 添字を省略した状態でスカラー関数にA,Bを同時に適用すると,下記のように同じ組み合わせの添字が補完される.
A + B -- A_t1_t2 + B_t1_t2
関数適用の前に“!”が付加されていた場合は,下記のように違う添字が補完される.
A !+ B -- A_t1_t2 + B_t3_t4
添字が省略されたテンソルが,テンソル関数に適用された場合は,補完はおこなわれない.
上記の添字の補完規則には実は必然性がある. 添字が省略された場合の添字補完規則を上記のように設定すると,微分形式のための演算子を簡潔に定義できる. 微分形式の演算子の定義の具体例は,第14章で紹介する. あとで第14章でも述べるように,“!”が使われる必要があるのは,微分形式の演算子の定義の中だけになる. そのため,基本的にユーザーは“!”については意識しなくてよい.
12.10tensorMap自動挿入の仕組み
本節は,型システムによるtensorMap自動挿入の仕組みについて説明する.
12.10.1基本原理
Egisonの型システムは,関数適用ごとに,仮引数の型が(型クラス制約まで考慮したうえで)Tensor a型に実体化できるかを判定する. 実体化できる仮引数をテンソル互換(tensor-compatible)な仮引数と呼ぶ. tensorMapが挿入されるのは,つぎの2つの条件がそろったときである:
- 仮引数がテンソル互換でない(=スカラー仮引数である)
- 実引数の型が
Tensor a型である
tensorMapは,第一引数の関数を第二引数のテンソルの成分ごとに適用してテンソルを返す組み込み関数である.
仮引数の型がテンソル互換かどうかは,つぎのように定まる:
Integerのような具体的なスカラー型 — テンソル互換でない(スカラー仮引数)- 明示的な
Tensor a型 — テンソル互換 - 型変数 — 付いている型クラス制約のすべてを
Tensor型が満たせるかで決まる.制約がなければ常にテンソル互換である.
{Eq a}のaもテンソル互換である(ライブラリにinstance {Eq a} Eq (Tensor a)があるため). 一方,{Ord a}や{AddSemigroup a}のaはテンソル互換でない(Tensor型はこれらのクラスのインスタンスをもたない).
この分類は関数の主型(推論された型)だけから決まるため,どこにtensorMapが挿入されるかは決定的であり,型注釈は挿入の制御のためには不要である. また,判定はHindley--Milner型推論の範囲に収まっており,添字の情報を型に持ち上げることも,依存型も必要としない.
12.10.2具体例
図12.4で定義したmin関数を使って挙動を確認する.
def min (x: a) (y: a) : a := if x < y then x else y
min [|1,2,3|]_i [|10,20,30|]_j
-- Internally transformed to:
-- tensorMap (\xi -> tensorMap (\yi -> min xi yi) [|10,20,30|]_j) [|1,2,3|]_i
-- Result: [|[|1,1,1|],[|2,2,2|],[|3,3,3|]|]_i_j
min [|1,2,3|]_i [|10,20,30|]_i
-- Result: [|1,2,3|]_i
min関数の本体は<を使っているため,仮引数の型は{Ord a}という制約つきの型変数aと推論される. Tensor型はOrdクラスのインスタンスではないため,aをTensor型に実体化することはできない. つまりminの仮引数はスカラー仮引数であり,テンソルが渡されると自動的にtensorMapが挿入される. 型注釈をすべて省いてdef min x y := if x < y then x else yと書いても,同じ型が推論されるので挙動は変わらない — リフトするかどうかは推論された主型だけに従う.
一つ目の式の結果のテンソルの添字が“_i_j”となっている. tensorMapは,第一引数の関数に第二引数のテンソルの成分を適用した結果がテンソルである場合,その結果のテンソルの添字をtensorMap全体の結果のテンソルの添字の末端に移動する. このために結果のテンソルの添字が“_i_j”となる. この仕組みがテンソルの添字記法を使ってスカラー関数を適用することを可能にしている.
12.10.3型変数のテンソル互換性
型変数の分類の分かれ目は,制約の有無そのものではなく,付いている制約をTensor型が満たせるかである. 制約のない型変数はどんな型にも — Tensor型にも — 実体化できるので,テンソル互換である. たとえば恒等関数にテンソルを渡しても,tensorMapは挿入されず,テンソルがそのまま通る.
def myId (x: a) : a := x
myId [|1,2,3|]_i -- [| 1, 2, 3 |]_i
テンソルを要素として運ぶ総称的な高階関数(リスト操作など)が期待どおり動くのは,この分類のおかげである.
制約が付いていても,Tensor型がそのクラスのインスタンスをもつならテンソル互換のままである. たとえば{Eq a}にはinstance {Eq a} Eq (Tensor a)があるため,等値比較はテンソル全体に対しておこなわれる(成分ごとにはリフトされない).
def eqTest {Eq a} (x: a) (y: a) : Bool := x == y
eqTest [|1,2|]_i [|1,2|]_i -- True
eqTest [|1,2|]_i [|1,3|]_i -- False
一方,Tensor型がインスタンスをもたないクラスの制約が付くと,スカラー仮引数になる.
def double {AddSemigroup a} (x: a) : a := x + x
double [|1,2,3|]_i
-- Since Tensor is not an instance of AddSemigroup,
-- tensorMap is automatically inserted:
-- tensorMap (\xi -> double xi) [|1,2,3|]_i
-- Result: [|2,4,6|]_i
AddSemigroup aという制約により,aはAddSemigroupクラスのインスタンスの範囲でしか実体化できない. Tensor型はそのインスタンスではないため,テンソルが渡されると自動的にtensorMapが挿入され,各成分(Integer型)に対してdouble関数が適用される.
12.10.4テンソル関数の場合
一方,仮引数の型が明示的にTensor a型である場合,tensorMapは挿入されない.
def (.) (t1: Tensor a) (t2: Tensor a) : Tensor a :=
contractWith (+) (t1 * t2)
[|1,2,3|]~i . [|10,20,30|]_i
-- tensorMap is not inserted; the tensor is passed as-is
-- Result: 140
12.10.5高階関数に渡される関数
高階関数の引数として渡される関数にも挿入は働く. このときtensorMapは関数の適用位置にではなく,関数引数そのものをイータ展開して挿入される. つまり,渡された関数fが\x -> tensorMap f xや\x y -> tensorMap2 f x yのようなラッパに変換され,成分ごとの適用はラッパの本体でおこなわれる.
def inc (x: Integer) : Integer := x + 1
map inc [[|1,2|]_i, [|10,20|]_i]
-- inc is eta-expanded to \x -> tensorMap inc x
-- Result: [[|2,3|]_i, [|11,21|]_i]
foldl1 (+) [[|1,2|]_i, [|10,20|]_i]
-- (+) is eta-expanded to \x y -> tensorMap2 (+) x y
-- Result: [|11,22|]_i
イータ展開が起こる条件は,関数引数のかたちによって異なる. 1引数のスカラー関数は,適用先が期待するコールバックの型にテンソルが現れる場合にイータ展開される (上のmapの例では,リストの要素がテンソルであることが型からわかる). 一方,2引数のスカラー関数は,型からテンソルが見えるかどうかによらず,例外なくtensorMap2版にイータ展開される. tensorMapとtensorMap2はスカラー値に対しては恒等に働くため,この無条件のラップは常に安全である. この設計のおかげで,foldlの累積器のように,計算の途中でスカラーからテンソルに変わる引数も正しく処理される.
foldl (+) 0 [[|1,2|]_i, [|10,20|]_i]
-- The accumulator starts as the scalar 0 and becomes
-- a tensor at the first addition
-- Result: [|11,22|]_i
なお,“.”のように仮引数がTensor a型のコールバックはイータ展開されず,テンソルのまま渡される.
12.10.6効率化のための工夫
実際の実装では,効率化のためにtensorMap2という組み込み関数も使われる. tensorMapをネストして使う方法では,対角化するために対角成分しか必要ない場合でも対角成分以外の成分ももつテンソルを生成してしまう. tensorMap2は\(2\)引数関数と二つのテンソルを引数にとり,結果のテンソルに必要な成分だけを計算するように実装されている.
12.11添字の反転とflipIndices関数
偏微分をするために使われる\(\partial\)/\(\partial\)関数はスカラー関数である. しかし,\(\partial\)/\(\partial\)関数はただのスカラー関数ではない. \(\partial\)/\(\partial\)関数は第二引数のテンソルの添字の上下を反転する. たとえば,(\(\partial\)/\(\partial\) \(\Gamma\)~i_j_k x~l)は,添字として“~i_j_k_l”をもつ四階のテンソルを返す.
このような動作を実現するために,EgisonにはflipIndicesという組み込み関数が用意されている. flipIndicesは,その引数のテンソルのすべての添字の上下を反転させる. 上下添字は反転させても上下添字のままである.
\(\partial\)/\(\partial\)関数は,以下のようにflipIndicesを使って定義される.
def `$\partial$`/`$\partial$` (f: Tensor MathValue) (x: Tensor MathValue)
: Tensor MathValue :=
tensorMap2 partialDiffMV f (flipIndices x)
-- partialDiffMV is an auxiliary function that computes
-- partial differentiation on scalar values
def partialDiffMV (f: MathValue) (x: MathValue) : MathValue := ...
tensorMap2により,fとflipIndices xの各成分に対してpartialDiffMV関数が適用される. flipIndices xにより第二引数の添字が反転されるため,結果のテンソルの添字も反転する.
以下は,\(\partial\)/\(\partial\)の使用例である.
declare symbol r, `$\theta$`, i, j
`$\partial$`/`$\partial$` [|(r * (sin `$\theta$`)),(r * (cos `$\theta$`))|]_i [|r,`$\theta$`|]_j
-- [| [| 'sin `$\theta$`, ('cos `$\theta$`) * r |], [| 'cos `$\theta$`, - ('sin `$\theta$`) * r |] |]_i~j
`$\partial$`/`$\partial$` [|(r * (sin `$\theta$`)),(r * (cos `$\theta$`))|]_i [|r,`$\theta$`|]_i
-- [| 'sin `$\theta$`, - ('sin `$\theta$`) * r |]~_i
一つ目の例では,第二引数の添字が_jから~jに反転され,結果の添字が_i~jとなる.
12.12generateTensor式によるテンソルの生成
generateTensor式はテンソルの初期化をするために便利な組み込み構文である. generateTensor式は第一引数にリストを引数にとる関数,第二引数に生成したいテンソルのサイズをとる. たとえば,すべての成分が\(1\)であるサイズが\((3, 4)\)の行列を生成するには以下のようにgenerateTensor式を書く.
generateTensor [2]#1 [3, 4]
-- [| [| 1, 1, 1, 1 |], [| 1, 1, 1, 1 |], [| 1, 1, 1, 1 |] |]
無名match関数と組み合わせると短い記述でいろいろなテンソルを生成できる. たとえば単位行列を生成するには以下のようにすればよい.
generateTensor (\match as list integer with
| [$n, #n] -> 1
| _ -> 0)
[3, 3]
-- [| [| 1, 0, 0 |], [| 0, 1, 0 |], [| 0, 0, 1 |] |]
12.13テンソルの宣言
テンソルを変数に束縛する方法を解説する. まずテンソルは通常の値と同様にdef式やlet式で定義することができる.
def A : Tensor Integer := [| [| 11, 12 |], [| 21, 22 |] |]
A -- [| [| 11, 12 |], [| 21, 22 |] |]
数学や物理では同じ変数名で添字の上下の型が違うテンソルにそれぞれ別の値を入れることがよくある. Egisonでもその慣習に対応するために,添字の上下の型ごとに違うテンソルを定義できるようにしている. Egisonは,変数を参照するとき,変数名と添字の型の両方を使う. 変数定義のときに,変数名の後ろに添字を続けて記述することによって添字の型を指定する.
def g_i_j : Tensor MathValue := [| [| 2, 2 |], [| 2, 2 |] |]_i_j
def g~i~j : Tensor MathValue :=
[| [| 1 / 2, 1 / 2 |], [| 1 / 2, 1 / 2 |] |]~i~j
g_1_1 -- 2
g~1~1 -- 1 / 2
添字の型を指定してテンソルが束縛されている変数に参照するには,ダミーシンボル(dummy symbol)を使うのが便利である. ダミーシンボルは,#で表現され,すべてユニークなシンボルとして扱われる. ダミーシンボルはEgisonに組み込みで実装されている機構である. ダミーシンボルを使うと,上記で定義したg~~とg__を以下のように参照できる.
g_#_# -- [| [| 2, 2 |], [| 2, 2 |] |]_#_#
g~#~# -- [| [| 1 / 2, 1 / 2 |], [| 1 / 2, 1 / 2 |] |]~#~#
宣言済みのシンボルを使っても添字の型を指定してテンソルを参照することもできるが,ダミーシンボルを使う方が宣言の必要がなく手軽である.
declare symbol i, j
g_i_j -- [| [| 2, 2 |], [| 2, 2 |] |]_i_j
g~i~j -- [| [| 1 / 2, 1 / 2 |], [| 1 / 2, 1 / 2 |] |]~i~j
なお,ひとつの式のなかに現れる複数のダミーシンボルは,それぞれ異なるシンボルとして扱われる.
数式でテンソルを定義するときのように,左辺の変数の添字としてシンボルを書くこともできる.
def A_i_j : Tensor Integer := [| [| 11, 12 |], [| 21, 22 |] |]_i_j
def B_i_j : Tensor Integer := [| [| 11, 12 |], [| 21, 22 |] |]_j_i
A_#_# -- [| [| 11, 12 |], [| 21, 22 |] |]_#_#
B_#_# -- [| [| 11, 21 |], [| 12, 22 |] |]_#_#
この機能は以下のような糖衣構文としてEgisonでは実装されている.
def A_i_j := ...
-- => def A__ := withSymbols [i, j]
-- transpose [i, j] ...
transpose関数は,テンソルの成分を第一引数で指定された順番に転置する組み込み関数である.
12.14添字付加のために便利な構文
階数がパラメーター\(n\)によって変わるテンソル\(A\)について,\(A_{i_{1}...i_{n}}\)のように添字を付加したいことがある. このためにsubrefsとsubrefs!という組み込み関数がEgisonには用意されている. これらの関数は第一引数にテンソルに第二引数に添字のリストを付加する. subrefsは第一引数のテンソルの既存の添字に追加で第二引数に添字のリストを付加するのに対して,subrefs!は既存の添字を消して新たに添字を付加し直す.
subrefs! A (map 1#i_$1 [1..n])
subrefs A (map 1#i_$1 [1..n])
\(A_{i_{1}...i_{n}}\)のような形のテンソルは数式でよく現れるため,上記のsubrefs!とsubrefsを使ったプログラムについては以下のような糖衣構文が用意されている.
A_(i_1)...(i_n)
A..._(i_1)...(i_n)
上記の内容は\(A^{i_{1}...i_{n}}\)のような上添字をもつテンソルにも用意されており,このためにsuprefsとsuprefs!という組み込み関数がEgisonには用意されている.
subrefsやsuprefsのように既存の添字に追加で添字を付加する機能は,第14章で紹介する微分形式についての関数を定義するときに使われる.
12.15テンソルの対称性・歪対称性の宣言
テンソルが対称であるとは,図12.15の例のように,上三角の成分と下三角の成分が一致することをいう. テンソルが歪対称であるとは,図12.15の例のように,上三角の成分と下三角の成分の符号が反転することをいう. テンソルが歪対称であるとき,対角成分は0となる.
数学や物理で現れるテンソルの多くが対称性をもつ. たとえば,14.2節で計算するリーマン曲率テンソル\(R_{abcd}\)は\(R_{abcd} = -R_{abdc}\),\(R_{abcd} = -R_{bacd}\),\(R_{abcd} = R_{cdab}\)という複数の対称性をもつ. 数学者や物理学者はこれらの対称性を意識しながら適宜計算を省略する. Egisonでも対称性を意識した計算の最適化を実装したいが,プログラミング言語でこの最適化をするには,明示的にテンソルの対称性を宣言する必要がある. Egisonはテンソルの対称性を宣言するための記法が実装されている. 本節は,この記法の使い方と実装を解説する.
12.15.1テンソルの対称性を宣言する記法
リーマン曲率テンソルには,上記の対称性に加えて第一ビアンキ恒等式\(R_{abcd} + R_{acdb} + R_{adbc} = 0\)とよばれる対称性もある. この第一ビアンキ恒等式の表現として,\(R_{a[bcd]} = 0\)という表記がある. Egisonに実装されているテンソルの対称性を宣言する記法は,この表記法に触発されて得られたものである.
具体例をみせながら,その記法を紹介する. Egisonでリーマン曲率テンソル\(R_{abcd}\)は下記のように定義できる. 右辺に複雑な式があるが,本節では無視していただいて問題ない. 左辺だけに注目してほしい.
def R_a_b_c_d : Tensor MathValue := withSymbols [i, j]
g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
`$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)
\(R_{abcd} = -R_{abdc}\)という歪対称性を宣言するには,以下のように添字_a_bを波括弧{}で囲む.
def R{_a_b}_c_d : Tensor MathValue := withSymbols [i, j]
g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
`$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)
上記のように\(R_{abcd}\)を定義すると,たとえば\(R_{21cd}\)を参照したとき,\(R_{12cd}\)の計算結果の符号を反転した値を返すようになる. 対称性を複数同時に宣言することもできる. \(R_{abcd} = -R_{abdc}\)と\(R_{abcd} = -R_{bacd}\)を同時に宣言するには,以下のように添字_a_bと_c_dの両方を波括弧{}で囲む.
def R{_a_b}{_c_d} : Tensor MathValue := withSymbols [i, j]
g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
`$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)
こうすると,たとえば\(R_{2121}\)を参照したとき,\(R_{1212}\)の計算結果を返すようになる.
\(R_{abcd} = R_{cdab}\)のような複雑な対称性も記述できる. この対称性を記述するためには添字_a_bと_c_dをそれぞれひとまとまりで扱うために丸括弧()で囲む. そして,これらを角括弧[]で囲む. 波括弧{}が歪対称性を宣言するために使われるのに対し,角括弧[]は対称性を宣言するために使われる.
def R[(_a_b)(_c_d)] : Tensor MathValue := withSymbols [i, j]
g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
`$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)
三つの対称性\(R_{abcd} = -R_{abdc}\),\(R_{abcd} = -R_{bacd}\),\(R_{abcd} = R_{cdab}\)を同時に宣言することもできる.
def R[{_a_b}{_c_d}] : Tensor MathValue := withSymbols [i, j]
g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
`$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)
まとめると,Egisonは対称性の宣言には三種類の括弧を使い分ける. 角括弧[]は対称性を宣言するために使う. 波括弧{}は歪対称性を宣言するために使う. 丸括弧()は複数の添字をひとまとまりにするために使う.
対称なテンソルの添字は隣り合っていることが多いため,数学や物理で現れるテンソルの対称性は,この記法でほぼ宣言することができる. :=の右辺のプログラムを全く変更せずに対称性を宣言できるところはこの記法のよいところである.
12.15.2対称性の宣言によってテンソルの定義が短くなる例
さきほど,この手法の利点として,:=の右辺のプログラムを全く変更する必要がないと述べたが,:=の右辺のプログラムが簡略化できるケースもある. たとえば,下記のようにテンソルの各ブロックごとに異なる式を使って値が定義されるテンソルがそのようなケースに該当する.
def R'_i_j_k_l : Tensor MathValue :=
generateTensor
(\match as list integer with
| [#1, #1, _, _] -> 0
| [_, _, #1, #1] -> 0
| [#1, $b, #1, $d] -> -1 * p^2 * `$\delta$`~(b - 1)_(d - 1)
| [$a, #1, #1, $d] -> p^2 * `$\delta$`~(a - 1)_(d - 1)
| [#1, $b, $c, #1] -> p^2 * g_(b - 1)_(c - 1)
| [$a, #1, $c, #1] -> -1 * p^2 * g_(a - 1)_(c - 1)
| [#1, $b, $c, $d] -> -1 * p * `$\nabla$`J_(b - 1)_(c - 1)~(d - 1)
| [$a, #1, $c, $d] -> p * `$\nabla$`J_(a - 1)_(c - 1)~(d - 1)
| [$a, $b, #1, $d] -> -1 * p * `$\nabla$`J~(d - 1)_(a - 1)_(b - 1)
| [$a, $b, $c, #1] -> p * `$\nabla$`J_(c - 1)_(a - 1)_(b - 1)
| [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)~(d - 1)
+ -1 * p^2 * J_(b - 1)_(c - 1) * J_(a - 1)~(d - 1)
+ p^2 * J_(a - 1)_(c - 1) * J_(b - 1)~(d - 1)
+ 2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)~(d - 1))
[5, 5, 5, 5]
対称性により条件分岐を大きく減らすことができる.
def R'[{_i_j}{_k_l}] : Tensor MathValue :=
generateTensor
(\match as list integer with
| [#1, #1, _, _] -> 0
| [#1, $b, #1, $d] -> -1 * p^2 * `$\delta$`~(b - 1)_(d - 1)
| [#1, $b, $c, $d] -> -1 * p * `$\nabla$`J_(b - 1)_(c - 1)~(d - 1)
| [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)~(d - 1)
+ -1 * p^2 * J_(b - 1)_(c - 1) * J_(a - 1)~(d - 1)
+ p^2 * J_(a - 1)_(c - 1) * J_(b - 1)~(d - 1)
+ 2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)~(d - 1))
[5, 5, 5, 5]
12.15.3実装
テンソルの対称性を宣言する記法の実装方法について解説する. この記法はgenerateTensor式を使う糖衣構文として実装されている. 本節では,この変換を具体例をいくつか紹介することによって説明する.
まず対称性を宣言する角括弧[]がどう展開されるか説明する. 以下のプログラムの...の箇所にはなにか適当なテンソルを返すプログラムがはいる.
def X[_i_j] := ...
上記の形のプログラムは,以下のようなプログラムに展開される.
def X_i_j : Tensor a :=
let tmpX_i_j := ...
generateTensor
(\i j -> if i > j then tmpX_j_i
else tmpX_i_j)
(tensorShape tmpX_#_#)
tmpXという新たな変数を導入し,定義したいテンソルを代入する. X自体はgenerateTensor式を使って定義する. このgenerateTensor式は,下半分の成分については,上半分の成分を参照するように定義されている. Egisonはテンソルの成分の評価を遅延するため,tmpXの下半分の成分は計算されることはない. そのため,テンソル成分の計算コストが半分になる.
歪対称性を宣言する波括弧{}も同じように展開される.
def X{_i_j} := ...
下半分の成分の符号が上半分の成分に対して反転していることと,対角成分が\(0\)になるようにgenerateTensor式の内部が変更されている.
def X_i_j : Tensor a :=
let tmpX_i_j := ...
generateTensor
(\i j -> if i > j then -tmpX_j_i
else if i = j then 0
else tmpX_i_j)
(tensorShape tmpX_#_#)
12.16tensorMap挿入の詳細な仕組み
Egisonでは,多相関数がテンソル引数に対して正しく動作するように,コンパイラが自動的にtensorMapやtensorMap2を挿入する. 本節では,この自動挿入の仕組みの詳細を解説する.
12.16.1処理フローとタイミング
tensorMapの挿入は,型推論(Phase 5-6)の後,型クラス展開(Phase 8-2)の前に実行される(Phase 8-1). 処理の流れは以下のとおりである:
- Phase 5-6: 型推論により,すべての式に型が付与される.
- Phase 8-1: TensorMap挿入により,必要な箇所に
tensorMap/tensorMap2が自動挿入される. - Phase 8-2: 型クラス展開により,型クラスメソッド(たとえば
(+))が辞書引きの形式(dict_AddSemigroup_("plus"))に変換される.
TensorMap挿入を型クラス展開の前に実行する理由は,引数の型(スカラーかテンソルか)を先に確定させることで,型クラス展開時にインスタンス選択が正しく行えるようにするためである.
12.16.2適用スパイン単位の二相の変換
挿入は,関数適用のスパイン(f a1 ... an)を単位として二相でおこなわれる. 第一相では,関数の主型から,スパインのどの引数位置がスカラー仮引数かを決定する. 第二相では,テンソルが渡されるスカラー位置をまとめてtensorMapやtensorMap2で包む. 位置の決定と包み込みを分離しているため,挿入の結果は引数を処理する順序に依存しない (12.16.7節の合流性).
12.16.3挿入の基本原則
TensorMap挿入は以下の基本原則に基づいて行われる:
原則1: 型コンストラクタ内のスカラー型に対する演算への挿入
型コンストラクタ(リスト[a],タプル(a, b)など)の内側にスカラー型,またはTensor型がインスタンスをもたないクラスの制約が付いた型変数がある場合,その型に対する演算には常にtensorMapまたはtensorMap2を挿入する.
たとえば,xs: [a]という型をもつ変数xsから取り出された要素xに対して,スカラー型を期待する演算(+)を適用する場合,tensorMap2 (+)という形式に変換される.
原則2: スカラーに対するtensorMapの動作
tensorMapとtensorMap2は,スカラー値に対してもそのまま適用できるように実装されている:
tensorMap f scalarはf scalarを返す(テンソルでない場合は恒等的に動作)tensorMap2 f s1 s2はf s1 s2を返す
この性質により,実行時に引数がスカラーかテンソルかを判定する条件分岐を挿入する必要がなくなり,実装が大幅に簡略化される.
12.16.4イータ展開された型クラスメソッドの処理
高階関数に渡された関数のイータ展開そのもの(挿入条件と例)は12.10.5節で解説した. 本節では,型クラスメソッドが関わる場合の実装上の処理を補足する.
型クラスメソッドは,TensorMap挿入の段階ではまだイータ展開された形式で現れる. たとえば,(+)演算子は以下のような形式になっている:
\etaVar1 etaVar2 -> dict_AddSemigroup_("plus") etaVar1 etaVar2
この2引数ラムダ式の本体が2引数関数適用である場合,本体全体をtensorMap2でラップする:
\etaVar1 etaVar2 -> tensorMap2 (\x y -> dict_AddSemigroup_("plus") x y) etaVar1 etaVar2
この変換により,型クラスメソッドに対してもtensorMap挿入が正しく適用される.
12.16.5具体例: sum関数
多相的なsum関数の変換過程を追うことで,TensorMap挿入の仕組みをより具体的に理解できる.
元の定義
def sum {AddMonoid a} (xs: [a]) : a := foldl (+) zero xs
この関数は,型クラス制約{AddMonoid a}をもつ多相的な型[a] -> aをもつ.
Phase 5-6: 型推論後
型推論により,型変数aが具体的な型(たとえばt0)にインスタンス化される:
def sum : {AddMonoid t0} [t0] -> t0 :=
\xs ->
foldl ((+) : {AddSemigroup t0} t0 -> t0 -> t0) (zero : {AddMonoid t0} t0) (xs : [t0])
ここで,xsの型は[t0]であり,型コンストラクタ[]の内側に型クラス制約付き型変数t0が存在する. また,(+)の型は{AddSemigroup t0} t0 -> t0 -> t0であり,スカラー型を引数にとる二項関数である.
Phase 8-1: TensorMap挿入後
(+)は二項関数であり,両方のパラメータがスカラー型(t0)であるため,tensorMap2でラップされる:
def sum : {AddMonoid t0} [t0] -> t0 :=
\xs ->
foldl (tensorMap2 (+)) zero xs
この時点で,xsの要素がテンソルである場合でも,tensorMap2により要素ごとの加算が正しく実行されるようになる.
Phase 8-2: 型クラス展開後
型クラスメソッド(+)が辞書引きの形式に展開される:
def sum : {AddMonoid t0} [t0] -> t0 :=
\dict_AddMonoid xs ->
foldl (tensorMap2 (dict_AddMonoid_("plus"))) (dict_AddMonoid_("zero")) xs
ここで,dict_AddMonoidはAddMonoid t0インスタンスのメソッド辞書である. スーパークラスの関係により,AddMonoidの辞書は自身のメソッド(zero)と継承されたAddSemigroupのメソッド(+)の両方を含む.
実行時の動作
この変換により,sum関数はスカラーとテンソルの両方に対して正しく動作する:
スカラーの場合 (t0 = Integer):
sum [1, 2, 3]
-- foldl1 (tensorMap2 (+)) [1, 2, 3]
-- tensorMap2 (+) 1 2 --> (+) 1 2 --> 3
-- tensorMap2 (+) 3 3 --> (+) 3 3 --> 6
-- Result: 6
スカラーに対しては,tensorMap2が恒等的に動作するため,通常の加算が行われる.
テンソルの場合 (t0 = Tensor Integer):
sum [[| 1, 2 |], [| 3, 4 |]]
-- foldl1 (tensorMap2 (+)) [[| 1, 2 |], [| 3, 4 |]]
-- tensorMap2 (+) [| 1, 2 |] [| 3, 4 |] --> [| 1+3, 2+4 |] --> [| 4, 6 |]
-- Result: [| 4, 6 |]
テンソルに対しては,tensorMap2が要素ごとに加算を適用する.
混合ケース:
sum [[| 1, 2 |], 3]
-- tensorMap2 (+) [| 1, 2 |] 3 --> tensorMap (\x -> x + 3) [| 1, 2 |]
-- --> [| 1+3, 2+3 |] --> [| 4, 5 |]
-- Result: [| 4, 5 |]
一方がテンソル,もう一方がスカラーの場合でも,tensorMap2が適切に処理する.
12.16.6まとめ
TensorMap挿入の仕組みにより,Egisonでは以下が実現されている:
- ユーザーは型クラス制約を使って多相的な関数を定義するだけで,テンソル演算が自動的にサポートされる.
- コンパイラが型情報をもとに
tensorMap/tensorMap2を自動挿入するため,ユーザーが明示的に記述する必要がない. - 実行時の型に応じて,スカラー演算とテンソル演算が自動的に切り替わる.
- 高階関数(
foldl,mapなど)に渡される関数引数に対しても,自動的に適切な変換が適用される.
この設計により,Egisonの数式処理システムは,スカラーとテンソルを統一的に扱うことができ,かつユーザーにとって直感的で使いやすいインターフェースを提供している.
12.16.7挿入の性質(保証)
型主導のtensorMap挿入は,以下の性質をもつように設計されている.
- 保守性: テンソルを使わないプログラムは,挿入によって一切変化しない.
スカラーだけのプログラムの意味は,挿入機構の導入前とまったく同じである.
- 決定性: どこに
tensorMapが挿入されるかは,関数の主型(principal type)だけから一意に決まる.型注釈は挿入の制御のためには不要であり,推論された型が同じなら挿入結果も同じである.
- 多引数の合流性:
tensorMap2や入れ子のtensorMapによる多引数のリフトは,どの引数から処理しても同じ結果になる(入れ子の順序に意味の差がない).
Tensor型のべき等性: 型のレベルではTensor (Tensor a)はTensor aと同一視される.これはEgisonのテンソルが「平坦な多次元配列+添字リスト」であり,テンソルのテンソルという入れ子構造が 値のレベルに存在しないことに対応している.
これらの性質は,型保存や型安全性とあわせて,Egisonの型付きテンソル計算の理論として定理の形で整備されている.