過去2回の記事「関係（非決定性写像）に関する用語」「(続き) 関係（非決定性写像）に関する記法」で、関係の話をしました。関係の計算にはテンソル計算を使うと便利です。テンソル計算は、物理や微分幾何だけでなく、様々な場面で使える汎用的でとても便利な道具です。
しかし、テンソル計算が自由に出来るまでのハードルはけっこう高くて、挫折する人も多いようです。僕も挫折した一人です。テンソル計算が難しい理由は：
- 奇妙な書き方を使う。
- やたらに省略をする。
見慣れない奇妙な書き方には違和感・抵抗感を感じます。が、「なんだこれ？」「気持ち悪い」という感情を抑え込めば乗り越えられます。より深刻な問題点は「やたらに省略をする」ほうで、省略されてしまった情報を補完するのが難しいのです。
とは言え、「省略されてしまった情報を補完する行為」が必要なのはテンソル計算に限ったことではありません。至るところで省略はしますからね。最近のプログラミング言語／証明支援系は、型推論機能、エラボレーション機能（賢く忖度して解釈や変換をする機能）を持っていて、省略されてしまった情報を頑張って補完します。人間より上手に補完するかも知れません。
人間対人間のコミュニケーションでも型推論・エラボレーションは必須なので、この記事でその話をします。テンソル計算に型推論・エラボレーションを適用することを想定してますが、テンソル計算自体の話はしません（たぶん後続の記事で）。テンソルの特別な場合である行列を事例にします。$`\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\For}{\Keyword{For }}
\newcommand{\Notation}{\Keyword {Notation }}
\newcommand{\valueIn}{\Keyword{ value-in }}
\newcommand{\implicitSigma}{\Keyword{implicit-sigma }}
\newcommand{\implicitLambda}{\Keyword{implicit-lambda }}
\newcommand{\isA}{\Keyword{ is-a }}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\hyp}{\text{－}}
%\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
`$
内容：
型推論
$`{\bf Z}`$ は整数の集合、$`{\bf N}_{\ge 1}`$ は正の〈1 以上の〉自然数の集合とします。整数 $`x \in {{\bf Z}}`$ を正の自然数 $`n\in {\bf N}_{\ge 1}`$ で割り算すると、整数になるとは限りませんが、有理数（$`{\bf Q}`$）の範囲なら商を求められます。このことを次のように書きましょう。
$`\For x\in {\bf Z}, n\in {\bf N}_{\ge 1}\\
\quad x/n \valueIn {\bf Q}
`$
'$`\Keyword{value-in}`$' は '$`\in`$' と書いても同じですが、目立つように色付きキーワードを使っています。
型理論では、同じことを型判断〈{type | typing} judgement〉という形式で書きます。
$`\quad x : {\bf Z}, n : {\bf N}_{\ge 1} \vdash x/n : {\bf Q}`$
この記事では、すぐ上の型判断の書き方は使いませんが、同じ内容を $`\Keyword{For}, \Keyword{value-in}`$ で書いた形式を型判断と呼びます。
上の型判断の一部を疑問符で置き換えます。
$`\For x\in {\bf Z}, n\in {\bf N}_{\ge 1}\\
\quad x/n \valueIn ?
`$
「疑問符のところに何が入るでしょうか？」という問題が型推論問題〈type {synthesis | inference} problem〉です。何の条件もないと、型推論問題の答は一意に決まりません。色々な意見があるでしょう。
- 整数や自然数の範囲で割り算が出来るとは限らないから、答はなしだ。
- 余り付き割り算をして整数商を求めるなら、$`? = {\bf Z}`$ だ。
- 商を有理数の範囲で考えれば、$`? = {\bf Q}`$ が妥当だな。
- いっそ、商は実数と考えて、 $`? = {\bf R}`$ がいいだろう。
型推論問題を解くには、条件・制約となる追加情報が必要です。まずスラッシュ記号（'$`/`$'）は $`\mrm{myDiv}`$ という関数の略記だとします。このことを次のように書きます。
$`\Notation x/n := \mrm{myDiv}(x, n)`$
型推論問題を次のように書き換えます。
$`\Notation x/n := \mrm{myDiv}(x, n)\\
\For x\in {\bf Z}, n\in {\bf N}_{\ge 1}, \mrm{myDiv}\in \mrm{Map}({\bf Z}\times {\bf N}_{\ge 1}, {\bf Q})\\
\quad x/n \valueIn ?
`$
記法〈書き方〉の約束である $`\Keyword{Notation}`$ を考慮すると、型推論問題は以下のようです。
$`\For x\in {\bf Z}, n\in {\bf N}_{\ge 1}, \mrm{myDiv}\in \mrm{Map}({\bf Z}\times {\bf N}_{\ge 1}, {\bf Q})\\
\quad \mrm{myDiv}(x, n) \valueIn ?
`$
こうなると、確実に $`? = {\bf Q}`$ だと答えることができます。
コミュニケーションのなかで型推論問題を解くには、記法の約束や明示的に書いてない条件・制約などを文脈のなかから読み取る必要があります。また、一般的に成立する型推論のパターンを知っている必要もあります。今の場合なら、次が一般的に成立する型推論のパターンです。
$`\For x\in X, y\in Y, f\in \mrm{Map}(X \times Y, Z)\\
\quad f(x, y) \valueIn Z
`$
行列
$`R`$ は足し算と掛け算を備えた集合（半環と呼ぶ）だとします。記号の乱用で $`R = (R, +, 0, \cdot, 1)`$ と書きます。よく使われる演算記号 $`+, \cdot`$ 、定数記号 $`0, 1`$ はオーバーロード〈多義的使用〉します。我々が慣れ親しんだ計算法則は成立するとします。ただし、引き算・割り算は要求しません。
$`X, Y`$ が集合のとき、$`X, Y`$ をインデックス集合とする$`R`$-係数の行列とは次の写像です。
$`\quad a: X\times Y \to R`$
写像〈関数〉の値 $`a(x, y)`$ をテンソル計算の習慣に従い、$`a_x^y`$ とも書きます。
$`\Notation a_x^y := a(x, y)`$
行列を縦横のテーブル形式で書くなら、$`x`$ が横方向のインデックスで、$`y`$ が縦方向のインデックスです。$`a_x^y`$ が行列の成分値です。
違和感・抵抗感を感じたかも知れませんが、次のことを思い出してください。
- 「なんだこれ？」「気持ち悪い」という感情を抑え込めば乗り越えられます。
インデックス集合 $`X, Y`$ に無限集合を許すかどうかは、「$`R`$ が無限和を持つか？」「有限サポート条件を付けるか？」などに関わるのですが、話がややこしくなるので今は気にしないことにします。とりあえず、インデックス集合は有限集合に限定してかまいません。
$`X, Y`$ をインデックス集合とする$`R`$-係数行列の全体からなる集合を $`\mrm{Mat}[R](X, Y)`$ と書きます*1。係数となる半環 $`R`$ を固定しているときは $`\mrm{Mat}(X, Y)`$ と省略します。
$`a\in \mrm{Mat}[R](X, Y)`$ であることを $`a:X \to Y`$ とも書きます -- ンッ、あれれ？ 矢印を使った書き方が二種類出てきてしまいました。
$`\quad a: X\times Y \to R\\
\quad a: X \to Y
`$
矢印のような人気の(?)記号は引っ張りだこで、オーバーロードされるのは珍しくありません。珍しくはないのですが、区別しにくいので困ります。そこで、$`\Keyword{is-a}`$ という色付きキーワードを使って区別することにします。
$`\quad a\in \mrm{Map}(X\times Y, R)\\
\Iff a: X\times Y \to R \isA \text{map}\\
\:\\
\quad a\in \mrm{Mat}[R](X ,Y)\\
\Iff a: X \to Y \isA R\text{-matrix}
`$
矢印のオーバーロードはとんでもなく多いですね*2。例えば、写像〈map〉、部分写像〈partial map〉、非決定性写像〈nondeterministic map〉、関係〈relation〉のどれも矢印で書きます。
$`\quad f\in \mrm{Map}(X, Y)\\
\Iff f: X\to Y \isA \text{map}\\
\:\\
\quad f\in \mrm{Partial}(X, Y)\\
\Iff f: X\to Y \isA \text{partial}\\
\:\\
\quad f\in \mrm{NonDet}(X, Y)\\
\Iff f: X\to Y \isA \text{nondet}\\
\:\\
\quad f\in \mrm{Rel}(X, Y)\\
\Iff f: X\to Y \isA \text{rel}
`$
非決定性写像と関係は事実上同じものです。関係とブール値係数行列も事実上同じものです。よって、次の3つは区別する必要がありません。（$`{\bf B}`$ はブール値の集合です。）
$`\quad f: X \to Y \isA \text{nondet}\\
\quad f: X \to Y \isA \text{rel}\\
\quad f: X \to Y \isA {\bf B}\text{-matrix}
`$
区別すべきモノは区別するのと同時に、区別しなくていいモノを同一視するのは重要なことです。
行列の掛け算とアインシュタイン規約
$`a, b`$ を行列とするとき、$`a, b`$ の（この順での）掛け算は以下のように定義します。セミコロン（'$`;`$'）が掛け算記号で、通常の行列の掛け算とは左右が逆順になります。
$`\For a:X \to Y \isA R\text{-marix}\\
\For b:Y \to Z \isA R\text{-marix}\\
\For x\in X, z\in Z\\
\quad (a;b)_x^z := \sum_{y} a_x^y b_y^z`$
ここで使われた暗黙の規則、あるいは省略事項を挙げましょう。
- $`R`$ の要素（スカラーと呼んでいいでしょう）の掛け算記号 '$`\cdot`$' は省略している。
- $`\sum`$ は総和記号だが、下付きの $`y`$ が $`y\in Y`$ であることは明示してない。
ここから先、次のような約束をします。
- 総和をとる変数（今の例では $`y`$）の型（所属する集合）は、事前に宣言しておいて、総和記号のなかには書かなくてもよい。
- $`\sum_y`$ の代わりに $`\Sigma\,y.`$ と書いてもよい。この書き方は、ラムダ記法にあわせたもの。
上の約束のもとで、行列の掛け算の定義は：
$`\For a:X \to Y \isA R\text{-marix}\\
\For b:Y \to Z \isA R\text{-marix}\\
\For x\in X, y\in Y, z\in Z\\
\quad (a;b)_x^z := \Sigma\,y. a_x^y b_y^z`$
さらに劇的な省略を導入します。総和記号（$`\sum_y`$ または $`\Sigma\,y.`$）を完全に省略します。この省略の習慣をアインシュタインの総和規約〈Einstein summation convention〉、あるいは単にアインシュタイン規約と呼びます。
$`\For a:X \to Y \isA R\text{-marix}\\
\For b:Y \to Z \isA R\text{-marix}\\
\For x\in X, y\in Y, z\in Z\\
\quad (a;b)_x^z := a_x^y b_y^z`$
総和記号が省略されたことをどうやって判断するかというと、インデックス〈添字〉$`y`$ が上下に出現するので、「上下に出現したインデックスは総和をとる」という約束〈規約〉です。
アインシュタイン規約には戸惑うし、総和をとるインデックスを判別するのが難しかったりします。そこで、暗黙のシグマ〈implicit sigma〉の場所を明示化する（暗黙じゃなくする）キーワード $`\Keyword{implicit-sigma}`$ を使いましょう。
$`\For a:X \to Y \isA R\text{-marix}\\
\For b:Y \to Z \isA R\text{-marix}\\
\For x\in X, y\in Y, z\in Z\\
\quad (a;b)_x^z := (\implicitSigma a_x^y b_y^z)`$
$`\Keyword{implicit-sigma}`$ は、アインシュタイン規約に慣れるまでのヒントです。自転車に乗れるようになるために補助輪を使うようなものです。
行列の掛け算記号にセミコロンを使うのは見慣れない人も多いでしょうから、通常の書き方を（記法として）定義しておきます。
$`\For a:X \to Y \isA R\text{-marix}\\
\For b:Y \to Z \isA R\text{-marix}\\
\Notation b \circ a := a; b\\
\Notation b\, a := b \circ a
`$
暗黙のラムダと型推論
アインシュタイン規約により総和記号〈シグマ〉を省略してしまうのはビックリする人もいるでしょう。しかし、アインシュタイン規約よりずっとたちが悪い省略が常用されています。それは、関数を表すラムダ記号の省略です。
次の型判断は正しい型判断です。
$`\For f \in \mrm{Map}(X\times Y, Z)\\
\For a \in X, b \in Y\\
\quad f(a, b) \valueIn Z\\
\quad \lambda\, x\in X. f(x, b) \valueIn \mrm{Map}(X, Z)\\
\quad \lambda\, x\in X. \lambda\, y\in Y. f(x, y) \valueIn \mrm{Map}(X, \mrm{Map}(Y, Z) )\\
\quad \lambda\, (x, y)\in X\times Y. f(x, y) \valueIn \mrm{Map}(X\times Y, Z)
`$
ラムダ変数（関数の引数変数）の宣言も事前にすることにすれば、次も同じ型判断です。自由変数と束縛変数〈ラムダ変数〉に同じ名前 $`x, y`$ を使っているのが“気持ち悪い”かも知れませんが、普通に使っている書き方です（良くはないけど）。
$`\For f \in \mrm{Map}(X\times Y, Z)\\
\For x \in X, y \in Y\\
\quad f(x, y) \valueIn Z\\
\quad \lambda\, x. f(x, y) \valueIn \mrm{Map}(X, Z) \\
\quad \lambda\, x. \lambda\, y. f(x, y) \valueIn \mrm{Map}(X, \mrm{Map}(Y, Z) )\\
\quad \lambda\, (x, y). f(x, y) \valueIn \mrm{Map}(X\times Y, Z)
`$
ラムダ記号を書くのが面倒だから省略しよう ‥‥ すると：
$`\For f \in \mrm{Map}(X\times Y, Z)\\
\For x \in X, y \in Y\\
\quad f(x, y) \valueIn Z\\
\quad f(x, y) \valueIn \mrm{Map}(X, Z)\\
\quad f(x, y) \valueIn \mrm{Map}(X, \mrm{Map}(Y, Z) )\\
\quad f(x, y) \valueIn \mrm{Map}(X\times Y, Z)
`$
$`f(x, y)`$ の型（所属する集合）がなんだか分からなくなります。つまり、型推論が不可能になります。結局、正しい解釈はできないことになります。
実は（悲報ですが）、「ラムダ記号を書くのが面倒だから省略しよう」は日常茶飯におこなわれています。
前回記事「(続き) 関係（非決定性写像）に関する記法」の一部をそのまま引用します。
$`R \in \mrm{Rel}(X, Y)`$ をブール値係数行列とみなした上で、上下の添字〈インデックス〉を使った成分記法で、次のように書きます。
$`\quad R = (R_x^y)_{x\in X}^{y\in Y} = (R_x^y)`$
文字 '$`R`$' が今回記事の係数半環の '$`R`$' とかち合って〈コンフリクトして〉ますが、それもアルアルなので、しれっと小文字 $`r`$ に書き換えてみれば：
$`\quad r = (r_x^y)_{x\in X}^{y\in Y} = (r_x^y)`$
$`(r_x^y)_{x\in X}^{y\in Y}`$ は、ラムダ記法の別記法です。つまり、
$`\Notation (r_x^y)_{x\in X}^{y\in Y} := \lambda\, x\in X, y \in Y.r_x^y
= \lambda\, (x, y) \in X \times Y.r_x^y`$
次のような（正しい！）型判断はできます。
$`\For r \in \mrm{Map}(X\times Y, {\bf B})\\
\For x \in X, y \in Y\\
\quad r_x^y \valueIn {\bf B}\\
\quad \lambda\, (x, y) \in X\times Y.r_x^y \valueIn \mrm{Map}(X\times Y, {\bf B})\\
\quad (r_x^y)_{x\in X}^{y\in Y} \valueIn \mrm{Map}(X\times Y, {\bf B})\\
\quad \lambda\, (x, y).r_x^y \valueIn \mrm{Map}(X\times Y, {\bf B})\\
\quad (r_x^y)_{x}^{y} \valueIn \mrm{Map}(X\times Y, {\bf B})
`$
しかし、$`(r_x^y)_{x\in X}^{y\in Y} = (r_x^y)`$ の左右の型は食い違っているので、等式だと認めるのは困難です。右辺の丸括弧に特殊な意味があるのか？ とか推測できますが、丸括弧なんて全然当てになりません。
暗黙のシグマ〈implicit sigma〉の場合と同様に、暗黙のラムダ〈implicit lambda〉で省略を明示化しましょう。
$`\For r \in \mrm{Map}(X\times Y, {\bf B})\\
\For x \in X, y \in Y\\
\quad r_x^y \valueIn {\bf B}\\
\quad (\implicitLambda r_x^y) \valueIn \mrm{Map}(X\times Y, {\bf B})
`$
矢印記号を使ってみると：
$`\For r \in \mrm{Map}(X\times Y, {\bf B})\\
\For x \in X, y \in Y\\
\quad r_x^y \valueIn {\bf B}\\
\quad (\implicitLambda r_x^y) : X \times Y \to {\bf B} \isA \text{map}\\
\quad (\implicitLambda r_x^y) : X \to Y \isA {\bf B}\text{-matrix}
`$
暗黙のシグマ（アインシュタイン規約）と暗黙のラムダを同時に使って、行列の掛け算の定義と型判断を書いてみましょう。
$`\For a:X \to Y \isA R\text{-marix}\\
\For b:Y \to Z \isA R\text{-marix}\\
\For x\in X, y\in Y, z\in Z\\
\quad (b\, a)_x^z := (\implicitSigma b_y^z a_x^y) \valueIn R\\
\quad (\implicitLambda (\implicitSigma b_y^z a_x^y) )\valueIn \mrm{Map}(X \times Z, R)\\
\quad (\implicitLambda (\implicitSigma b_y^z a_x^y) ): X \times Z \to R \isA \text{map}\\
\quad (\implicitLambda (\implicitSigma b_y^z a_x^y) ): X \to Z \isA R\text{-matrix}`$
一番最後の行は、明示的に書けば次のとおりです。
$`\quad \lambda\, (x, z) \in X \times Z. \Sigma\, y\in Y. b_y^z a_x^y : X \to Z \isA R\text{-matrix}`$
次でも同じことです。
$`\quad \lambda\, x\in X, z\in Z. \Sigma\, y\in Y. b_y^z a_x^y : X \to Z \isA R\text{-matrix}`$
あるいは：
$`\quad (\sum_{y \in Y} b_y^z a_x^y)_{x\in X}^{z \in Z} : X \to Z \isA R\text{-matrix}`$
緑色のキーワードと関連情報は“補助輪”なので、取り外されることがあります。
- $`\Keyword{For}`$ で書かれている“前提となる型宣言”は、文脈のなかに紛れているかも知れない。何も書いてなくて推測するしかないかも知れない。
- 暗黙のシグマは、ほんとに暗黙で何も書いてないかも知れない。
- 暗黙のラムダは、ほんとに暗黙で何も書いてないかも知れない。
- $`\valueIn`$ の部分が書かれてないなら、自分で型推論問題 $`\valueIn ?`$ を設定して解く必要がある。
おわりに
上下の添字を使ったテンソル記法は難読で分かりにくいデメリットがありますが、コンパクトに書けて記述や計算が速くできるメリットがあります。通常は、デメリットは無視してメリットを取るのです。
ここまで、行列をテンソル記法で書いてみて、“補助輪”（ヒント情報）付きの解説をしました。テンソルを使った記述や計算では、緑色キーワードの“補助輪”が取り外された状態で話が進みます。型推論・エラボレーションは自力でおこなって読み解く必要があります。本番に臨む前に、“補助輪あり”で練習をすることをおすすめします。
