檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2017-05-29 (月)

Scilabで行列計算をしてみる

| 10:13 | Scilabで行列計算をしてみるを含むブックマーク

今までR言語で行列計算してたんですが、Scilabに替えてみました。行列計算に限れば、Scilabのほうがずっと使い勝手がいいです。

  1. R言語には不満が募ってきた
  2. Scilab
  3. Scilabコンソール
  4. 行列計算をはじめる
  5. 行列のブロック操作と寸法
  6. 成分と部分行列の取り出し
  7. インデックス・アクセスと関数呼び出し
  8. 逆行列行列式
  9. おわりに

R言語には不満が募ってきた

数値的行列計算が必要なとき僕は、R言語を使っていました。Rコンソールを立ち上げれば、その場ですぐ計算できるので便利ではあるのですが、いくつか不満もあります。

  1. 行列を直接表現するリテラル表記がなくて、matrix(c(1, 3, 2, 4), 2, 2) のような関数呼び出しが必要でうっとうしい。
  2. 行列の掛け算記号が %*% 。基本演算子が3打鍵必要なのがイヤ。
  3. 行列のブロック操作がサクサクできないのでフラストレーションを感じる。

ここでRの悪口を言っても生産的ではないので詳細は書きませんが、3番目の不満が意味不明でしょうから説明します。「行列のブロック操作」と書きましたが、正式になんと言うのか知りません。例示するなら、

A = ¥begin{bmatrix}1 & 2 ¥¥ 3 & 4¥end{bmatrix} ¥¥B = ¥begin{bmatrix}5 & 6 ¥¥ 7 & 8¥end{bmatrix}

という行列A, Bがあったとき、例えばAとBを対角位置に並べてCを作る操作とかです。

C = ¥begin{bmatrix}A & O ¥¥ O & B¥end{bmatrix} = ¥begin{bmatrix}1 & 2 & 0 & 0 ¥¥3 & 4 & 0 & 0 ¥¥0 & 0 & 5 & 6 ¥¥0 & 0 & 7 & 8 ¥end{bmatrix}

もっと簡単な例だと:

X = ¥begin{bmatrix}1 ¥¥ 2 ¥end{bmatrix} ¥¥Y = ¥begin{bmatrix}3 ¥¥ 4¥end{bmatrix} ¥¥Z = ¥begin{bmatrix}X & Y ¥end{bmatrix}  = ¥begin{bmatrix} 1 && 3 ¥¥ 2 && 4 ¥end{bmatrix}

Scilab

ちょっと調べてみて、Scilab(サイラボ)がヨサゲな印象でした。Scilabのホームページは:

https://www.scilab.org/download/latestから各プラットフォームごとのインストール用アーカイブ(バイナリ配布物)をダウンロードできます。現時点(2017年春)での最新バージョンは Scilab 6.0.0 です。インストールは簡単です、特に説明することはないです。

https://www.scilab.org/resources/documentation/tutorials から、日本語PDF文書Scilab_beginners_jp.pdf(はじめてのScilab -- 33ページ)、Xcos_beginners_jp.pdf(はじめてのXcos -- 15ページ)をダウンロードできます。もう少し詳しい解説はintroscilab.pdf(INTRODUCTION TO SCILAB -- 87ページ)。文書は若干古めで、最新バージョンとはズレがあります。が、深刻な問題にはならないでしょう。

ソフトウェアに付属のヘルプも日本語化されていて(見出しは英語のまま)、かなり充実しています。ブラウザでマニュアルを見たいなら、インターネット上のページがあります。

ソフトウェア付属のヘルプとWebオンラインマニュアルは、最新バージョンの情報だと期待してよさそうです。

どうでもいいことですが、Scilabのlabを「ラボ」と読むのは「ラボラトリー(laboratory)」の略だという前提があるからで、labだけなら「ラブ」に近いと思うのだけど…。僕は「サイラブ」と読んで(呼んで)しまいますね。

[追記]次のサイトに、日本語を含む多言語による情報があります。

[/追記]

Scilabコンソール

Scilabをインストールしたら起動します。初期状態では、メインウィンドウ内にいくつかのサブウィンドウが詰め込まれた最近のIDEっぽい外観です。ゴチャゴチャしていてい僕は好きじゃないのですが、カスタマイズとかは後回しにしてスーパー電卓(a super desktop calculator)*1としてScilabを使ってみます。

Scilab 6.0.0 コンソール」(日本語UI)とタイトルされたペイン(サブウィンドウ)がScilabコンソールです。このコンソールが対話的インタプリタのコマンドラインインターフェイスです。今回はScilabコンソールしか使いません。

「-->」がインタプリタのプロンプトマークで、この後にキーボード入力して、Enter/Returnキーを押せばScilabインタプリタが応答を返します。

--> disp("Hello, world")

 Hello, world


--> 1 + 2
 ans  =

   3.


--> x = 1 + 2
 x  =

   3.


--> y = x*2 + 1
 y  =

   7.


--> sqrt(y) // yの平方根
 ans  =

   2.6457513

1行目のdisp()はプリント用関数です。1 + 2 のような計算式を入力すれば結果が表示されますが、その結果はansという変数に代入されます。ただし、明示的な代入文を書けば(x = 1 + 2)、ansへの自動代入はされません。計算は倍精度浮動小数点数(64ビット実数)で行われ、値がちょうど整数でも小数点は表示されます*2。関数呼び出しは、たいていのプログラミング言語と同じ func(arg) の形です。スラッシュ2個から行末まではコメントです。

行列計算をはじめる

Scilabでは、行列を非常に分かりやすい形式で入力できます。1行分のデータはカンマか空白で区切り、次の行に移るにはセミコロンを使います。

--> [1, 2; 3, 4]
 ans  =

   1.   2.
   3.   4.


--> [1 2; 3 4] // カンマの代わりに空白でもよい
 ans  =

   1.   2.
   3.   4.


--> a = [1 2; 3 4] // 行列を変数に代入
 a  =

   1.   2.
   3.   4.

行列の掛け算はアスタリスク1文字です。加減はもちろんプラスとマイナス。

--> b = [5 6; 7 8]
 b  =

   5.   6.
   7.   8.


--> a*b
 ans  =

   19.   22.
   43.   50.


--> a + b
 ans  =

   6.    8.
   10.   12.


--> a - b
 ans  =

  -4.  -4.
  -4.  -4.

スカラー倍もアスタリスクです。

--> 2*a
 ans  =

   2.   4.
   6.   8.


--> a*-1
 ans  =

  -1.  -2.
  -3.  -4.

Scilabにベクトル型データはありません*3が、1行n列-行列かn行1列-行列でベクトルを表現できます。どっちにするかは「決め」(約束)の問題です。例えば、ベクトルをn行1列-行列=列ベクトルで表現するとして、行列とベクトルの積は次のようです。

--> a*[2; -1]
 ans  =

   0.
   2.


--> b*[2; -1]
 ans  =

   4.
   6.

行列の転置(縦と横の入れ替え)は、'(シングルクォート)を後置します*4

--> a'
 ans  =

   1.   3.
   2.   4.


--> [2; -1]'
 ans  =

   2.  -1.

ベクトルの内積は転置して掛ければいいので:

--> x = [2; -1]; y = [5; 3]; // 2つの代入文を行って、結果の表示は行わない

--> x'*y // ベクトルxとyの内積
 ans  =

   7.

行列のブロック操作と寸法

特別な行列を表現する関数が用意されています。対角成分が1で他は0である行列は eye(行数, 列数) で、すべての成分が0である行列は zeros(行数, 列数) で作れます。

--> eye(2, 2)
 ans  =

   1.   0.
   0.   1.


--> eye(3, 2)
 ans  =

   1.   0.
   0.   1.
   0.   0.


--> zeros(3, 2)
 ans  =

   0.   0.
   0.   0.
   0.   0.

冒頭に挙げたブロック操作をやってみます。

--> a
 a  =

   1.   2.
   3.   4.


--> b
 b  =

   5.   6.
   7.   8.


--> o = zeros(2, 2)
 o  =

   0.   0.
   0.   0.


--> c = [a o; o b]
 c  =

   1.   2.   0.   0.
   3.   4.   0.   0.
   0.   0.   5.   6.
   0.   0.   7.   8.


--> x = [1; 2]; y = [3; 4];

--> z = [x y]
 z  =

   1.   3.
   2.   4.

簡単でしょ。

行列の行数と列数が欲しいときはsize()関数、成分の個数が欲しいときはlength()関数を使います。

--> size(c)
 ans  =

   4.   4.


--> length(c)
 ans  =

   16.


--> size([1; 2])
 ans  =

   2.   1.


--> size([1; 2]')
 ans  =

   1.   2.


--> length([1; 2])
 ans  =

   2.

成分と部分行列の取り出し

多くのプログラミング言語では、配列、リスト、タプル、ベクトル、行列などの成分(要素、項目)を取り出すにはブラケットを使って、x[2], a[1, 2] のように書きます。Scilibでは、丸括弧で x(2), a(1, 2) のように書きます。

--> x
 x  =

   1.
   2.


--> x(1)
 ans  =

   1.


--> a
 a  =

   1.   2.
   3.   4.


--> a(1, 2)
 ans  =

   2.

関数呼び出しと区別が付かなくて困らないか? 困りません。それどころか、区別が付かないのでかえって便利です、後で例を挙げます。JVM上で動く関数型言語Scalaでは、やはりインデックス・アクセスと関数呼び出しが同じ形式ですね。

次に、行列の単一成分に限らず、いくつかの成分をまとめて取り出してみます。そのために範囲記法を説明しておくと、n:m で「nからmまでの整数範囲」*5を意味します。

--> 0:3
 ans  =

   0.   1.   2.   3.


--> 1:10
 ans  =

   1.   2.   3.   4.   5.   6.   7.   8.   9.   10.

範囲の実体は横ベクトル(1行n列の行列)です。この範囲記法を使うと、行列の一部を素早く抜き出せます。

--> c
 c  =

   1.   2.   0.   0.
   3.   4.   0.   0.
   0.   0.   5.   6.
   0.   0.   7.   8.


--> c(1:4, 2:3)
 ans  =

   2.   0.
   4.   0.
   0.   5.
   0.   7.


--> c([1 2 3 4], [2 3])
 ans  =

   2.   0.
   4.   0.
   0.   5.
   0.   7.


--> c([2 3], [2 3])
 ans  =

   4.   0.
   0.   5.

範囲は横ベクトルなので、直接横ベクトルを書いても同じです -- 長い範囲だと直接書くのはシンドイですがね。範囲を示すコロンの特別な用法として、次のような書き方ができます。

--> c(:, [2, 3])
 ans  =

   2.   0.
   4.   0.
   0.   5.
   0.   7.


--> c(:, 2)
 ans  =

   2.
   4.
   0.
   0.


--> c(1, :)
 ans  =

   1.   2.   0.   0.

コロンだけだと、その行列が持つ行範囲、列範囲になるのです。行列のサイズを意識せずに「行全部/列全部」を指定できるので便利です。

抜き出す部分は、範囲では記述できないパランパランな部分でもいいです。

--> c
 c  =

   1.   2.   0.   0.
   3.   4.   0.   0.
   0.   0.   5.   6.
   0.   0.   7.   8.


--> c(:, [1 4])
 ans  =

   1.   0.
   3.   0.
   0.   6.
   0.   8.

インデックス・アクセスと関数呼び出し

前節で、「インデックス・アクセスと関数呼び出しを区別しないほうが便利だ」と書きました。実例を挙げましょう。

整数引数の関数fと、整数n, m(n≦m)に関して次の総和を考えます。

 ¥sum_{i = n}^{m} f(i)

これを、関数f, 整数n, mを引数とする関数(高階関数)と考えて、

 total(f,¥, n,¥, m) ¥: := ¥sum_{i = n}^{m} f(i)

としましょう。これをScilabの関数で書くと次のようになります。プログラムとして見やすいように、f→fun、n→from、m→to とリネームしています。

function ret = total(fun, from, to)
    ret = 0
    for i = from:to do
        ret = ret + fun(i)
    end
endfunction

Scilabの関数定義構文の説明はしませんが、何となくは分かるでしょう。

さて、奇数の総和は平方数になるという事実があります。

 ¥sum_{i = 1}^{n} 2n - 1 ¥: = ¥: n^2

この事実を関数total()を使って確認してみます。

--> function ret = odd(n)
  >     ret = 2*n - 1
  > endfunction

--> odd(1)
 ans  =

   1.


--> total(odd, 1, 4)
 ans  =

   16.


--> total(odd, 1, 5)
 ans  =

   25.

関数odd()を定義して、関数(高階関数)total()に渡したのですが、奇数の列は別に関数でなくてもかまいません。

--> 1:2:9
 ans  =

   1.   3.   5.   7.   9.


--> total(1:2:9, 1, 4)
 ans  =

   16.


--> total(1:2:9, 1, 5)
 ans  =

   25.

ここで、1:2:9は範囲(実体は行ベクトル)ですが、1から2ずつ増加して9に至る整数並びです。

関数も行ベクトル(あるいは列ベクトル)も同じ形式でアクセスできるので、total()の第1引数は関数でもベクトル(特殊な行列)でもいいのです。計算手順とデータを統一的に扱えて便利です。

逆行列行列式

行列Aの逆行列はA-1と書きます。この書き方にならって、Sailabでも a^-1 という記法で逆行列を表現できます。また、逆数と同じ 1/a でも逆行列です。


--> a
 a  =

   1.   2.
   3.   4.


--> a^-1
 ans  =

  -2.    1.
   1.5  -0.5


--> 1/a
 ans  =

  -2.    1.
   1.5  -0.5


--> a*1/a
 ans  =

   1.   0.
   0.   1.

ウーン、まーいいんですけど、僕は inv(a) という書き方が落ち着きます。


--> inv(a)
 ans  =

  -2.    1.
   1.5  -0.5


--> a*inv(a)
 ans  =

   1.          0.
   8.882D-16   1.


--> inv(a)*a
 ans  =

   1.          0.
   2.220D-16   1.

アレッ? a*inv(a)が単位行列になってませんね。2.220D-16はものすごく小さい数なので、浮動小数点数の誤差でしょうが、1/aだと正確に0だったのは不可解。ちょっと事情が分かりません。

逆行列の存在・非存在は行列式を見れば分かりますが、aの行列式はdet(a)です。

--> a
 a  =

   1.   2.
   3.   4.


--> det(a)
 ans  =

  -2.


--> inv(a)
 ans  =

  -2.    1.
   1.5  -0.5


--> det(inv(a))
 ans  =

  -0.5


--> det(a*inv(a))
 ans  =

   1.

おわりに

というわけで、Scilabだと行列計算が気持ちよく出来るよ というお話でした。

*1:"INTRODUCTION TO SCILAB"の22ページに、Scilabは"a super desktop calculator"であり、またそれ以上のものである、と書いてあります。

*2:デフォルトが実数(浮動小数点数)ですが、n = int32(10) のような型変換を使うと、適当なビット長(この場合は32ビット)の整数データを作れます。整数の10は、10. ではなくて 10 と表示されます。

*3:実は、厳密に言えばスカラー型もありません。1行1列の行列がスカラーとして扱われています。

*4:'(シングルクォート)は実際はエルミート転置(Hermitian transpose, conjugate transpose)です。単なる転置は.'(ドットとクォート)という演算子ですが、実数成分の場合は単なる転置もエルミート転置も変わりはありません。

*5:x:y という書き方の意味は、xを初項とする等差数列のyを越えない部分です。例えば、1.2:5 の値は [1.2, 2.2, 3.2, 4.2] となります。今の文脈では、初項と上限に整数値(データ型は実数)を取っているので整数範囲を表すことになっています。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170529

2017-05-24 (水)

無料で入手できる本格的(紙なら高額)な理数系専門書15選 第2回(2017年春)

| 10:16 | 無料で入手できる本格的(紙なら高額)な理数系専門書15選 第2回(2017年春)を含むブックマーク

去年・2016年の夏に、「無料で入手できる本格的(紙なら高額)な理数系専門書15選」という記事でインターネットから入手可能な専門書を15冊紹介しました。

出版されている書籍と同じ内容のPDFファイルやHTMLページがインターネットに公開されている例は意外と多いみたいで、一年たたずに新しい15冊のリストができました。前回(2016年夏)と同様に、著作権があやしいものは除外し、著者本人または著者の所属組織のWebサイト、あるいはarXiv.org, TAC (Theory and Applications of Categories)で公開されているものだけを紹介します。また、この記事の後半で過去に紹介した20冊のタイトルとURLを再掲します。

  1. Differential Algebraic Topology: From Stratifolds to Exotic Spheres
  2. Lectures on the Geometry of Manifolds
  3. 3次元多様体入門
  4. Parametrized Homotopy Theory
  5. Noncommutative Geometry
  6. Category Theory in Context
  7. Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist
  8. Category Theory for Computing Science
  9. Higher Operads, Higher Categories
  10. Axiomatic Method and Category Theory
  11. Practical Foundations of Mathematics
  12. Geometric Integration Theory
  13. Foundations of Algebraic Specification and Formal Software Development
  14. Stochastic Integration with Jumps
  15. Optimal transport, old and new

幾何

Differential Algebraic Topology: From Stratifolds to Exotic Spheres

著者Kreckが創始したストラティフォールドという概念をベースにした代数トポロジーの教科書です。ストラティフォールドを使うことにより、代数的不変量を幾何的に構成しています。目標は、エキゾチック7-球面の構成(19章)で、11章あたりからその準備がはじまるようです。

Lectures on the Geometry of Manifolds
Lectures On The Geometry Of Manifolds

Lectures On The Geometry Of Manifolds

初版は1996年で、それ以来メンテナンスされているようで、最新の修正は今年(2017年)です。大部な教科書で、多様体について必要なことは解析寄りのことまで、たいていのことが書いてあります。

3次元多様体入門
3次元多様体入門

3次元多様体入門

紙の本は絶版になっていて入手困難です。PDF版だけの追補もあります。他の本では書いてないような話題を扱っていて、3次元幾何の貴重な情報源です。

Parametrized Homotopy Theory

本格的なホモトピー論の教科書です。本格的過ぎて、まったく歯が立ちませんわ。パラメータ付き(parametrized)というのは、バンドルやファイバー空間のような状況を言っているようです、よく知らんけど。

最初だけ眺めると、空間のコンビニエント圏(onvenient category)の議論があります。ほかでもコンビニエント圏の話を見たので、けっこう重要な概念かもしれないです。

Noncommutative Geometry: Alain Connes
Noncommutative Geometry

Noncommutative Geometry

コンヌの非可換幾何の教科書です。翻訳本も出てます。幾何と言っても非可換幾何は、通常の幾何と相当に様子が違います。なんか物理っぽい。僕は、全体のオーバービューが書いてあるIntroductionを読んで、不思議な雰囲気を味わうだけ。

圏論

Category Theory in Context
Category Theory in Context (Aurora: Dover Modern Math Originals)

Category Theory in Context (Aurora: Dover Modern Math Originals)

気鋭の圏論家・Riehl女史による解説書。内容は標準的です。トム・レンスターの『ベーシック圏論』とマックレーンのThe Bookの中間くらいのレベルでしょうか。

Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist

このテキストは、昔、圏論勉強会で使ったことがあります。古い本で多少読みにくいかも知れません。でも、型理論、ラムダ計算、圏論の関係についてはシッカリ書いてあります。

Category Theory for Computing Science

コンピューティング・サイエンスを意識しながら圏論を丁寧に解説しています。スケッチ(sketche)の説明があるのは珍しいですね。トポスも説明されています。

Higher Operads, Higher Categories
Higher Operads, Higher Categories (London Mathematical Society Lecture Note Series)

Higher Operads, Higher Categories (London Mathematical Society Lecture Note Series)

高次圏(n-圏)の解説書です。高次圏へのアプローチは矢鱈に色々ありますが、これはオペラッドを使うものです。通常の圏も含めて予備知識も書いてあるので、高次圏の概要を知るには良い本だと思います。

Axiomatic Method and Category Theory
Axiomatic Method and Category Theory (Synthese Library)

Axiomatic Method and Category Theory (Synthese Library)

紙の初版が285ページ、改訂版で300ページですが、PDFは337ページもあります。通常の圏論の本とは毛色が違います*1。科学哲学っぽい雰囲気です。歴史や思想に興味がある人には面白いかも。

Practical Foundations of Mathematics

HTMLで提供されています。PDFに比べて視認性は悪いですが、ハイパーテキストである点は便利です。圏論の本と言っていいでしょう。圏論型理論とか圏論的論理についての解説です。

その他

Geometric Integration Theory
Geometric Integration Theory (Cornerstones)

Geometric Integration Theory (Cornerstones)

幾何積分論(幾何測度論)とは、プラトー問題などを扱う分野のようです。解析はまったく苦手なんで、コメントできません。

Foundations of Algebraic Specification and Formal Software Development

表記のURLはディレクトリインデックスです。章ごとのPDFと全体のPDFが置かれています。題名通り、一般代数(universal algebra)や形式的体系を使った仕様技術について書かれています。インスティチューションについての解説があります。例えば、大乗仏教中観派の話の予備知識が得られます。

Stochastic Integration with Jumps

紙の本とタイトルが違いますが、内容は同じようです。確率微分方程式の話、という以上のことは分かりません、あしからず。

Optimal transport, old and new

最適輸送理論(Optimal Transport Theory)とは「物質をある場所から他の場所へ最小費用で移す」理論だそうです(「最適輸送理論梗概」)。この本は、この分野の定番本みたいです。

著者のヴィラニは「数学界のレディー・ガガ」("The Lady Gaga of mathematics")と呼ばれているそうです。常にクラバットに蜘蛛のブローチという独特なファッション、なかなか強烈です。その姿と話しっぷりはTEDトークで見ることができます。

過去に言及したオンラインの専門書

無料で入手できる本格的(紙なら高額)な理数系専門書15選
  1. Algebraic Topology / Allen Hatcher
    https://www.math.cornell.edu/~hatcher/AT/ATpage.html
  2. Elementary Applied Topology / R. Ghrist
    https://www.math.upenn.edu/~ghrist/notes.html
  3. Category theory for scientists (Old version) / David I. Spivak
    http://arxiv.org/abs/1302.6946
  4. Higher Topos Theory / Jacob Lurie
    http://www.math.harvard.edu/~lurie/papers/highertopoi.pdf
  5. Tensor Categories / Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik
    http://www-math.mit.edu/~etingof/egnobookfinal.pdf
  6. Lectures on tensor categories and modular functor / Bojko Bakalov, Alexander Kirillov Jr
    http://www.math.stonybrook.edu/~kirillov/tensor/tensor.html
  7. Monoidal Functors, Species and Hopf Algebras / Marcelo Aguiar, Swapneel Mahajan
    http://www.math.cornell.edu/~maguiar/a.pdf
  8. Homotopy Theory of Higher Categories / Carlos T. Simpson
    http://arxiv.org/abs/1001.4071
  9. The Blind Spot / Jean-Yves Girard
    http://iml.univ-mrs.fr/~girard/coursang/coursang.html
  10. Bayesian Reasoning and Machine Learning / David Barber
    http://web4.cs.ucl.ac.uk/staff/D.Barber/textbook/090310.pdf
  11. An introduction to measure theory / Terence Tao
    https://terrytao.files.wordpress.com/2011/01/measure-book1.pdf
  12. Towards the mathematics of quantum field theory (An advanced course) / Frederic Paugam
    https://webusers.imj-prg.fr/~frederic.paugam/documents/enseignement/master-mathematical-physics.pdf
  13. Eloquent JavaScript: A Modern Introduction to Programming / Marijn Haverbeke
    http://eloquentjavascript.net/Eloquent_JavaScript.pdf
  14. Advanced R / Hadley Wickham
    http://adv-r.had.co.nz/
  15. Software Engineering for Internet Applications / Eve Andersson, Philip Greenspun, and Andrew Grumet
    http://philip.greenspun.com/seia/
無料で入手できる本格的(紙なら高額)な微分幾何の専門書4選
  1. Functional Differential Geometry / Gerald Jay Sussman, Jack Wisdom, Will Farr
    https://groups.csail.mit.edu/mac/users/gjs/6946/calculus-indexed.pdf
  2. The Convenient Setting of Global Analysis / Andreas Kriegl, Peter W. Michor
    http://www.mat.univie.ac.at/~michor/apbookh-ams.pdf
  3. Synthetic Differential Geometry Second Edition / Anders Kock
    http://home.math.au.dk/kock/sdg99.pdf
  4. Synthetic Geometry of Manifolds / Anders Kock
    http://home.math.au.dk/kock/SGM-final.pdf
英語版無料PDFか、それとも日本語版商業出版物か:圏論と測度論
  1. Basic Category Theory / Tom Leinster
    https://arxiv.org/abs/1612.09375
  2. An introduction to measure theory / Terence Tao (再度)
    https://terrytao.files.wordpress.com/2011/01/measure-book1.pdf

*1:「毛色が違う」は差別表現だ、なんて言う人もいるようですが、三毛猫と黒猫は実際に毛色が違うけど、その事実を指摘すると猫に失礼なの?

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170524

2017-05-23 (火)

型付きラムダ計算 構文論 再入門 2/2: カリー/ハワード対応のために

| 11:49 | 型付きラムダ計算 構文論 再入門 2/2: カリー/ハワード対応のためにを含むブックマーク

型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のために」の続きです。

前回 1/2 の内容:

  1. 予備知識と参考資料
  2. 大きなラムダ計算とは何か
  3. 概要と目標
  4. 集合と写像に関する基礎的事項
  5. 型システム

今回 2/2 の内容:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

疑似ラムダ項の構文

ラムダ項の構文を定義したいのですが、まずはザックリとした構文定義をします。ザックリなので、ここでの定義だけでは不十分です。ここで定義される項(構文的な表現)はちゃんとしたラムダ項ではないので疑似ラムダ項(lambda pseudoterm)と呼びます。なお、「ラムダ項」と「ラムダ式」は原則として同義語ですが、小さなラムダ式をラムダ項と呼ぶことが多いです。

変数(と呼ばれる記号)の集合をVarとします。疑似ラムダ項とは次のようなものです(帰納的な定義)。

  1. [変数] xが変数(x∈Var)ならば、x は疑似ラムダ項である。
  2. [ユニット] !は疑似ラムダ項である。
  3. [適用] E, Fが疑似ラムダ項ならば、E▷F は疑似ラムダ項である。
  4. [ペア] E, Fが疑似ラムダ項ならば、(E F) は疑似ラムダ項である。
  5. [第一成分] Eが疑似ラムダ項ならば、E_1 は疑似ラムダ項である。
  6. [第二成分] Eが疑似ラムダ項ならば、E_2 は疑似ラムダ項である。
  7. [関数抽象] xが変数、Aが型、Eが疑似ラムダ項ならば、λx:A.E は疑似ラムダ項である。
  8. [括弧] Eが疑似ラムダ項ならば、(E) (Eを括弧で囲んだ形)は疑似ラムダ項である。
  9. 以上により定義されたものだけが疑似ラムダラムダ項である。

E▷F とまったく同じ意味(別記法)で F・E も使います。'▷'と'・'で左右が逆になりますが、どっちを使うのも自由です。今後'・'を多く使うでしょうが、'▷'のほうが圏論の図式順記法や絵算との相性がいいです。

レヴィ(Paul Blain Levy)によるCBPV(Call-By-Push-Value)の項言語でも、適用の書き方は「引数 適用記号 関数」の語順です。レヴィは適用記号にバックスラッシュを使っていました。左から右にデータと制御が流れるイメージですね。「Call-By-Push-Valueの不純な関数型言語」参照。

演算子の優先順位は次のようです。演算子の優先順位に頼ると間違いを犯しやすいので、なるべく丸括弧を使いましょう。

優先順位 演算子 演算子形式 結合性 注意
1 _1, _2 後置単項 なし
2 中置二項
2 中置二項 ▷と左右が逆だが同じ
3 (- -) 中置二項 空白が演算子記号

疑似ラムダ項の例をいくつか挙げます。

  1. x
  2. x▷y
  3. y・x (x▷yと同じ)
  4. (x y)
  5. (! x)
  6. ((x y) z)
  7. x_1
  8. ((x y) z)_2
  9. f・(((x y) z)_2)
  10. λx:A.(f・(((x y) z)_2))

記号のインフォーマルな意味を説明しておきます。正式な意味論を述べるわけではなくて、心理的な納得感・安心感が目的です。

  • [ユニット] !は、単元集合1(型の記号はI)の唯一の要素を表す定数記号だと思ってください。Eが0引数関数を表すとき、E・! として評価します。実際のプログラミング言語では、ユニット定数に()を使うことが多いみたいです。
  • [適用] '▷'と'・'は適用(appとapp')を表す中置演算子記号です。'▷'の右、'・'の左に関数オブジェクト(の表現)を置きます。E▷F の値は、Eの評価結果とFの評価結果である関数オブジェクトをappに渡した結果です。適用の記号を省略することはありません
  • [ペア] 空白は関数のペアを作る中置演算子記号です。書き方はLispのリスト記法と同じです。使い方はLispのドットペア記法と同じになります。空白ペアの意味は、関数のデカルト・ペア、または関数の直積です。空白ペアがデカルトペアを表すか直積を表すかは、型証明系(後述)により変わります。
  • [第一成分][第二成分] E_1は、Eの第一成分を意味します。'_1'自体は、第一成分を取り出す後置演算子です。'_2'も同様です。
  • [関数抽象] λx:A. は、型付き変数xによる関数抽象(ラムダ抽象)で、変数xを仮引数とする関数オブジェクトを作ります。
  • [括弧] 曖昧さを避けたり、優先順位を変えるために丸括弧を使います。

疑似ラムダ項Eの自由変数の集合FreeVar(E)は次のように定義します。

  1. xが変数(x∈Var)ならば、FreeVar(x) = {x}
  2. FreeVar(!) = 空集合
  3. E, Fが疑似ラムダ項ならば、FreeVar(E▷F) = FreeVar(E)∪FreeVar(F)
  4. E, Fが疑似ラムダ項ならば、FreeVar((E F)) = FreeVar(E)∪FreeVar(F)
  5. Eが疑似ラムダ項ならば、FreeVar(E_1) = FreeVar(E)
  6. Eが疑似ラムダ項ならば、FreeVar(E_2) = FreeVar(E)
  7. xが変数、Aが型、Eが疑似ラムダ項ならば、FreeVar(λx:A.E) = FreeVar(E)\{x}
  8. Eが疑似ラムダ項ならば、FreeVar((E)) = FreeVar(E)

FreeVar(E)\{x} は、FreeVar(E)から変数xを(あれば)取り除いた集合です。

疑似ラムダ項に対しても、通常の手順によりアルファ変換(alpha conversion)を行えます。アルファ変換は束縛変数をリネームしますが、自由変数のリネームも同様に行えます(リネームで意図せぬラムダ束縛が生じないように注意)。アルファ変換と自由変数のリネームは似てますが、リネーム対象(束縛変数か自由変数か)が違うので区別してください。

ラムダ項の構成と型付け

x:A, y:B のように、変数ごとの型宣言が並んだものをΓ, Δなどのギリシャ文字大文字で表すことにします。この並びのことも型宣言(type declaration)と呼びます。他に、型環境(type environment)とか型コンテキスト(type context)とか呼ぶこともあります。でも、人によって用語法は異なります→「型理論ってば」。

型宣言Γは、変数:型 の形をカンマで区切って並べたものです。変数が重複してはダメで、すべて異なる変数が出現します。Γは空であってもかまいません。Γに出現する変数の集合をVarSet(Γ)とします。

型宣言Γと疑似ラムダ項Eを組にした〈Γ| E〉 を型宣言付き擬似ラムダ項(type-declared lambda pseudoterm)と呼びます。型宣言付き疑似ラムダ項のなかには、不適切なものが含まれています。適切な項とは、型が確定するものです。項の適切さ=項の型付け可能性を定義するために、型判断というものを導入します。

型宣言付き疑似ラムダ項〈Γ| E〉と型Aを組にした 〈Γ| E〉 :A の形を型判断(type judgement)と呼びます。型判断は、「型宣言Γのもとで、ラムダ項Eの型はAである」という主張です。型判断の書き方を変えて、Γ |- E:A とか Γ ⇒ E:A とするとシーケント計算に繋がります。が、今回はシーケント形式は使いません。シーケント形式でのラムダ計算は次の記事に書いています。ラムダ式の構文や推論規則は今回と微妙に違いますが、本質的な差はありません。

最初から正しいと認める型判断を公理型判断(axiom type judgement)、型公理(type axiom)、あるいは混乱の心配がなければ単に公理(axiom)と呼びます。以下に公理型判断のパターンを列挙します。

  • [変数] Γのなかに x:A が含まれるならば、〈Γ| x〉:A は公理である。
  • [ユニット] 〈Γ| !〉:I は公理である。Γは任意で、空でもよい

型推論規則(type inference rule)は、型判断から新しい型判断を作り出す規則です。型推論規則は、次のような型推論図(type inference (rule) figure)で記述します。「推論図」、「推論規則」、「規則」という言葉は同義語として使われるので注意してください。

(適用の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
〈Γ| E〉:A  〈Δ| F〉:A->B
 --------------------------[適用]
   〈Γ, Δ| E▷F〉:B

 〈Γ| E〉:A 〈Γ| F〉:B
 ------------------------[デカルトペア]
   〈Γ| (E F)〉:A×B

  〈Γ| E〉:A×B
 ----------------[第一成分]
 〈Γ| E_1〉:A

 〈Γ| E〉:A×B
 ----------------[第ニ成分]
 〈Γ| E_2〉:B

 〈x:A, Γ| E〉:B
 ------------------------[関数抽象]
  〈Γ| λx:A.E〉:A->B

型推論規則は、ラムダ項の構文構成規則(term forming rule)と、型付け規則(typing rule)の両方を兼ねています。項の構成と同時にその型も与えているのです。

変数と定数(!は定数)は公理で規定し、他の構文的構成は推論規則で表現しています。しかし、後で出てくる代入(substitution)を前提にして、推論規則を公理に移すこともできます。例えば、ペアの構成を公理にできます。

  • [ペア] Γのなかに x:A と y:B がこの順で(x:A が先で)含まれるならば、〈Γ| (x y)〉:A×B は公理である。

型推論図を積み重ねた図形を型証明図(type proof figure)と呼びます。しばしば、単に証明図ともいいます。次は型証明図の例です。☆は、直下が型公理であることを示す目印です。

     ☆                     ☆
 -----------[変数] -------------------[変数]
〈x:A| x〉:A     〈f:A->B| f〉:A->B                 ☆
 --------------------------------------[適用]  -----------------[変数]
        〈x:A, f:A->B| x▷f〉:B                〈g:B->C| g〉:B->C
 -------------------------------------------------------------------[適用]
              〈x:A, f:A->B, g:B->C| (x▷f)▷g〉:C
            ----------------------------------------[関数抽象]
            〈f:A->B, g:B->C| λx:A.(x▷f)▷g〉:A->C

型証明図の最下段に現れる型判断を、その型証明図の結論(conclusion)と呼びます。最上段がすべて星印(☆)である型証明図は閉じた型証明図(closed type proof figure)と呼びます。閉じた型証明図の結論となる型判断は型証明可能(type provable)だといいます。混乱の恐れがないなら単に証明可能(provable)でもいいです。

型宣言付き疑似ラムダ項〈Γ:E〉が、〈Γ|E〉:A という型判断と、この型判断を結論とする閉じた型証明図を持つとき、型付け可能(typable)と呼びます。次の2つの言い方は同じ意味です。

  • 型判断 〈Γ|E〉:A が型証明可能である。
  • 〈Γ|E〉は型付け可能で、ΓのもとでのEの型はAである。

型宣言付き疑似ラムダ項〈Γ|E〉が型付け可能なとき、それを型付きラムダ項(typed lambda term)、または型付きラムダ式(typed lambda expression)と呼びます。文脈から分かるなら、「型付き」を省略して単にラムダ項、ラムダ式でもかまいません。

〈Γ| E〉が型付きラムダ式のとき、全体を大きなラムダ式、内部にある疑似ラムダ項Eを小さなラムダ式とも呼びます。この呼び名は、内部のEだけでは不十分なことを強調するために使っています。小さなラムダ式だけでは、型付け可能かどうかは分かりません。

[適用]推論規則を、次のデカルト適用(Cartesian application)に置き換えたほうが理論的な扱いは楽になります。[適用]でも[デカルト適用]でも、どっちを採用しても証明系の能力は変わりません。

〈Γ| E〉:A  〈Γ| F〉:A->B
 --------------------------[デカルト適用]
   〈Γ| E▷F〉:B

しかし、[デカルト適用]を使う前に型宣言を揃えるのがめんどくさいので、[適用]を採用しました。

大きなラムダ式のアルファ変換

例として次の大きなラムダ式を考えてみましょう。

  • 〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉

この大きなラムダ式は、次の型判断を持ちます(型判断を持つ型宣言付き疑似ラムダ項を、大きなラムダ式と呼ぶのでした)。

  • 〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉:B->C

この型判断の根拠(型証明図)は次です。

                        ☆                         ☆
                   ------------[変数]  -----------------------------[変数]
    ☆             〈x:A| x〉:A        〈f:A->(B->C)| f〉:A->(B->C)
 -----------[変数] -------------------------------------------------[適用]
〈y:B| y〉:B       〈x:A, f:A->(B->C)| f・x〉:B->C
 --------------------------------------------------[適用]
      〈y:B, x:A, f:A->(B->C)| (f・x)・y〉:C
      -------------------------------------------[関数抽象]
      〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉:B->C

大きなラムダ式のインフォーマルな解釈は写像です。型は集合だと思うと、〈x:A, f:A->(B->C)| λy:B.(f・x)・y〉は次の写像を表します。

  • x∈A, f∈(A->(B->C) に対して、式 λy:B.(f・x)・y で表される(B->C)の要素を対応させる。

写像の表現としては、入力変数の名前はどうでもいいので、〈s:A, k:A->(B->C)| λy:B.(k・s)・y〉でも同じ写像を表します。この事情を考慮して、大きなラムダ式にもアルファ変換を定義します。大きなラムダ式のアルファ変換は、内部の小さなラムダ式に対して自由変数のリネームになります。その点を注意すれば、要領は通常のアルファ変換と同じです。混乱しそうなときは、大きなアルファ変換という言葉を使います。

大きなアルファ変換は、必要なときにいつでも実行してかまいません。例えば[適用]推論規則には、「適用の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない」という制限がついてましたが、事前にアルファ変換をするなら、この制限はないも同然です。大きなアルファ変換を明示的に書くときは、次の推論図を使います。

  〈Γ| E〉:A
  ---------------[アルファ変換]
  〈Γ'| E'〉:A

Γ'とE'は、変数をリネームした結果

今後は、大きなアルファ変換で移れる大きなラムダ式は同一視することにします。大きなアルファ変換による同値関係の商集合を考える、とも言えます。

大きなラムダ式の構造規則

推論規則の上段・下段を比べると、関数抽象以外では、上段の型宣言はそのまま下段に引き継がれます。関数抽象では、一番左の個別宣言が取り除かれます。現状では、個別宣言の順序を変えたり、個別宣言を足すことはできません。これでは困ります。

そこで、大きなラムダ式の型宣言部分を操作する規則を導入します。それらの規則を構造規則(structural rule)と呼びます。構造規則も型判断に対する推論図として表現します。構造規則の名前は、直積以外はシーケント計算にちなみます。

  • (interchange)
  • (thinning)
  • (contraction)
  • 直積(direct product)
 〈Γ, x:A, y:B, Δ| E〉:C
 --------------------------[換]
 〈Γ, y:B, x:A, Δ| E〉:C

 〈Γ| E〉:A
 ---------------------[増]
 〈Δ, Γ, Π| E〉:A

 〈Δ, x:A, y:A, Π| E〉:C
 --------------------------[減]
 〈Δ, x:A, Π| E[x/y]〉:C

 〈Δ, x:A, y:B, Π| E〉:C
 --------------------------------------[直積]
 〈Δ, p:A×B, Π| E[p_1/x, p_2/y]〉:C

[増]構造規則を使う前提で、型公理を減らすことができます。

  • [変数] 〈x:A| x〉:A
  • [ユニット] 〈| !〉:I

別にうれしくないので型公理を減らしませんけどね。

[換]構造規則を何度か使うと、型宣言の順序を自由に入れ替えることができます。入れ替えても型判断はそのまま成立する(あるいは、やっぱり成立しない)ので、型判断における型宣言の順序はどうでもいいことが分かります。

[直積]構造規則は、シーケント計算では論理規則に分類されています。論理における構造規則と論理規則の区分は、ラムダ計算の構文論/意味論の観点からは重要ではありません。割とどうでもいい区分です。なお、ラムダ計算とシーケント計算の関係は、次の記事でも触れています。

マルチ代入

E1, ..., En が小さなラムダ式、x1, ..., xn は変数とします。小さなラムダ式Fに対して、Fのなかに出現する自由変数xi(それがあれば)をEi(i = 1, ..., n)で置き換えた式を、

  • F[E1/x1, ..., En/xn]

と書きます(書き方については「型推論に関わる論理の概念と用語 その6:substitutionの記法」参照)。これは、同時置き換えであって、変数1個ずつ順番に置き換えるわけではありません。複数の変数に対する同時置き換えをマルチ代入(multi-substitution)と呼ぶことにします。「マルチ」を使ったのは、複圏(multicategory = operad)と関係しているから、という理由もあります。代入(置き換え)で、意図せぬラムダ束縛が生じないように注意する点は自由変数のリネームと同様です。

マルチ代入は、代入(置き換え)の並列実行だと言っていいでしょう。しかし、並列実行は直列逐次実行でシミュレートできます。何も考えずに逐次実行すると、奇妙な結果になるので、適切に変数のリネームをする必要がありますが、個々の変数出現を1つずつ順番に処理することでマルチ代入をシミュレートできます。

置き換え操作は、型を考慮せずに実行することができますが、型を考慮した正しい置き換えのルールは、次の型推論図で示されます。この推論図(推論規則)もマルチ代入と呼びます。

(マルチ代入の条件: VarSet(Γ1), ..., VarSet(Γn), VarSet(Δ) は、どの2つも共通部分が空(disjoint)でなくてはならない)
 〈Γ1| E1〉:A1
  ...
 〈Γn| En〉:An
 〈x1:A1, ..., xn:An, Δ| F〉:B
  -------------------------------------------[マルチ代入]
 〈Γ1, ..., Γn, Δ| F[E1/x1, ..., En/xn]〉:B

横線の上段は、n個の型判断を横に並べたものですが、スペースとレイアウトの関係上縦に並べています。Δは、代入で手付かずの変数が含まれる型宣言です。[マルチ代入]推論規則はΔを許すので、変数すべてを置き換える必要はありません。参考に、[マルチ代入]推論規則に対応するストリング図変形を挙げておきます。

Δが空のときはフル・マルチ代入(full multi-substitution)といいます。

(フル・マルチ代入の条件: VarSet(Γ1), ..., VarSet(Γn) は、どの2つも共通部分が空(disjoint)でなくてはならない)
 〈Γ1| E1〉:A1
  ...
 〈Γn| En〉:An
 〈x1:A1, ..., xn:An| F〉:B
  -------------------------------------------[フル・マルチ代入]
 〈Γ1, ..., Γn| F[E1/x1, ..., En/xn]〉:B

推論規則としての[マルチ代入]と[フル・マルチ代入]は同等(どっちを採用しても同じ)ですが、実用上の便利さからマルチ代入を採用します。

型証明系TPS1

今まで述べたことの中間まとめをしておきましょう。

疑似ラムダ項Eと型宣言Γの構文を説明して、それらの組み合わせとして型判断〈Γ| E〉:A (Aは型)を導入しました。型判断は「型宣言Γのもとで、ラムダ項Eの型はAである」という主張です。その主張が正しいことを保証するメカニズムが型証明系(type proof system)です。

一般に論理的証明系(演繹系)は、証明すべき主張を表現する(sentence)の集合、最初から正しいと(天下りに)決めた文である公理(axiom)の集合、新しい文を作り出す手順を示す推論規則(inference rule)の集合からなります。今回の型証明系では、文は型判断であり、公理の集合と推論規則の集合は次のように与えられました。

  1. [変数]公理
  2. [ユニット]公理
  3. [適用]推論規則
  4. [デカルトペア]推論規則
  5. [第一成分]推論規則
  6. [第ニ成分]推論規則
  7. [関数抽象]推論規則
  8. [マルチ代入]推論規則

補助的に、(大きな)アルファ変換と構造規則があります。

  1. アルファ変換
  2. [換]構造規則
  3. [増]構造規則
  4. [減]構造規則
  5. [直積]構造規則

推論規則/アルファ変換/構造規則の組み合わせが証明ですが、証明は証明図という図形で表します。

今回我々が定義した型に関する証明系をTPS1(Type Proof System 1 固有名詞)と呼ぶことにします。いちおうのまとまりが付いたので、TPS1という名前を付けましたが、TPS1は型付きラムダ計算を展開するには機能不足だし、意味論がないので文字通り意味不明だと注意しておきましょう。後でもう少し拡張します。圏論的意味論もいずれ述べる予定です(今回は正式な意味論はなし)。

型判断をα, βなどのギリシャ文字小文字で表すことにします。型判断αがTPS1において証明可能なことを、記号的に次のように書きます。

  • |-TPS1 α

証明図の最上段に現れる型判断を、その証明図の仮定(assumption)と呼びます。星印が上に位置する公理は仮定ではありません。TPS1において、型判断α1, ..., αnを仮定して型判断βが相対証明可能(relatively provable)とは次の意味です。

  • βを結論として、α1, ..., αn の全部または一部を仮定として持つTPS1の証明図が存在する。

記号的には次のように書きます。

  • α1, ..., αn |-TPS1 β

相対証明可能なことも単に証明可能性という場合が多いです。

メタな記号 |-TPS1 を定義したのですが、このようなメタな定義でよいのか? は議論の余地があります。上記の定義では、証明系が仮定を使うとき、「仮定の一部を捨ててもよい」「1つの仮定を何度も使ってよい」「仮定をどの順番で使ってもよい」などを暗黙に前提しています。つまり、仮定の“集まり”を集合だと前提していて、リストやマルチセットは考えてません。

メタな概念である「証明可能性」をさらに形式化して扱うときは、このへんのところをもっと検討する必要があります。

TPS1における代入消去と型付けの一意性

大きなラムダ式〈Γ| E〉は、定義により型付け可能です。つまり、TPS1で証明可能な型判断〈Γ| E〉:A があります。しかし、型Aが一意に決まるかどうかは明らかではありません。

TPS1において、型判断 〈Γ| E〉:A が証明可能なとき、その証明図がひとつとは限りません。例えば、 〈| (! !)〉:I×I は次のようにして証明できます。

     ☆                    ☆
 ----------[ユニット]  ----------[ユニット]
 〈| !〉:I             〈| !〉:I
 ----------------------------------[デカルトペア]
        〈| (! !)〉:I×I

これより短い証明図はありませんが、長い証明図は書けます。例えば:

[ユニット2つ]は次の図とする。
     ☆                    ☆
 ----------[ユニット]  ----------[ユニット]
 〈| !〉:I             〈| !〉:I


                  ☆                      ☆
            ----------------[変数]  ----------------[変数]
           〈x:I, y:I| x〉:I       〈x:I, y:I| y〉:I
            ----------------------------------------------[デカルトペア]
 [ユニット2つ]     〈x:I, y:I| (x y)〉:I×I
 ---------------------------------------------[マルチ代入]
             〈| (! !)〉:I×I

2つの証明図に対応するグラフ(ツリー)は次のようになります。

このような冗長で回り道をした証明ができてしまうのは、マルチ代入規則があるせいです。マルチ代入規則を除外して、他の規則だけにすると(多少の工夫もして)、型判断に対する証明図が(あれば)ひとつだけになります。

しかし、今まで在った推論規則をなくしてしまうので、今まで証明できていた型判断が証明できなくなるリスクがあります。幸いなことに、この心配は無用で、次のメタ定理が成立します。

  • ある型判断がTPS1で証明可能なとき、マルチ代入規則なしでも証明できる。

もっと具体的に言えば:

  • ある型判断のTPS1の証明図があるとき、その証明図を変形して、マルチ代入規則なしの証明図を構成できる。

この事実は、シーケント計算のカット消去定理(Cut elimination theorem)の対応物です。代入消去定理(Substitution elimination theorem)と呼びましょう。

代入消去により得られた証明図は、それ以上は短くできない形をしているので一種の正規形(normal form)となります。正規形の証明図=マルチ代入なしの証明図に限定すれば、型判断と証明図が1:1に対応します。型判断がなんにしろ証明可能なら、それは唯一の正規形証明図を持ちます。

正規形証明図の一意性から、型付けの一意性が従います。

  • 大きなラムダ式〈Γ| E〉が型付け可能なら、その型は一意的に決まる。

適切なアルゴリズムにより、型と共に型付けの証拠である正規形証明図も一意的に得られます。これは大変に都合の良い性質で、TPS1はラムダ計算の構文的基盤として適切であると言っていいでしょう。

証明図に対する代入消去は、代入計算の実行を意味するので、代入消去のアルゴリズムは、“証明図を実行する手順”=“証明図のインタプリタ実装”を与えます。証明図の実行結果である正規形証明図はメタレベルの“値”と解釈されます。つまり、TPS1の証明図をプログラム・ソースコードとするプログラミング・システムがあると考えることができるのです。

ラムダ計算のポリ化: 型証明系TPS2

今まで、型宣言付き疑似ラムダ項は〈Γ| E〉という形で、内部に必ず1個の疑似ラムダ項を持っていました。これを一般化して、内部に複数個の疑似ラムダ項を書いていいことにします。次のような形です。

  • 〈Γ| E1, ..., En〉 (n ≧ 1)

この形を、型宣言付きポリ疑似ラムダ項(type-declared lambda poly-pseudoterm)と呼びます。名前が長すぎるので、ポリ・ラムダ式(poly-lambda expression)とも呼ぶことにします。「ポリ」を付けたのは、多圏(polycategory)と関係するからです。

疑似ラムダ式の並びをΦ, Ψなどのギリシャ文字大文字で表すことにすると、ポリ・ラムダ式は〈Γ| Φ〉という形になります。並び(リスト)の長さをlength(-)と書くことにして、ポリ・ラムダ式の(width)と余幅(cowidth)を次のように定義します。

  • width(〈Γ| Φ〉) = length(Γ)
  • cowidth(〈Γ| Φ〉) = length(Φ)

width(〈Γ| Φ〉) = 0 はあり得ますが、cowidth(〈Γ| Φ〉) ≧ 1 です(cowidth(〈Γ| Φ〉) = 0 は今のところ認めません、後で許容するように変更しますが)。任意のn, m(n ≧ 0, m ≧ 1)に対して、width(〈Γ| Φ〉) = n, cowidth(〈Γ| Φ〉) = m であるポリ・ラムダ式が存在します。

ポリ・ラムダ式に対するポリ型判断(poly type judgement)は、次の形です。

  • 〈Γ| E1, ..., En〉:A1, ..., Am

ポリ型判断の幅と余幅もポリ・ラムダ式の場合と同様に定義できます。

ポリ型判断の証明可能性に関して、次が成立することが要請されます。

  1. n = 1 のとき、〈Γ|E〉:A が証明可能かどうかは、既にTPS1で定義されている通り。
  2. n ≧ 2 のとき、〈Γ| E1, ..., En〉:A1, ..., An が証明可能なのは、〈Γ| E1〉:A1, ..., 〈Γ| En〉:An がすべてTPS1で証明可能なとき。

二番目の要請を、推論図として表現すると、次のようになります。

 〈Γ| E1〉:A1
   ...
 〈Γ| En〉:An
 ------------------------------[デカルト併合]
 〈Γ| E1, ..., En〉:A1, ..., An

この推論図は、デカルト・タプルの構成法と似てるので、デカルト併合(Cartesian merge)と呼びます。参考に、[デカルト併合]推論規則に対応するストリング図変形を挙げておきます。

ポリ型判断に対して[マルチ代入]推論規則はうまく機能しないので、ポリ型判断に関する代入規則であるポリ代入(poly substitution)を導入します。

(ポリ代入の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
 〈Γ| E1, ..., En〉:A1, ..., An
 〈x1:A1, ..., xn:An, Δ|Ψ〉:B1, ..., Bn
 --------------------------------------------------------[ポリ代入]
 〈Γ, Δ| Ψ[E1/x1, ..., En/xn]〉:B1, ..., Bn

ここで、Ψ[E1/x1, ..., En/xn] は、リストΨに含まれるすべての疑似ラムダ項にマルチ代入[E1/x1, ..., En/xn]を施したリストを意味します。参考に、[ポリ代入]推論規則に対応するストリング図変形を挙げておきます。

上記の推論図において、Δが空のときはフル・ポリ代入(full poly-substitution)と呼びます。

ポリ型判断を扱う新しい型証明系TPS2を次のように定義します。

  1. TPS2の文は、ポリ型判断だとする。この定義より、(TPS1の文の集合) ⊆ (TPS2の文の集合)。
  2. TPS2の公理の集合は、TPS1の公理の集合と同じ。
  3. TPS2の推論規則(推論図)の集合は、TPS1の推論規則(推論図)に[デカルト併合]を加え、[マルチ代入]を[ポリ代入]と交換したもの。
  4. TPS2の推論図として、TPS1の構造規則(の推論図)もそのまま採用する。推論規則が冗長になる(不要なものまで入る)が気にしない。

TPS1とTPS2に関して、次のメタ定理が成立します。

  1. 〈Γ|E〉:A がTPS1で証明可能ならば、TPS2でも証明可能である。(自明)
  2. 〈Γ|E〉:A がTPS2で証明可能ならば、TPS1でも証明可能である。(非自明)
  3. 〈Γ| E1〉:A1, ..., 〈Γ| En〉:An がすべてTPS1で証明可能ならば、〈Γ| E1, ..., En〉:A1, ..., An がTPS2でも証明可能である。(自明)
  4. 〈Γ| E1, ..., En〉:A1, ..., An がTPS2で証明可能ならば、〈Γ| E1〉:A1, ..., 〈Γ| En〉:An はすべてTPS1でも証明可能である。(非自明)

これらのメタ定理の証明(証明系を外から見てのメタレベルの証明)は、もう少し準備して組み合わせ的・帰納的議論をする必要があります。今回は割愛します。

TSP2の証明可能性がTSP1での議論に帰着できるので、ポリ・ラムダ式の型付けの一意性が言えます。

もうひとつの型証明系TPS3

TPS1は、単一のラムダ式の型付けや代入計算を行うのに便利です。TPS2は、複数のラムダ式を一度に扱うために導入しました。TPS2の1個の型判断(ポリ型判断)は、TPS1の複数の型判断をまとめただけと言えます。

さて、大きなラムダ式の圏論的な扱いに適した型証明系としてTPS3を導入します。まず、TPS3では、〈Γ|〉という形の大きなラムダ式を認めます。TPS2における型は、単一型の非空リストでしたが、TSP3では空リスト()を認めます。これに伴い型判断(ポリ型判断)の構文も拡張します。

型証明系→ TPS1 TPS2 TPS3
型判断の幅 n n ≧ 0 n ≧ 0 n ≧ 0
型判断の余幅 m m = 1 m ≧ 1 m ≧ 0
単一の型 長さ1以上の型のリスト 任意長の型のリスト

Γは空も許す型宣言の並び、Φは空も許す型宣言の並び、A1, ..., An を空(n = 0)も許す型の並びとして、TPS3の型判断は、〈Γ| Φ〉:A1, ..., An の形です。3種類の並び(リスト)から構成されますが、並びの長さに何の制限もありません

型証明系としてのTPS3を定めるために、型公理と型推論規則を決めましょう。TPS2で使った以下の型公理/型推論規則はそのまま使い続けます。

  1. [変数]公理
  2. [ユニット]公理
  3. [適用]推論規則
  4. [第一成分]推論規則
  5. [第ニ成分]推論規則
  6. [関数抽象]推論規則

(大きな)アルファ変換も使います。構造規則は廃止します。

TSP3では次の公理を追加します。

  • [空] 〈Γ|〉:()

小さなラムダ式は無し、型は空リストです。Γは任意の型宣言です。特に、〈|〉:() は型公理です。

[デカルトペア]推論規則と[ポリ代入]推論規則、[デカルト併合]推論規則は、対応する別な規則と入れ替えます。対応する別な規則の名称は、モノイドペア(monoidal pair)、フル・ポリ代入(full poly-substitution)、モノイド併合(monoidal merge)です。

(モノイドペアの条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
 〈Γ| E〉:A 〈Δ| F〉:B
 ------------------------[モノイドペア]
   〈Γ, Δ| (E F)〉:A×B


 〈Γ| E1, ..., En〉:A1, ..., An
 〈x1:A1, ..., xn:An| Ψ〉:B1, ..., Bn
 --------------------------------------------------------[フル・ポリ代入]
 〈Γ| Ψ[E1/x1, ..., En/xn]〉:B1, ..., Bn


(モノイド併合の条件: VarSet(Γ)∩VarSet(Δ) は空でなくてはならない)
  〈Γ| Φ〉:A1, ..., An
  〈Δ| Ψ〉:B1, ..., Bm
   -------------------------------------[モノイド併合]
  〈Γ, Δ| Φ, Ψ〉:A1, ..., An, B1, ..., Bm

型証明系TPS3を次のように定義します。

  1. TPS3の文は、空を許すポリ型判断だとする。この定義より、(TPS2の文の集合) ⊆ (TPS3の文の集合)。
  2. TPS3の公理の集合は、TPS2の公理の集合に、[空]公理を追加したもの。
  3. TPS3の推論規則(推論図)の集合は、TPS2の推論規則(推論図)の[デカルトペア]、[ポリ代入]、[デカルト併合]をそれぞれ、[モノイドペア]、[フル・ポリ代入]、[モノイド併合]に入れ替えたもの。
  4. TPS2の構造規則(それはTPS1の構造規則)は採用しない。TPS3では、構造規則は不要。

念のため、TPS3の公理/推論規則を列挙しておきます。'*'はTPS2から変更しているものです。

  1. [変数]公理
  2. [ユニット]公理
  3. [空]公理 *
  4. [適用]推論規則
  5. [モノイドペア]推論規則 *
  6. [第一成分]推論規則
  7. [第ニ成分]推論規則
  8. [関数抽象]推論規則
  9. [フル・ポリ代入]推論規則 *
  10. [モノイド併合]推論規則 *
  11. アルファ変換

TPS3に関して、次のメタ定理が成立します。

  • TPS2で証明可能なポリ型判断はTPS3でも証明可能である。
  • TPS3で証明可能な余幅が0でないポリ型判断はTPS2でも証明可能である。

上記メタ定理の証明も割愛します。

TPS3の証明可能性がTPS2に帰着できるので、TPSでもポリ・ラムダ式の型付けの一意性が言えます。

LLEの定義

型証明系TPS3を定義したのは、TPS3が圏LLE(前回の「概要と目標」参照)を定義する道具に便利だからです。(実際の型証明に使うなら、TPS2のほうが便利でしょう。)

ポリ・ラムダ式〈Γ| Φ〉がTPS3で型付け可能なとき、そのポリ・ラムダ式を、あらためて大きなラムダ式と呼びます。今ここで「大きなラムダ式」の意味を拡張したわけです。すべての大きなラムダ式からなる集合をLLEとします。

大きなラムダ式αが、〈x1:A, ..., xn:An| E1, ..., En〉の形をしているとき、定義によりこれは型付け可能なので、次のポリ型判断がTPS3で証明可能です。

  • 〈x1:A, ..., xn:An| E1, ..., En〉:B1, ..., Bm

ここで、B1, ..., Bm は一意的に決まります。この事実を使って、大きなラムダ式αの域(domain)と余域(codomain)を次のように定義します。大きなラムダ式には余域が一意に決まることがポイントです。

  • dom(α) = (A1, ..., An)
  • cod(α) = (B1, ..., Bm)

dom(α)もcod(α)も型の並び(リスト)です。型の集合をType、型のリストの集合をType*とすれば、写像として、

  • dom:LLE→Type*
  • cod:LLE→Type*

となります。

(A1, ..., An)∈Type* とするとき、(A1, ..., An)に対する恒等ラムダ式(大きなラムダ式)は次のように定義できます。

  • idA1, ..., An = id(A1, ..., An) = 〈x1:A, ..., xn:An| x1, ..., xn

以上で、dom, cod, idが定義できました。LLEとType*を圏に仕立てるには、圏の結合(composition)が必要です。結合は、フル・ポリ代入によって定義します。cod(α) = (B1, ..., Bm), dom(β) = (B1, ..., Bm) のとき、α;βは次の推論図で定義されます。

  α    β
 -----------[フル・ポリ代入]
    α;β

次の圏の条件を示せます。

  1. dom(idA1, ..., An) = (A1, ..., An)
  2. cod(idA1, ..., An) = (A1, ..., An)
  3. cod(α) = dom(β) ならば、α;β が定義できる。
  4. dom(α;β) = dom(α)
  5. cod(α;β) = cod(β)
  6. (α;β);γ = α;(β;γ)
  7. idA1, ..., An;α = α
  8. α;idB1, ..., Bn = α

結合法則 (α;β);γ = α;(β;γ) 以外は自明だと思います。結合法則は、ポリ代入に関するメタ定理です。

以上により、LLEを射の集合、Type*を対象の集合とする圏LLEが定義できました。

LLEのモノイド構造

LLEにはモノイド構造が入ります。それをこの節で述べます。LLEのモノイド積の記号を□とします。

まず、LLEの対象に対するモノイド積を定義します。(A1, ..., An), (B1, ..., Bm)∈Type* に対して、(A1, ..., An)□(B1, ..., Bm) は連接で定義します。

  • (A1, ..., An)□(B1, ..., Bm) = (A1, ..., An, B1, ..., Bm)

Type*は、□をモノイド演算、空リスト()を単位元とするモノイドとなります。

LLEの射(大きなラムダ式)α, βに対しては、α□βを次の推論図で定義します。

  α   β
 ----------[モノイド併合]
   α□β

(LLE, □, ())は厳密モノイド圏になります。そのことを示すには、次の等式群を確認します。

  1. dom(α□β) = dom(α)□dom(β)
  2. cod(α□β) = cod(α)□cod(β)
  3. id(A1, ..., An)□(B1, ..., Bm) = (idA1, ..., An)□(idB1, ..., Bm)
  4. (α;β)□(γ;δ) = (α□γ);(β□δ)
  5. (α□β)□γ = α□(β□γ)
  6. α□id() = id()□α = α

交替律 (α;β)□(γ;δ) = (α□γ);(β□δ) は、(α□id);(id□β) = (id□β);(α;id) という簡略な形でもいいので、これらの証明は難しくありません。モノイド演算□が、列の連接に過ぎないので事情が非常に簡単になっています。繰り返し注意しますが、大きなアルファ変換は必要なら自動的に実行されると考えます。

ラムダ式の変換と同値に関する注意

ここまでの話では、ラムダ計算では非常に重要であるベータ変換やイータ変換、それらの変換により導入されるラムダ式の同値性が出てきてません。これらの変換と同値性は、構文論だけだと解釈が難しいでしょう。

大きなラムダ式α, βがあって、適切な意味論的解釈〚-〛があるとき、〚α〛 = 〚β〛 ならば、大きなラムダ式αとβは同値だと定めて α ≡ β と書くことにします。メタな命題である α ≡ β を、形式的に証明できる証明系(形式的体系)はどんなものか? と考える必要があります。

同値性に関する証明系は、TPS*より上位の体系になります。仮に、同値性に関する証明系をEPS(equivalence proof system)とすると、次のようなメタ命題のあいだの関係が問題になります。

  • [EPS証明可能性] 形式化された同値性 α ≡ β が形式的証明系EPSで証明可能である。
  • [意味論的同値] 意味論的解釈〚-〛に関して、〚α〛 = 〚β〛 が成立する。

EPSがマトモな証明系であるためには、次(健全性)が要求されます。

  • α ≡ β がEPSで証明可能ならば、〚α〛 = 〚β〛 が成立する。

ベータ同値やイータ同値はEPSの公理となる性質です。EPSに必要な公理はベータ同値/イータ同値だけではなくて、実は色々な公理が要請されます。例えば、〈u:I| u〉と〈u:I| !〉は同値であるべきです。

おわりに

ラムダ式の意味論やラムダ式の同値性の議論が、型付きラムダ計算論の中核でしょう。今回説明したことは、ラムダ式の型付けと代入計算だけ、つまり、圏論的意味論を展開する土台になる構文論の部分です。

型付きラムダ計算の圏論的意味論が目指すべきランドマークは、次の2つのメタな命題が同値であることを主張する“完全性定理”です。

  • |-EPS (α ≡ β)
  • CCCC.( C |= (α ≡ β) )

EPSはラムダ式の同値性に関する証明系で、CCCはすべてのデカルト閉圏(Cartesian Closed Categories)からなるクラスです。C |= (α ≡ β) は、Cに値を持つ解釈(意味関手)〚-〛C に関して 〚α〛C = 〚β〛C であることを意味します。

型付きラムダ計算に関する手法や結果を、このビッグピクチャーのなかに位置付けると、けっこう納得感があると思います。今回の一連の話も、ビッグピクチャーのピースを眺めたことになります。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170523

2017-05-22 (月)

型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のために

| 09:25 | 型付きラムダ計算 構文論 再入門 1/2: カリー/ハワード対応のためにを含むブックマーク

カリー/ハワード対応への障壁」において、カリー/ハワード対応(Curry-Howard correspondence/isomorphism)をうまく説明するのは難しい、という話をしました。その記事の最後の一言は:

いまだベストと思える説明に届かず。

その後も、ベスト(に近い)説明とはどんなものかと考えています。以前から僕は「大きなラムダ計算」という方法を使っているのですが、これをベースにするのがやはり良いように思えます。大きなラムダ計算は型付きラムダ計算の定式化のひとつです。大きなラムダ計算をまともに紹介したことがなかったので、この記事と引き続く記事の2回に分けて説明します(続く第2回もほぼ書き終えていますよ ^_^)。

この2回の記事で、大きなラムダ計算の構文的・証明論的側面を紹介します。ラムダ式への型付けアルゴリズムを形式的証明と捉えて、その証明系の性質を調べます。カリー/ハワード対応を意識してのことです。証明系に関するメタ定理は、ラムダ式と証明図の構造に沿った帰納法で(メタに)証明できますが、煩雑で若干テクニカルなのでだいたい省略します(いつかちゃんと書くかも)。

「型付きラムダ計算を、構文だけで理解するのは苦しい」と思うので、集合圏におけるインフォーマルな意味論にも少しだけ触れます。少数ですが、複圏/多圏のストリング図も(次回に)載せます。本格的な意味論や絵算(pictorial/graphical/diagrammatic calculation)は展開しませんが、単なる構文解説だけよりは実感が増すと思います。

今回 1/2 の内容:

  1. 予備知識と参考資料
  2. 大きなラムダ計算とは何か
  3. 概要と目標
  4. 集合と写像に関する基礎的事項
  5. 型システム

次回 2/2 の内容:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

予備知識と参考資料

ゼロからのラムダ計算入門には、10年前(2007年)に書いた一連の記事が、今でも役立つと思います。

  1. JavaScriptで学ぶ・プログラマのためのラムダ計算プログラミング言語JavaScriptを引き合いに出して、ラムダ計算をインフォーマルに説明しています。意図的ではありますが、関数抽象を(狭い意味の)「ラムダ式」と呼んだり、通例(「関数を引数に適用する」)とは逆の表現「引数を関数に適用する」をしているので注意してください。
  2. JavaScriptで学ぶ・プログラマのためのラムダ計算 問題集 : すぐ上の記事に対する練習問題集です。
  3. 絵を描いて学ぶ・プログラマのためのラムダ計算 : ラムダ項の構文解析木を使ってベータ変換を解説しています。なお、この過去記事で使っている絵はベータ変換の可視化が目的で、圏論ベース絵算のストリング図ではありません。

型無しラムダ計算の構文とベータ変換(簡約)を簡潔にまとめた記事として、id:tarao(たらお)さんによる次があります。

僕は、アルファ変換について説明してない(予告して不履行)ですが、アルファ変換はけっこう厄介です(ラムダ計算 - Wikipedia)。アルファ変換を知るには、id:sumii(住井)さんの次のテキストの1.5節あたりまで読むのがいいと思います。

ちなみに、上記テキストで"typing"の訳語が「型つけ」なのですが、ナルホド! 口頭でも「片付け」と混同しなくて良いですね。

型付きラムダ計算とデカルト閉圏の関係は次の記事達に書いています。解説というより、雰囲気を伝える“お話”です。興味があれば眺めてみてください。

大きなラムダ計算とは何か

型付きラムダ計算のラムダ式は、変数の型がハッキリしてないとダメなんです。ですから、λx.(g・(f・x)) のような式(ドット'・'は適用だとする)だけ出してもダメです。x, f, g の型を明示する必要があります。型の明示には型宣言を使うことにします*1。A, B, Cを型(の名前)だとして次のように宣言します。

  1. xの型は、A
  2. fの型は、AからBへの関数型
  3. gの型は、BからCへの関数型

これらの宣言を記号的に次のように書きます。

  1. x:A
  2. f:A->B
  3. g:B->C

'->'は関数型を作る記号で、普通の矢印'→'じゃなくて、ハイフンと不等号です。矢印'→'は他でも多用されるので記号を変えました。[A, B] という書き方も多いですが、ブラケットも他の目的で使うので、関数型は A->B にします。

ラムダ式と型宣言を一緒にしてパッケージしたものが大きなラムダ式*2です。ただし、ラムダ束縛変数の型宣言は'λ'の直後に埋め込んでいます(それが普通の書き方)。次は大きなラムダ式の例です。

  • 〈f:A->B, g:B->C| λx:A.(g・(f・x))〉

大きなラムダ式との対比のために、内側に置かれたラムダ式を小さなラムダ式とも呼びます。大きなラムダ式の基本的な形は次のようです。

  • 〈型宣言| 小さなラムダ式〉

小さなラムダ式(裸のラムダ式)ではなくて、常に大きなラムダ式を使って進めていくのが大きなラムダ計算です。基本はそれだけのことです。

この記事(+次回)で大きなラムダ計算について最初から説明するので過去記事を参照する必要はありませんが、歴史的経緯を言えば、2008年/2009年あたりのセミナーでは、大きなラムダ計算をインフォーマルに導入しています。

大きなラムダ計算の短い説明ならば次の記事にあります。

概要と目標

前節で説明したような大きなラムダ式(後で少し定義を拡張します)の全体を考えます。すべての大きなラムダ式からなる集合をLLE(large lambda expressionから)とします。LLEに、圏の構造を与えることができます。正確な言い方をすると、集合LLEをベースに圏を作れる、となります。集合LLEをベースに作った圏のほうは太字でLLEと書くことにしましょう。

集合LLEと圏LLEとの関係は、

  • Mor(LLE) = LLE

です。つまり、大きなラムダ式は圏LLEの射(morphism)となります。

では、圏LLEの対象は何でしょうか? それは、大きなラムダ計算で使う型の集合です。当該ラムダ計算で使用できるすべての型の集合をTypeとすると、

  • Obj(LLE) = |LLE| = Type*

です。Type*はTypeの要素を並べたリストの集合、つまり“単一の型を並べたリスト”の集合です。

この記事(+次回)の目標は、圏LLEを構成することです。

注意すべきは、圏LLE完全に構文的に作られているということです。(型付き)ラムダ計算に意味を与えることは、構文領域である圏LLEから意味領域となる圏Cへの関手を作ることです。(意味関手は、単なる関手以上にモノイド構造や閉構造などを保つことも要請します。)例えば、C = Set として、意味関手 SetSem:LLESet を作れば、ラムダ計算を集合と写像の計算として解釈することになります。

意味関手が値を取る圏Cを変えればまったく別な意味論ができます。例えば、順序代数構造(Heyting algebraなど)から作られたやせた圏Cとすることもできます。Cを固定しても意味関手は色々作れます*3

今回(+次回)は圏LLEを作るまでで、その上に意味関手を定義はしませんが、意味論を展開する構文的基盤を準備するのだと思うとよいでしょう。

集合と写像に関する基礎的事項

この節は、インフォーマルな意味論の説明に必要となる用語のまとめです。ザッと眺めるだけ、あるいは飛ばしてしまってもけっこうです。

A, B, Cなどは集合を表すとします。fがAからBへの写像であることを f:A→B と書きます。x∈A ならば、f(x)∈B です。A×Bは集合の直積で、g:A×B→C とは、「gが、AとBのペアを入力としてCの要素を返す写像である」ことです。x∈A, y∈B ならば、g(x, y)∈C です。なお、写像と関数は同義語として扱い、特に区別しません。

関数集合

AからBへの写像の全体を集合と考えたものをBAと書きます。この指数記法は入れ子にするのが辛いので、BAを A->B とも書きます。矢印風記法なら、入れ子も問題ありません; 例えば、A->(B->C) 。A->B を指数集合(exponential set; もともと指数記法で書いたので)とか関数集合(function set)と呼びます。

関数オブジェクト

f:A→B と f∈(A->B) は同じ意味ですが、「AからBへの写像」と「A->B の要素」を区別しないと混乱してしまうことが多いので、関数集合 A->B の要素を関数オブジェクト(function object)と呼ぶことにして、写像fに対応する関数オブジェクトを^fと書きます。(f^とも書きますが、今回は左肩にハットを付けます。)

  • f:A→B ⇔ ^f∈(A->B)

関数オブジェクト^fは、働きとしてのfをコンパイルした結果であるバイナリコードだと思うといいでしょう。^fはバイナリコード=実行可能データです。

適用

入力データxと実行可能データ^fを渡して実行する仮想マシン(の概念的モデル)をappとすると、appは次のような写像です。

  • app:A×(A->B)→B

実行結果は、もとの写像fの値となるので、次の等式が成立します。

  • app(x, ^f) = f(x)

appと入力の順序が逆である写像をapp'とします。

  • app':(A->B)×A→B
  • app'(^f, x) = f(x)

appやapp'を適用写像(application)とか評価写像(evaluation)と呼びます。

写像の直積

集合だけでなくて、写像にも直積を定義しましょう。f:A→X, g:B→Y のとき、f×g:A×B→X×Y は次のように定義します。

  • (f×g)(x, y) := (f(x), g(y))
デカルトペア

<f, g>(x) = (f(x), g(x)) と定義される写像を、fとgのデカルト・ペア(Cartesian pair)と呼びます。写像の直積とデカルトペアは、対角写像Δ(定義: Δ(x) = (x, x))により次のように関係付けられます。

  • <f, g> = Δ;(f×g)
射影と成分

A×B→A という射影をπ1、A×B→B という射影をπ2と書きます。f:C→A×B のとき、f1 = f;π1、f2 = f;π2 と書きます。f1をfの第一成分(first component)、f2をfの第ニ成分(second component)と呼びます。具体的に書くと:

  • f(z) = (x, y) のとき、f1(z) = x、f2(z) = y
単元集合と廃棄写像

1 = {0} として単元集合(シングルトン集合; singleton set)と呼びます。単元集合の唯一の要素は何でもいいです。単元集合を型とみなすときはユニット(unit)型とかヴォイド(void)型とか呼びます。

任意の集合Aから1への写像がただひとつだけあるので、それを!Aと書きます; !A:A→1。!Aには様々な呼び名があります: terminal morphism, final morphism, discarder, discharger など。ここでは、入力を捨ててしまうので廃棄写像(discarding map)と呼びましょう。

型システム

これから先「型」という言葉を頻繁に使います。「型」という言葉の解釈は、めちゃくちゃイッパイあります。ここでは、次の2つの立場を適宜使い分けます。

  1. 型とは集合である。
  2. 型とは単なる記号である。

インフォーマルな意味論としては、「型」は集合を表すと考えます。しかし今回は、オフィシャルな意味論の話はなくて、構文論だけです。実際のところは“ある種の記号”を「型」と呼ぶことになります。

インフォーマルな意味論も含めて、型を構成する手順を説明しましょう。まず、有限個の集合を選びます。例えば、自然数の集合 N = {0, 1, 2, ...} ひとつだだけを選びます。選んだ集合に名前(の記号)を割り当てます。例えば、自然数の集合に英字大文字'N'を割り当てます。他に、英字大文字'I'を単元集合1を表す記号として予約します。これで基本型記号(basic type symbol/name)が決まります。

何でもいいので2種類の結合子記号(connective symbol)を決めます。例えば'△'と'♂'にします。一般的な型記号(type symbol)、あるいは型項(type term)を帰納的に定義します。

  1. 基本型記号は型記号である。
  2. AとBが型記号ならば、(A△B) は型記号である。
  3. AとBが型記号ならば、(A♂B) は型記号である。
  4. 以上により定義されたものだけが型記号である。

心づもりとしては、型記号は集合を表すものです。基本型記号がNとIの場合、型記号Aが表す集合を〚A〛とすれば:

  1. 〚N〛 = N, 〚I〛 = 1
  2. 〚A△B〛 = 〚A〛×〚B〛
  3. 〚A♂B〛 = 〚A〛->〚B〛

例えば ((N△I)♂(N♂N)) の意味は 〚((N△I)♂(N♂N))〛 = (N×1)->(N->N) と計算できます。

以上の“記号の意味”はあくまで心づもり、想定であって、実際には意味論なしの構文論を考えます。したがって、オフィシャルには型とは型記号(型項)のことです。

型が等しいとは、集合の同一性や同型性ではなくて、記号として(図形として)の等しさです。(I△N) と N は違う記号なので違う型です。((N△N)△I) と (N△(N△I)) も違う記号なので違う型です。型Aと型Bがイコールだとは、AとBがまったく同じ記号のことです。

いま、結合子記号に'△'と'♂'を選びましたが、'×'と'->'にします。そうすると、集合のホントの直積/指数と区別が付かない問題が起きますが、文脈により、単なる結合子記号か集合の演算子記号かは区別できるでしょう。

また、(I×N) とか ((N×N)×I) のように律儀に括弧は付けず、I×N、N×N×I のように書きます。要するに、混乱がない限り普通の書き方をする、ということです。普通に書くと、人間の心理として集合を想定してしまいがちですが、オフィシャルには単なる記号だと肝に銘じてください。

続く

次回に続きます。次回で大きなラムダ式の構文を定義して、型付け(typing)を行うための形式的証明系を導入します。そして、構文論だけから得られる圏LLEを定義します。次回内容は:

  1. 疑似ラムダ項の構文
  2. ラムダ項の構成と型付け
  3. 大きなラムダ式のアルファ変換
  4. 大きなラムダ式の構造規則
  5. マルチ代入
  6. 型証明系TPS1
  7. TPS1における代入消去と型付けの一意性
  8. ラムダ計算のポリ化: 型証明系TPS2
  9. もうひとつの型証明系TPS3
  10. LLEの定義
  11. LLEのモノイド構造
  12. ラムダ式の変換と同値に関する注意
  13. おわりに

*1:変数に型情報をくっ付けるとか、型ごとに別な変数集合を準備するとかの方法もあります。ですが、型宣言が一番実用的だと思います。

*2:大きなラムダ式は、実質的には型付きラムダ項(typed lambda term)と変わりません。型宣言とのパッケージを徹底することが意図されています。

*3[追記]構文的な体系をひとつに固定したとして、圏Cに値を取る意味関手がたくさん定義できるのは事実です。しかし、これは鬱陶しくてイヤな状況です。できるなら、Cを決めれば一意的に意味関手が定まって欲しい -- この希望をかなえるように意味論を構成することは可能です。僕が「セマンティック駆動」と言ってきた方法は、Cを先に与えて、それから一意に意味関手を作る方法です。[/追記]

2017-05-18 (木)

よくあるタイポ

| 14:42 | よくあるタイポを含むブックマーク

キーボードで文字を書くと、余分な打鍵が発生して重複した2文字になることがあります。日本語だと、1文字2打鍵なので、それほど起こらないように思えますが、そうでもない。

僕のダイアリー内で「をを」「とと」「のの」を探したらけっこうありました。「とと」「のの」は正しい場合がありますが、「をを」はすべて誤入力です。修正した。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170518

2017-05-10 (水)

ヤコビ微分圏: はじまり

| 17:00 | ヤコビ微分圏: はじまりを含むブックマーク

CADG(Categorical Abstract Differential Geometry)の練習問題として、ヤコビ微分圏というモノを考えてます。ヤコビ微分圏は、通常の多変数微分計算のエッセンスを圏論的に取り出したものです。ヤコビ微分圏を考えるに至った動機やご利益について語ります。

内容:

  1. CADGとデカルト微分
  2. ヤコビ微分圏の動機
  3. 準半加法圏など
  4. ヤコビ微分圏の抽象的構成・具体的構成

CADGとデカルト微分

CADG(Categorical Abstract Differential Geometry)は、微分や“なめらかさ”の概念を圏論的に定式化して、微分幾何を抽象的に展開する試みです。90年代のリソース・ラムダ計算(resource lambda-calculus, 1993)や80年代のロシツキーの先駆的仕事(Jiri Rosicky, 1984)があったものの、“微分幾何”としての形が整ってきたのは2010年前後でまだ新しい分野です。その有効性と射程はいまだ明らかとは言えません*1

微分を持つ圏/なめらかな対象からなる圏”の定義には幾つもの案があります。そのなかでも基本的で重要なものはデカルト微分(Cartesian differential category)と接圏(tangent category)です。それぞれの圏(の種別)を最初に提案した論文(基本文献)は以下のものです。

デカルト微分圏に関しては、オリジナルから少し変更した一般化デカルト微分(generalized Cartesian differential category)をクラットウェルが定義しています。次の論文に記述があります。

上記の2つの論文のあいだで、一般化デカルト微分圏の定義が少し違っていますが、気にする程の違いではありません。それより、オリジナルのデカルト微分圏(ブルート/コケット/シーリー 2009)と一般化デカルト微分圏(クラットウェル 2013)の関係がハッキリしないほうが問題です。

どうも、一般化デカルト微分圏がオリジナルのデカルト微分圏を完全には包含してないように思えます(下図)。

一般化デカルト微分圏のなかで「すべての対象が(クラットウェルの意味で)“線形”である圏」は間違いなく(ブルート/コケット/シーリーの)デカルト微分圏になります。しかし、デカルト微分圏が必ず一般化デカルト微分圏になる保証はなく、「デカルト微分圏だが一般化デカルト微分圏にならない圏」が存在する可能性があります。とはいいながら、僕はその実例を知らないのですが。

仮に「デカルト微分圏だが一般化デカルト微分圏にならない圏」が在ったにしても、一般化デカルト微分圏のほうが使い勝手がいい定義なので、僕は一般化デカルト微分圏を採用します*2。と、そんな事情で、以降、単にデカルト微分圏と言ってもそれはクラットウェルの一般化デカルト微分圏のことです。

デカルト微分圏は、ユークリッド空間における微分計算の抽象的な定式化です。一方、接圏は、なめらかな多様体の圏から抽象した構造です。デカルト微分圏には必ず接圏の構造を入れられます。さらに、デカルト微分圏に制限構造(restriction structure)を載せて、グロンディ(Marco Grandis)の多様体完備化(manifold completion)すると接圏が出来ることもわかっています。また、適当な仮定のもとで接圏は局所的なデカルト微分圏構造を持ちます*3

以上のことから、「デカルト微分圏 : 接圏」の関係は、「多変数の微分計算 : 多様体微分幾何」の関係と同様だと言えます。CADGの主要な対象物は接圏ですが、その初等理論、局所理論としてデカルト微分圏の理論がある、という状況ですね。

ヤコビ微分圏の動機

f:RnRm をなめらかな写像だとして、一点でのfの微分係数はm行n列のヤコビ行列(Jacobian matrix)で与えられます。CADGでもヤコビ行列の対応物はあるのでしょうか。…… それがないのです。ヤコビ行列の対応物を作るのは可能なのですが、実際には、ヤコビ行列による定式化は採用されていません。その理由は(おそらく)、行列の対応物を作るのが面倒だからでしょう。行列概念なしでも微分計算は可能だし、そのほうが話が単純になります。

「ヤコビ行列を作るのは七面倒くさいだけでいいことないのか?」と疑問に思い、ちょっと試してみました。確かに面倒くさいです。が、いいこと(メリット、見返り)もあります。ヤコビ行列を使った定式化のいいところを挙げてみます。

  1. 通常の多変数微分計算の直接的な定式化である。
  2. 教育的な意義がある。
  3. 論理との関係が見える。
  4. 下部構造が面白い。
  5. 非関手的・非自然な手法が活躍する。

これらのいいことを順に説明していきます。以下では、ヤコビ行列を使った微分ヤコビ微分(Jacobian differential)、ヤコビ微分を備えた圏をヤコビ微分(Jacobian differential category)と呼ぶことにします。

通常の多変数微分計算の直接的な定式化である。

ほとんどの多変数微積分の教科書では、多変数の微分係数・導関数をヤコビ行列により定義していると思います。ですから、ヤコビ行列ベースの定式化は我々が慣れ親しんだシナリオをたどることになり、分かりやすいと思います。ヤコビ微分圏は、通常の微分計算をそのまま圏論フレームワーク内に移します

教育的な意義がある。

CADGでは、位相や極限に関する事は扱いません。これにより、微積分や微分幾何のなかで、何が位相・極限に依存して、何が代数計算だけで出来るのかが明確に切り分けられます。これは教育的に意義がありますが、通常の微分計算/微分幾何と異なったシナリオではピンと来ないでしょう。一番目のメリットである「普通さ」があるヤコビ微分圏なら、「切り分け」も意識しやすくなります。

論理との関係が見える。

僕が「おやっ」と思ったのは、ヤコビ微分圏内の微分計算の公式が命題論理の演繹(公理や推論規則)に対応していることです。含意記号を'⊃'として、微分公式に対応するめぼしい演繹を書くと:

  *(前提なし)
 -----[同一律]
 A⊃A

 A  A⊃B
 --------[モダス・ポネンス]
    B

 A⊃B  B⊃C
 -----------[カット]
   A⊃C

  A⊃(B⊃C)
 ------------
  B⊃(A⊃C)

  A⊃B   C⊃D
 --------------
 (A∧C)⊃(B∧D)

   A
 ----------
 (A⊃B)⊃B

これらの演繹が微分公式に対応していることは、行列概念(の圏論的対応物)とヤコビ微分を導入しないと見えてこないと思います。

下部構造が面白い。

ヤコビ微分を導入する前に、土台になる圏を整備しなくてはなりません。その圏は、デカルト圏にさらに構造が載ったものです。圏全体はデカルト圏で、特定された部分圏には余デカルト構造が入り半加法圏となっています(次節で記述)。このような構造には(僕は)初めて出会いました。それ自身、なかなか興味深いです。

非関手的・非自然な手法が活躍する。

以下に挙げる過去記事(割と最近)で、非関手的・非自然な手法を説明しました。それらの手法の構成素には、圏論的モダリティ、圏論的コンストラクタ、圏論的オペレータなどがあります*4

前段落で述べた「外側のデカルト圏と半加法的な部分圏」という構造を定義するには、圏論的モダリティが便利です。また、圏の対象Xにその線形化(linearization; または線形台 linear carrier)という対象L(X)を対応させる操作は圏論的コンストラクタです。圏上のヤコビ微分圏論的オペレータになります。ヤコビ微分圏は、非関手的・非自然な手法が活躍する事例としての意味があります。

準半加法圏など

ヤコビ微分圏の定義・構成が面倒になる理由は、下部構造の圏が単なるデカルト圏では済まないからです。ヤコビ微分圏の土台になる圏を準半加法圏(qusi-semiadditive category)と呼ぶことにします。「準半」て何だよそれ? と言われそうですが、「準半」に前例がないわけでもありません。

なんでこんな変な名前を付けざるを得ないのか? 「「余」と「双」の使い方がバラバラ」で愚痴ったことがありますが、「双デカルト圏」、「加法圏」、「半加法圏」のあたりは、圏論定義と用語法が腐っているところで、混乱必至。ですが、致し方ないので慣用の用語法に従うとすると、双積(biproduct)を持つ圏が半加法圏(semiadditive category)となります -- これはろくでもないネーミングだと思うんだけど…

それで、ヤコビ微分圏のために必要な圏は、一部分だけが半加法圏となっているデカルト圏です。「一部分だけ」を表す言葉にpartialがあるので、"partially semiadditive category"とかでも良さそうですが、partial/partiallyは、「偏微分」の「偏」として「複数変数のなかの特定変数に関してだけ」の意味で使いたいので温存したい。で、「完全には半加法圏ではない」から"quasi"を前置して"qusi-semiadditive category"=「準半加法圏」になったわけ。トホホホ。

準半加法圏は部分圏(充満部分圏ではない)として半加法圏を持つので、この半加法的部分圏のなかで線形代数ができます。次のような言葉の置き換えをすればイメージが掴めるでしょう。

  • 半加法的部分圏の対象 → ベクトル空間
  • 半加法的部分圏の射 → 線形写像

実際クラットウェルは、現状の用語法は無視して、半加法的対象と射を「線形対象」「線形射」と呼んでいます -- それもアリかも知れません。(現状の用語法に拘らないなら、準半加法圏は準線形デカルト圏であり、線形部分圏を持つ、と言えます。)

まーともかく、準半加法圏は、線形代数ができる部分圏(半加法圏)を持つわけです。しかし、行列概念の定義にはデカルト閉構造(の変種)も必要です。閉構造は外側のデカルト圏全体に存在するわけではなくて、半加法的部分圏が閉構造を持つのです。うーん、「閉」をどこに付けたらいいのかな? 準閉半加法圏? 閉準半加法圏? 準半加法閉圏? ハァー(ため息)、現状の用語法に合わせるのも限界かも。

ヤコビ微分圏の抽象的構成・具体的構成

前節で述べたように、ヤコビ微分圏の面倒な部分は土台になる圏の構成です。逆に言うと、土台になる圏を構成してその性質を十分調べておけば、微分オペレータは割と簡単です。古典的微分計算と対応付けたり、絵による微分計算(微分絵算)も出来るでしょう。

絵図主義者(picturalist)には朗報なんですが、微分圏は絵算と意外に相性がいいです。絵算の創始者の一人であるペンローズは、テンソルの代数計算だけでなく、テンソル場の微分計算も(ペンローズ・ヒエログリフとも呼ばれる)彼の図式法で遂行していたので、微分も絵で描けることもむべなるかなです。

*5

ヤコビ微分圏の典型的な事例は、ユークリッド空間の開集合と、その上で定義された無限回微分可能写像の圏です。各点のヤコビ行列により導関数微分オペレータを定義します -- これがまさにヤコビ微分です。この事例をうまく説明し、今まで見えにくかった構造に光を当てることが出来れば、ヤコビ微分圏の最初の目標はクリアしたと言えるでしょう。

ここまで、ヤコビ微分圏のご利益や周辺事情やロードマップを述べましたが、実質的内容には踏み込んでいません。たぶん、引き続く記事で(いつか)実際のところを話すと思います。一番の難所は錯綜した用語法の整理と選択かも知れません。

*1:現状では、キラーアプリケーションが見当たりません。めざましい応用例がないと、「ちょっと面白かったけど、結局、役に立たなかったね」となる危惧もあります。

*2:僕の感覚では -- つまり、合理的な説明がうまく出来ないのですが -- オリジナルのデカルト微分圏の定義は良くない、と思えます。使い勝手が悪いだけでなく、なにか外している感覚があります。

*3:これらのことを手っ取り早く知りたいなら、次のスライドがあります。Differential Join Restriction Categories, Differential Categories to Tangential Structure, Tangent categories are locally Cartesian differential categories

*4:他に関連記事として、「余可換コモノイド・モダリティ事件の解説」、「天空の支配者」。

*5:画像は、Wikipedia項目"Penrose_graphical_notation"より

トラックバック - http://d.hatena.ne.jp/m-hiyama/20170510

2017-05-08 (月)

圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却

| 12:24 | 圏論的コンストラクタと圏論的オペレータ: 関手性・自然性の呪縛からの脱却を含むブックマーク

圏論で関手と自然変換が重要なのは言うまでもありません。しかし、これらに拘り過ぎるのもマズイのではないか、と思います。プログラミングにおける型構成子や総称関数は、関手・自然変換に対応しないことがままあります。トレースや不動点オペレータは、関手・自然変換ではないけど重要な圏論的構成素です。非関手的対応、非自然な変換も積極的に使いましょう。

内容:

  1. 圏論的コンストラクタと圏論的オペレータとは何か
  2. 関手・自然変換の一部を見ているとき
  3. トレース、不動点微分
  4. モナドデカルト圏、コンパクト閉圏
  5. おわりに

圏論的コンストラクタと圏論的オペレータとは何か

最近、CADG(Categorical Abstract Differential Geometry)をまた調べています。CADGは十分な一般性を持つアブストラクト・ナンセンス(いい意味で)であり、複雑で多様な構成を必要とします。こういう状況では、関手でも自然変換でもないようなシロモノが色々と登場します。

先月、関手でも自然変換でもないようなモノを使う枠組みとして圏論的モダリティを紹介しました。モダリティを構成する素材として、非全域関手と非自然変換を説明しましたが、少し別な観点から、またこの記事で非全域・非自然なモノを解説します。

CDが圏のとき、|C|→|D|、または |C|→Mor(D) の形の写像圏論的コンストラクタ(categorical constructor)と呼びましょう。典型的な例は、プログラミングにおける型構成子(type constructor)です。例えばリスト型構成子は、型Xに対して、Xのリスト型List(X)(プログラミングではList<X>と書くことが多い)を対応させます。型引数を持つ総称関数は、|C|→Mor(D) のタイプの圏論的コンストラクタになります。例えば、id<X> は、型(圏の対象)Xに“Xの恒等関数”を対応させる圏論的コンストラクタとみなせます。

Cが幾つかの圏の直積圏のときを考えましょう。C = C1×...×Cn とします。このとき、C上で定義されたコンストラクタは、|C1|×...×|Cn|→D または |C1|×...×|Cn|→Mor(D) の形です。プログラミングでは、幾つかの型引数を持つ型構成子/総称関数が、直積圏上の(圏論的)コンストラクタに対応します。例えば、2つのベクトル空間V, Wに対して、VからWへのゼロ線形写像をOV,Wとすると、V, W|→OV,Wは2つの対象にひとつの射を対応させるコンストラクタです。

圏論的コンストラクタは対象全域で定義される必要はありません。例えば、順序集合の圏Ordで、「対象Xの最小元を指定する」という操作を考えてみます。これは付点モダリティの例になります。Xに最小元があれば、⊥X:1→X が決まります。しかし、最小元がない順序集合はいくらでもあるので、X|→⊥X : |Ord|→Mor(Ord) は部分的にしか定義されません。

圏の射に射を対応させる写像圏論的オペレータ(categorical operator)と呼びましょう。圏論的オペレータは、圏論コンビネータ(categorical combinator)とも呼びます。この文脈での「オペレータ」と「コンビネータ」は同義語です。ただし、「圏論コンビネータ」というと、S, K, Iなどを圏論的にゴニョゴニョすることだと思う人が多いので、主に「オペレータ」を使うことにします。「オペレータ」という言葉も多義的で曖昧なのですが、まーしょうがない。

例えば、A, B, Cを集合として、集合圏Setにおけるカリー化 (f:A×B→C)|→(Λ(f):A→CB) を考えてみましょう。これは、ΛA,B,C:Set(A×B, C)→Set(A, CB) という集合(Setの対象)3つで添字付けられた写像の族です。このように、圏論的オペレータの実体は、ホムセットのあいだの写像として与えられます。圏Cの構造を与える結合(composition)も、γA,B,C:C(A, B)×C(B, C)→C(A, C) という形の圏論的オペレータです。

圏論的オペレータは、シーケント計算の推論規則の形に書けます(「圏論の筆算としてのシーケント計算」参照)。直積をカンマ、指数(関数空間)を含意記号'⊃'で書くとして、カリー化は:

  A, B ⇒ C
 -----------[Curry = 左含意導入]
  A ⇒ B⊃C

圏の結合なら:

 A ⇒ B    B ⇒ C
 -----------------[Comp = カット]
     A ⇒ C

コンストラクタのなかには、シーケント計算の公理の形に書けるものもあります。A|→idA はそのようなコンストラクタです。

     *(前提なし)
 ---------------[Id = 同一律]
    A ⇒ A

圏論的コンストラクタと圏論的オペレータの区別は必ずしも明確ではありませんし、明確にする必要もないでしょう。関手の射部分(morphism part)をホムセットごとの関数で表した FX,Y:C(X, Y)→D(F(X), F(Y)) は、射から射を作り出しているので圏論的オペレータですが、|C|×|C|→Mor(Set) の形のコンストラクタだとも言えます。おおよその分類基準を書いておくと:

  • 対象のコンストラクタ: いくつか(0個, 1個, 2個, ...)の対象に対して対象を対応させる。
  • 射のコンストラクタ: いくつか(0個, 1個, 2個, ...)の対象に対してを対応させる。
  • オペレータ: いくつか(0個, 1個, 2個, ...)のに対してを対応させる。

関手・自然変換の一部を見ているとき

圏論的コンストラクタ、圏論的オペレータが関手・自然変換を定義しても、もちろんかまいません。実際には関手・自然変換なのだが、関手性・自然性に気付かないでいることもあります。

デカルト閉圏Cにおけるカリー化オペレータ ΛA,B,C:C(A×B, C)→C(A, CB) は、Bを固定してA, Cを動かせば、関手 (-)×B と (-)B のあいだの随伴性を主張しているので、自然同型(成分が同型である自然変換)です。しかし、カリー化が自然変換だと知らないで使っている場合もあるだろうし、自然性なしでも役に立ちます。

カリー化と一緒に使う評価射 evA,B:A×BA→B も、随伴性を構成する余単位自然変換ですが、カリー化との関係を理解していれば、2つの添字A, Bを持つ射の族としての扱いでも十分なことも多いです。

リスト型構成子 X|→List(X) や直積型構成子 X, Y|→X×Y も関手・二項関手に拡張できます。リスト型構構成子はリスト・モナドの一部となり、直積型構成子はデカルト・モノイド積関手の一部になります。モナドデカルト構造は関手概念を使わない定式化もあります(後述)。具体的な計算の場面では、コンストラクタ/オペレータの形のほうが使いやすかったりします。

関手性・自然性を見つけることは非常に重要ですが、関手性・自然性が明らかでないときは、とりあえずはコンストラクタ/オペレータ(コンビネータ)/モダリティとして定式化して調べるのが得策だと思います。どうやっても関手・自然変換にならなくても、役に立ってくれることもあります。

トレース、不動点微分

よく知られた圏論的オペレータにトレース・オペレータと不動点オペレータがあります。これらのオペレータの下部構造として対称モノイド圏が要求されます。トレース・オペレータTrと不動点オペレータFixは次の形をしています。

   f : A¥otimesX → B¥otimesX
 --------------------
  TrA,BX(f) : A → B

   f : A¥otimesX → X
 --------------------
  FixAX(f) : A → X

CADG(圏論的抽象微分幾何)に登場する微分オペレータを、一般化デカルト微分圏(generalized Cartesian differential category)で定式化した場合は次のようになります。Lは圏論的コンストラクタで、対象Xの線形化と呼ばれるモノがL(X)です。

   f : X → Y
 --------------------------
  DX,Y(f) : L(X)×X → L(Y)

トレース/不動点オペレータについては、過去に説明したことがあるので、それらの記事を参照してください(下のリスト)。トレース/不動点オペレータは、部分的な自然性や変形された自然性(対角自然性)を持ちますが、単なる自然変換として説明することはできません。

CADGの微分オペレータ(微分コンビネータ)については、いずれまた述べる機会があるでしょう。

モナドデカルト圏、コンパクト閉圏

モナド

モナドの定義には、クライスリ拡張(Kleisli extension)を使うスタイルがあります。このスタイルを使う場合のモナドの構成素は:

  1. 型構成子 X|→T(X)
  2. 総称関数 ηX:X→T(X)
  3. f:X→T(Y) の形の関数に働く高階総称関数(これがクライスリ拡張) (-)# 、f#:T(X)→T(Y)

Tは“値が対象であるコンストラクタ”、ηは“値が射であるコンストラクタ”、(-)#は“オペレータ”です。拡張オペレータはほんとは添字付きで (-)#X,Y:C(X, T(Y))→C(T(X), T(Y)) です。これらのコンストラクタ/オペレータのあいだの条件(公理)によりモナドが定義されます。

デカルト

デカルト圏を定義するには幾つものやり方がありますが、そのなかのひとつでは次の構成素を使います。

  1. 対象に対してだけ定義された直積 X, Y|→X×Y
  2. 対象X, Yに対して一意に定義された射 π1X,Y:X×Y→X と π2X,Y:X×Y→Y
  3. 特定された対象1
  4. 対象Xに対して一意に定義された射 !X:X→1
  5. f:X→Y, g:X→Z という形の射に対して定義されたデカルト・ペアリング <-, -> 、<f, g>X,Y,Z:X→Y×Z

直積×は“ニ変項のコンストラクタ”、π1, π1は“添字を2つを持つ射のコンストラクタ”、!は“添字を1つ持つ射のコンストラクタ”、<-, ->は“ニ変項(入力の射が2つ)のオペレータ”です。デカルト・ペアリング・オペレータを添字付きで書けば、<-, ->X,Y,Z:C(X, Y)×C(X, Z)→C(X, Y×Z) 。これらのコンストラクタ/オペレータのあいだの条件(公理)によりデカルト圏が定義されます。

コンパクト閉圏

C = (C, ¥otimes, I) は対称モノイド圏であるとして、Cにコンパクト閉構造を載せることを考えましょう。そのとき、次の構成素を追加します。

  1. 対象Xに対して一意に定義された対象X*、Xの双対対象
  2. 対象Xに対して一意に定義された射 ηX:I→X*¥otimesX 、双対の単位
  3. 対象Xに対して一意に定義された射 εX:X¥otimesX*→I 、双対の余単位

(-)*は“コンストラクタ”、ηとεは“射を値とするコンストラクタ”です。これらのコンストラクタ/オペレータのあいだに条件を課します。その条件から、結果的に(-)*は反変関手に拡張できて、η, εも自然変換だとみなせますが、最初から関手性・自然性を仮定する必要はありません。

おわりに

ここで僕が言いたいことは、我々に必要な操作・構成がすべて関手・自然変換であるとは限らないことです。また、最終的には関手・自然変換だと判明するにしても、最初からその姿で現れないかも知れません。そのような操作・構成の定式化に圏論的コンストラクタ/圏論的オペレータが有効です。

コンストラクタ/オペレータは、プログラミングの型構成子/総称関数/高階総称関数などに対応するので、プログラミング的(運算的; calculational)な概念になります。このため、計算には有利となることもあります。

圏論的コンストラクタ/圏論的オペレータは、非全域関手/非自然変換の利用形態のなかで頻出するパターンを取り出して名付けたものです。非全域関手/非自然変換は組織化されて圏論的モダリティとなります。モダリティは、必ずしも関手・自然変換とは限らないメカニズムを使って、圏上の構造を定義する手法です。圏論的モダリティは、圏論の枠内で複雑さ/多様さ(あるいは“汚さ”)をうまく処理してくれます。

2017-05-01 (月)

天空の支配者

| 15:48 | 天空の支配者を含むブックマーク

上空にいる足し算の親玉を捕まえる」で次のように書きました。

雰囲気的に言うと、地上の圏Cの足し算構造を、上空にあるメタ圏内のただひとつの代数系が支配していることになります。

この「上空にいる親玉」を、もっと小洒落た呼び方をしたい、と。で、「天空の支配者」はどうかな、と。天空を支配する者ではなくて、天空にいて地上を支配している者を指します。「天空の城」(ラピュタ)の英訳が"Castle in the Sky"らしいから、"Ruler in the Sky"かな。

支配者、あるいは統御構造の実体は何かというと、最近言い出した圏論的モダリティというヤツです。

モダリティは、関手と自然変換の制約をゆるくしたもので非全域性と非自然性を許します。特に全域かつ自然であるモダリティは従来の関手と自然変換による構造になります。

連休の期間、CADG (Categorical Abstract Differential Geometry)に対する天空の支配者を探そう、と思っています。モダリティによる定式化は、複雑で錯綜した状況を整理するのに役立つので、圏上の微分構造(differential structure)/接構造(tangent structure)にも有効そうです。

“圏上の微分構造/接構造=CADG”は、去年(2016年)の夏に調べたことがありますが、なめらかな多様体の圏やベクトルバンドルの圏の上空に幾つものモナドやコモナドが居るような構造だと思われます。さらに、モナド/コモナドを構成するもっと細かい構成素があり、それらが天空の支配者として君臨している気がしています。今は「思われる/気がしている」状況なので、天空を眺めて支配者を捕捉したいな、というわけ。

2017-04-26 (水)

余可換コモノイド・モダリティ事件の解説

| 12:35 | 余可換コモノイド・モダリティ事件の解説を含むブックマーク

一昨日の記事「圏論的モダリティ:圏上の非自然な構造達」の「僕のモダリティ経験」の節で:

試しに、非負実数係数のテンソルの圏に余可換コモノイド・モダリティを入れてみると、そのモダリティと整合する部分圏として部分性と確率的非決定性の両方がうまく定義できるようです。これが分かったとき、僕にとってはA-ha momentでした。

非全域関手と非自然変換」にて:

特に役に立つのは、2つの非自然変換から構成される余可換コモノイド・モダリティです。余可換コモノイド・モダリティの事例はそのうち述べるつもりです。

予告に従い、余可換コモノイド・モダリティの事例について述べます。タイトルに「事例」でなく「事件」と付けているのは、これから述べることが僕には思いがけないことだったからです。

内容:

  1. 余可換コモノイド・モダリティが定義する部分圏、不思議だ
  2. 余可換コモノイド・モダリティ
  3. 集合圏の余可換コモノイド・モダリティ
  4. 関係圏の余可換コモノイド・モダリティ
  5. モダリティと単葉関係/全域関係
  6. 非負実数係数テンソルとその圏
  7. 非負実数テンソルの圏の余可換コモノイド・モダリティ
  8. モダリティと非分散テンソル/マルコフ・テンソル
  9. 参考文献

余可換コモノイド・モダリティが定義する部分圏、不思議だ

池尻大橋駅から10秒くらいの近さのカフェ・ベローチェで、割と何となくナプキンペーパーで計算していたのですが、計算結果を見て「エッ?!」と驚きました。事前に予想も期待もしてなかった結果だったからです。これが、僕が余可換コモノイド・モダリティに興味を持つキッカケとなった「事件」(大げさだけど)です。詳しい説明は後の節でしますが、概要だけこの節で言っておきます。

係数(成分)が非負実数であるテンソル(幾つかの数を適当な次元の矩形状に並べたモノ)を考えます。非負実数係数のテンソルに関して次の言葉を使いますが、これらは後で定義します。

すべての非負実数(係数の)テンソルから構成される圏NNTens(non-negative (coefficient) tensors)に、自明と思える簡単なモダリティΔ(余乗法)とε(余単位)を入れると:

  1. Δと整合する射の全体は、非分散ブール・テンソルの全体と一致する。Δと整合する射が作るNNTensの部分圏は、有限集合を対象とする部分写像の圏FinPartialと同型である。
  2. εと整合する射の全体は、マルコフ・テンソルの全体と一致する。εと整合する射が作るNNTensの部分圏は、有限離散測度空間を対象とするマルコフ核(別名 stochastic map/kernel/relation)の圏FinStockと同型である。
  3. Δとεの両方と整合する射の全体は、非分散ブールかつマルコフなテンソルの全体と一致する。Δ, εと整合する射が作るNNTensの部分圏は、有限集合と写像の圏FinSetと同型である。

これと似た結果は関係圏Relでも成立します。関係に関する次の言葉も後で定義します。

  • 単葉(一価)関係(univalent relation)
  • 全域関係(total relation)

Relにおける余乗法と余単位も同じ記号Δ, εで表すとして:

  1. Δと整合する射の全体は、単葉な関係の全体と一致する。Δと整合する射が作るRelの部分圏は、部分写像(partial map)の圏Partialと同型である。
  2. εと整合する射の全体は、全域な関係の全体と一致する。
  3. Δとεの両方と整合する射の全体は、単葉かつ全域な関係の全体と一致する。Δ, εと整合する射が作るRelの部分圏は、集合と写像の圏Setと同型である。

うーん? なんでこんな現象が起きるのだろう? 内在的必然性とか背後のメカニズムとかはサッパリ分かりません。不思議だが本当だ。

Δとεの組み合わせは余可換コモノイド・モダリティとなります。経験則として、このモダリティ(Δ, ε)の一部または全部と整合する射を考えることは、面白い部分圏を抽出する手段として有効だ、とは言えそうです。理由は分からんけど。

余可換コモノイド・モダリティ

C = (C, ¥otimes, I, α, λ, ρ, σ) を対称モノイド圏とします。α, λ, ρはそれぞれ、結合律子(associator)、左単位律子(left unitor)、右単位律子(right unitor)、対称(symmetry)です(律子に関しては「律子からカタストロフへ」を参照)。

一般に、Cの対象Aに対して、自己関手 KA:CC はすべての対象をAに移し、すべての射をidAに移す“定数関手”とします。また Sq:CC は、対象も射もモノイド積の意味で平方(二乗)する関手です。

  • KA(X) = A, KA(f) = idA
  • Sq(X) = X¥otimesX, Sq(f) = f¥otimesf

モノイド単位対象Iに対する定数関手KIと平方関手Sqを考えます。この2つは、非全域関手ではなくて普通の(全域な)関手です。さらに非自然変換 Δ::Id ?⇒ Sq :CC と ε::Id ?⇒ KI :CC を考えます。ここで、IdはCの恒等関手です。特殊な矢印記号'?⇒'は、非自然(必ずしも自然ではない)ことを表します。このへんのところは「非全域関手と非自然変換」を参照。

非自然変換Δ, εの、対象Xにおける成分は次の形です。

  • ΔX:X→X¥otimesX in C
  • εX:X→I in C

2つの非自然変換Δとεの組み合わせ(Δ, ε)が余可換コモノイド・モダリティであるとは、任意の対象Xに対して、3つ組 (X, ΔX, εX) が余可換コモノイドになることです。他に、Δとεが圏のモノイド構造と調和するための一貫性条件も要求します。

余可換コモノイドの公理は昨日の記事の「対称モノイド圏の余可換コモノイド・モダリティ」に載せています。ここでは、図を描いておきましょう。余乗法Δは分岐の黒丸、余単位εはストッパーの横棒のアイコンで示すことにします。射の描画方向は ↓→ です。

余結合律、左余単位律、右余結合律、余可換律は次のとおりです。idXを単にXと書き、律子(構造同型射)α, λ, ρによる細かい調整は省略しています。

Δとεとモノイド積/モノイド単位との一貫性(調和性)は次の等式で表現できます。

  1. ΔX⊗Y = (ΔX¥otimesΔY);(X¥otimesσX,Y¥otimesY)
  2. εX⊗Y = εX¥otimesεY
  3. εI = idI

絵なら次のようです。点線は、モノイド単位対象を表す“空なワイヤー”です。

また、f:X→Y in C が“Δと整合すること”と“εと整合すること”は次の図で表せます。

集合圏の余可換コモノイド・モダリティ

集合圏Setに対して、余可換コモノイド・モダリティを定義します。集合圏のモノイド積は直積(記号'×')、モノイド単位対象は 1 = {0} とします。Δ, εを次のように定義します。

  • ΔX:X→X×X, ΔX(x) = (x, x)
  • εX:X→1, εX(x) = 0

集合Xごとの(X, ΔX, εX)が余可換コモノイドになること、そして一貫性条件を満たすことを確認してみてください。

集合圏Setの余可換コモノイド・モダリティでは、すべての射(集合のあいだの写像)がモダリティと整合します。つまり、f:X→Y in Set に対して:

  • f;ΔY = ΔX;(f×f) : X→Y×Y
  • f;εY = εX : X→1

これも簡単に確認できます。

結局、今定義した集合圏の余可換コモノイド・モダリティ(Δ, ε)では、Δもεも自然変換になります。自然変換は非自然変換の特別なものなので問題はありませんが、モダリティと整合する射として部分圏を抽出することは出来ません。部分圏を作る目的から言えば、自然な全域モダリティは役立たずなのです。

余可換コモノイド・モダリティが自然変換になっている状況は、実はモノイド積が直積(デカルト積)になっている場合に限られます。次の定理があります。

  • 対称モノイド圏Cに余可換コモノイド・モダリティ(Δ, ε)があり、Δとεが自然変換のとき、モノイド積は直積(デカルト積)である。

証明は割愛しますが、このことから、直積ではないモノイド積を持つ対称モノイド圏では、自然変換で与えられる余可換コモノイド・モダリティは存在しないことになります。モダリティが欲しかったら、非自然なものを許すしかないのです。これは、非自然性に関する重要な知見です。

関係圏の余可換コモノイド・モダリティ

次に、関係圏Relに余可換コモノイド・モダリティを入れましょう。関係圏のモノイド積も直積(記号'×')、モノイド単位対象は 1 = {0} です。Δとεも集合圏と同じですが、表現の仕方は少し違います。

  • ΔX:X→(X×X), ΔX = {(x, (x', x''))∈X×(X×X) | x = x' = x''} = {(x, (x, x))∈X×(X×X) | x∈X}
  • εX:X→1, εX = {(x, 0)∈X×1 | xは任意(無条件)} = X×1

集合Xごとの(X, ΔX, εX)が関係圏において余可換コモノイドになることも、そして一貫性も、集合圏のときと同様に確認できます。

集合圏とは違い、関係圏の射はΔ, εと整合するとは限りません。t:{1, 2}→{1, 2} in Rel を次のように定義します。

  • t = {(1, 1), (1, 2)}

このtでは、t;Δ{1, 2} = Δ{1, 2};(t×t) は成立しないし、t;ε{1, 2} = ε{1, 2} も成立しません。具体的に計算すれば分かります。

  • t;Δ{1, 2} = {(1, 1), (1, 2)};{(1, (1, 1)), (2, (2, 2))} = {(1, (1, 1)), (1, (2, 2))}
  • Δ{1, 2};(t×t) = {(1, (1, 1)), (2, (2, 2))};{((1, 1), (1, 1)), ((1, 1), (1, 2)), ((1, 2), (1, 1)), ((1, 2), (1, 2))} = {(1, (1, 1)), (1, (1, 2))}
  • t;ε{1, 2} = {(1, 1), (1, 2)};{(1, 0), (2, 0)} = {(1, 0)}
  • ε{1, 2} = {(1, 0), (2, 0)}

以上の計算から、

  • t;Δ{1, 2} ≠ Δ{1, 2};(t×t)
  • t;ε{1, 2} ≠ ε{1, 2}

t = {(1, 1), (1, 2)} は、Δともεとも整合しない射です。

モダリティと単葉関係/全域関係

関係圏Relにおいて、どのような射がΔ, εと整合するかを見ておきましょう。

r:X→Y in Rel がΔと整合するとします。このとき、r;ΔY = ΔX;(r×r) : X→Y×Y in Rel が成立します。等式の左辺/右辺を具体的に書き下してみます。

   r;ΔY
 = {(x, y)∈X×Y | (x, y)∈r};{(y, (y', y''))∈Y×(Y×Y) | y = y' = y''}
 = {(x, y)∈X×Y | (x, y)∈r};{(y, (y, y'))∈Y×(Y×Y) | y = y'}
 = {(x, (y, y'))∈X×(Y×Y) | (x, y)∈r かつ y = y'}

   ΔX;(r×r)
 = {(x, (x, x))∈X×(X×X) | x∈X};{((x, x'), (y, y'))∈(X×X)×(Y×Y) | (x, y)∈r かつ (x', y')∈r}
 = {(x, (y, y'))∈X×(Y×Y) | (x, y)∈r かつ (x, y')∈r}

r;ΔY = ΔX;(r×r) であるためには:

  • (x, y)∈r かつ y = y' ⇔ (x, y)∈r かつ (x, y')∈r

⇒方向は自明なので、実質的な条件は:

  • (x, y)∈r かつ (x, y')∈r ⇒ y = y'

この条件を満たす関係 r:X→Y in Rel単葉(univalent, 一価)な関係と呼びます。したがって、

  • 関係rがΔと整合する ⇔ rは単葉関係である

次に、r:X→Y in Rel がεと整合するとします。このとき、r;εY = εX : X→1 in Rel が成立します。等式の左辺/右辺を具体的に書き下してみます。

   r;εY
 = {(x, y)∈X×Y | (x, y)∈r};{(y, 0)∈Y×1 | yは任意}
 = {(x, 0)∈X×1 | xに対して、(x, y)∈r となる y∈Y が存在する}

   εX
 = {(x, 0)∈X×1 | xは任意}

r;εY = εX であるためには:

  • xに対して、(x, y)∈r となる y∈Y が存在する ⇔ xは任意

言い換えれば:

  • 任意のxに対して、(x, y)∈r となる y∈Y が存在する

この条件を満たす関係 r:X→Y in Rel全域(total)な関係と呼びます。したがって、

  • 関係rがεと整合する ⇔ rは全域関係である

Δとεの両方と整合する関係(Relの射)は、単葉かつ全域な関係となります。単葉かつ全域な関係は、写像だと思ってもかまいません。つまり、関係圏Relの部分圏として集合と写像の圏を再現しています。この部分圏に制限すれば、Δとεは自然変換になるので、部分圏上に自然な余可換コモノイド・モダリティが載ります。自然な余可換コモノイド・モダリティは直積(デカルト構造)を定義するので、この部分圏に制限したモノイド積が直積を与えることも分かります。

デカルト圏(直積/終対象を持つ圏)と、そのデカルト圏を拡張したモノイド圏の組としてはフレイド圏(Freyd category)があります。余可換コモノイド・モダリティを持った対称モノイド圏は、フレイド圏とかなり似ています。そういえば、フレイド圏に非自然な対角や余対角を載せることはやったことがありました。

プレモノイド圏やバイノイド圏は、関手性が破れた積を扱う仕組みでした。どうも、非関手的(no-fanctorial)/非自然(non-natural)な対応や族を扱う必然性はありそうです。モダリティは、非関手的/非自然な構造を扱う道具になる気がします。

非負実数係数テンソルとその圏

これから、係数(成分)が非負実数であるテンソルと、そのようなテンソルを射とする圏NNTens(category of non-negative tensors)に関して手早く(あるいは雑に)説明します。そして、次のような、特別な種類のテンソルを定義します。

R≧0を非負実数の全体とします。以下、X, Y, Zなどは有限集合を表すとします。写像 f:X×Y→R≧0非負実数(係数の)テンソル(non-negative (coefficient) tensor)と呼びます。fをテンソルとして扱うときは、f(x, y)をf[x→y]またはf[x←y]と書くことにします。また、f = (f[x→y] | x∈X, y∈Y) という書き方も用います。これは、行列の成分表示と同じだと思えばいいです。

f = (f[x→y] | x∈X, y∈Y) のテンソルとしてのプロファイルは、X→Y だとします。fは2つの見方ができます。2つの見方を適宜切り替えます。

f = (f[x→y] | x∈X, y∈Y), g = (g[y→z] | y∈Y, z∈Z) のテンソルとしての結合f;gは次のように定義します。

  • (f;g)[x→z] = Σ(y∈Y | f[x→y]g[y→z])

有限集合Xに対する恒等テンソルidXは:

  • idX[x→x'] = (if x = x' then 1 else 0)

idXの成分表示は、クロネッカーのデルタδ[x→x']を使うことも多いです。つまり、idX = (δ[x→x'] | x∈X, x'∈X) 。

ここまでの定義では、添字集合に任意の有限集合を許した行列とテンソルの差はありません。テンソルと呼ぶのは、X = X1×...×Xn, Y = Y1×...×Ym のようなときに、f = (f[x1, ..., xn→y1, ..., ym] | x1∈X1, ..., xn∈Xn, y1∈Y1, ..., ym∈Ym) という表現を使うからです。テンソルの具体的な計算例は、「確率的推論・判断の計算法:マルコフ・テンソル絵算」にあります。ブラケット内の x1, ..., xn→y1, ..., ym で、矢印よりカンマが優先される(結合度が強い)ので注意してください。

非分散テンソル

f:X→Y in NNTens のとき、a∈X に対して次の性質を定義します。

  • fがaで消失するとは、すべてのy∈Yに対して、f[a→y] = 0 のこと。
  • fがaで分散(または分岐)するとは、f[a→y'] ≠ 0 かつ f[a→y''] ≠ 0 かつ y' ≠ y'' であるy', y''が存在すること。

消失と分散を否定すると:

  • fがaで消失しないとは、f[a→y] ≠ 0 となるyが存在すること。
  • fがaで分散しない(または分岐しない)とは、任意のy', y''に対して、y' ≠ y'' であるならば、f[a→y'] = 0 または f[a→y''] = 0 となること。

任意のx∈Xに対してxで分散しないテンソル非分散テンソル(nondispersive tensor)と呼ぶことにします。非分散テンソルは消失を禁止してないので、Xの一部でfは消失しているかも知れません。

ブール・テンソル

テンソルの係数が0か1のどちらかの場合、0をfalse、1をtrueと思うとブール値なので、ブール・テンソル(boolean tensor, Boole tensor)と呼びましょう。ただし、計算はブール値ではなくて非負実数の計算を行うので、1 + 1 = 1 なんてことはありません。このため、ブール・テンソルの結合がブール・テンソルとは限りません。

マルコフ・テンソル(Markov tensor

テンソル f = (f[x→y] | x∈X, y∈Y) が、任意の x∈X に対して Σ(y∈Y | f[x→y]) = 1 のときマルコフ・テンソル(Markov tensor)と呼びます。「確率的推論・判断の計算法:マルコフ・テンソル絵算」の計算はすべてマルコフ・テンソルの計算です。

非負実数テンソルの圏の余可換コモノイド・モダリティ

非負実数テンソルの圏NNTensに余可換コモノイド・モダリティを入れます。NNTensのモノイド積は、対象に対しては直積(記号'×')、射に対してはテンソル積(記号'¥otimes')とします。f:X→Y, g:Z→W in NNTens のとき、f¥otimesg:X×Z→Y×W は次のように定義されます。

  • (f¥otimesg)[x, z → y, w] = f[x→y]g[z→w]

モノイド単位対象は I = {*} とします。唯一の要素を星印にしているのは、「確率的推論・判断の計算法:マルコフ・テンソル絵算」で使った u[x] = u[*→x] のような書き方に合わせるためです。

余乗法Δと余単位εは次のように定義します。

  • ΔX:X→(X×X), ΔX[x→x', x''] = (if x = x' = x'' then 1 else 0)
  • εX:X→I, εX[x→*] = 1

(Δ, ε)が余可換コモノイド・モダリティとなることを示すのは、テンソル計算のよい練習問題です。実際の計算は省略しますが、便利な略記法をここで述べておきます。

テンソルの計算では、しばしば添字を動かした総和をとります。例えば、f:X→Y×Z, g:Y→W, h:Z→W のときに k = f;(g¥otimesh) : Z→W×W を計算するとします。k[x→w, w']を求めるには総和と取ります。

  • k[x→w, w'] = Σ(y∈Y, z∈Z | f[x→y, z]g[y→w]h[z→w'])

このとき、総和を意味するΣを省略して、

  • k[x→w, w'] = (y, z | f[x→y, z]g[y→w]h[z→w'])

と書きます。これは「アインシュタインの総和規約」ですが、和を取る添字は残しています。和を取る添字を目視で判断するのがそれほど楽でではないからです。次の節の計算ではこの総和規約を使います。

モダリティと非分散テンソル/マルコフ・テンソル

非負実数テンソルの圏NNTensにおいて、どのような射がΔ, εと整合するかを調べます。僕が、池尻大橋カフェ・ベローチェのナプキンペーパーにした計算とは、これから述べる計算です。

f:X→Y in NNTens がΔと整合するとします。このとき、f;ΔY = ΔX;(f×f) : X→Y×Y in NNTens が成立します。等式の左辺/右辺を具体的に書き下してみます。

   (f;ΔY)[x→y', y'']
 = (y | f[x→y]Δ[y→y', y''])
 = if y = y' = y'' then f[x, y] else 0

   (ΔX;(f×f))[x→y', y'']
 = (x', x'' | Δ[x→x', x'']f[x'→y']f[x''→y''])
 = if x = x' = x'' then f[x→y']f[x→y''] else 0

整合性は次の等式となります。

  • (if y = y' = y'' then f[x, y] else 0) = (if x = x' = x'' then f[x→y']f[x→y''] else 0)

等式の両辺が等しくなるためには、y' = y'' 以外の部分では、(右辺のテンソル)[x→y', y''] = 0 です。したがって、次が成立します。

  • y' ≠ y'' ならば、f[x→y']f[x→y''] = 0

fの係数(成分)は非負実数なので:

  • f[x→y']f[x→y''] = 0 ⇔ f[x→y'] = 0 または f[x→y''] = 0

結局、

  • y' ≠ y'' ならば、 f[x→y'] = 0 または f[x→y''] = 0

これが任意のxに対して成立するので、fは非分散テンソルです。

また、y' = y''( = y) である部分に関しても、次の制約があります。

  • f[x, y] = f[x→y']f[x→y'']

y = y' = y'' なので、

  • f[x, y] = (f[x→y])2

これは、f[x→y] = 0 または f[x→y] = 1 を意味するので、fはブール・テンソルです。

これで、f:X→Y in NNTens がΔと整合することは、fが非分散ブール・テンソルであることだと分かりました。x∈X に対して、f[x→y] = 1 となるyは高々1つで、残りの係数(成分)f[x→y]はすべて0です。

次に、f:X→Y in NNTens がεと整合するときを考えます。そのとき、f;εY = εX : X→I in NNTens が成立します。

   (f;εY)[x→*]
 = (y | f[x→y]ε[y→*])
 = (y | f[x→y]ε)

   εX[x→*]
 = 1

これより、(y | f[x→y]ε) = 1 がすべての x∈X で成立します。つまり、fはマルコフ・テンソルです。

Δとεの両方と整合するテンソルNNTensの射)は、非分散ブールかつマルコフなテンソルとなります。これは、x∈X に対して、f[x→y] = 1 となるyは1つだけあり、残りの係数(成分)f[x→y]はすべて0となるテンソルです。

非分散ブールかつマルコフなテンソルとは、有限集合XからYへの写像と同じことです。関係圏の場合と同様に、余可換コモノイド・モダリティ(Δ, ε)と整合する部分圏として(有限)集合と写像の圏が再現します。

参考文献

非負実数テンソルの圏NNTensには余可換コモノイド・モダリティが載ります。余可換コモノイド・モダリティ付きの圏としては、NNTensRel(関係圏)はかなり類似しています。現象としては「面白いな」と思いますが、たまたまやってみた計算が発端なので、全体の構図は見えません。よく分からなくてモヤモヤしてます。

とりあえず、ヒントになりそうな論文を挙げておきます(過去に言及した論文達ですが)。

古め(1999年)の論文ですが、色々なアイディアや話題が詰め込まれています。セリンガーが対角(diagonals)と呼んでいるものは余可換コモノイド・モダリティです。

今年(2017年)になって書かれたものだと思います。使われている絵算(pictorial/graphical/diagrammatic calculation)は、余可換コモノイド・モダリティを含むものです。測度論の晦渋な議論に入り込むのを上手に避けながらdisintegrationの計算をしています。

デカルト微分圏をはじめて(2009年頃)導入した論文です。非関手的(non-functorial)/非自然(non-natural)な構造を色々使っている点で参考になるでしょう。

2017-04-24 (月)

圏論的モダリティ:圏上の非自然な構造達

| 09:28 | 圏論的モダリティ:圏上の非自然な構造達を含むブックマーク

圏論的モダリティ(categorical modality)は、圏の対象に構造を持たせるメカニズムです。ただし、構造の素材が関手や自然変換とは限りません。モダリティは、圏の射と整合しない付加的構造を対象に導入する方法だとも言えます。

「モダリティ」という言葉は耳慣れないかも知れませんが、線形論理の意味論や微分圏では、"exponential modality", "storage modality", "resource modality", "coalgebra modality" といった言葉を使います*1。ここでは、線形論理特有のニュアンスは取り除いて、一般的な広い意味で「モダリティ」を使います*2

僕がモダリティに興味を持つ動機については最後の節に書いてあります。

内容:

  1. 集合圏の付点モダリティ
  2. ユークリッド空間のあいだのなめらかな写像の圏のベクトル空間モダリティ
  3. 圏論的モダリティの定義
  4. 対称モノイド圏の余可換コモノイド・モダリティ
  5. 僕のモダリティ経験

集合圏の付点モダリティ

集合圏Setにおいて、その対象(つまり集合)で添字付けられた射(写像)の族 θX:1→X を考えます。ここで、1 = {0} はSetの終対象である単元集合です。圏Setと、射の族 θ = (θX | X∈|Set|, X≠¥emptyset) を一緒にした(Set, θ)を考えます。

集合Xに対する θX:1→X により、Xの一点θX(0)が定まるので、空でないすべての集合が付点集合(pointed set)の構造を持ちます。ここで大事なことは、θが自然変換ではないことです。

θが自然変換 θ::(1への定数関手)⇒IdSet:SetSet なら、任意の f:X→Y in Set に対して次の図式が可換になるはずです。

1 -(θX)→ X
|        |f
↓        ↓
1 -(θY → Y

しかし、すべてのfに対して f(θX(0)) = f(θY(0)) なわけではありません。つまり、θは自然変換にはなりません

θのような、自然変換とは限らない射の族を圏論的モダリティ(categorical modality)、混乱の恐れがなければ単にモダリティと呼びます(後でもっと正確な定義を述べます)。θは、各対象に付点集合の構造を与えるので付点モダリティ(pointed-set modality)と呼ぶことにします。

f(θX(0)) = f(θY(0)) であるようなfを考えることはできます。そのようなfを付点モダリティθと整合する(consistent)射と呼びましょう。θと整合する射の全体は圏Setの部分圏を定義します。その部分圏に限定するならば、先の図式は可換となるので、θは部分圏においては自然変換となります(空集合の扱いに注意が必要ですが)。

θと整合する射の全体からなる圏は、付点集合の圏PtSetとは違います。例えば、集合{0, 1}を考えると、この集合を台集合(underlying set)とする付点集合は ({0, 1}, 0), ({0, 1}, 1) の2つがあります。どちらもPtSetの対象となります。しかし、集合{0, 1}に対するモダリティ(の成分)θ{0, 1}はひとつしかありません。θ{0, 1}で導入される付点集合は、({0, 1}, 0)か({0, 1}, 1)のどちらか一方です。

集合圏Setに付点モダリティを付けることは、空でない各集合からその要素を1個選び出す究極の選択関数の存在を仮定して、そのような選択関数を1個指定することです。

ユークリッド空間のあいだのなめらかな写像の圏のベクトル空間モダリティ

初等的な多変数微分を扱う舞台となるような圏を定義しましょう。C(Rn, Rn) は、ユークリッド空間Rnで全域的に定義されて、Rmに値を取るなめらか(無限回微分可能)な写像の全体とします。

有限次元ユークリッド空間を対象とする圏を考えたいのですが、Rn←→n と1:1対応するので、n次元ユークリッド空間の代わりに単なる整数n(n≧0)を使うことにします。その前提で、圏ESmoothを次のように定義します。(EはEuclideanのつもり。)

  • |ESmooth| = N = {0, 1, 2, ...}
  • ESmooth(n, m) = C(Rn, Rn)
  • 射の結合は、写像としての結合(合成)。
  • 恒等射idnは、RnRnの恒等写像

集合圏の場合と同様に付点モダリティθを定義します。今回のθは、次のような非常にハッキリした定義を持ちます。

  • θn:0→n in ESmooth
  • その実体は、関数 θn:R0Rn
  • R0 = {0} なので、θn(0) = (Rnのゼロ) と定義する。

θ以外に、ψ = (ψn:(n + n)→n in ESmooth | n∈N), τ = (τn:n→n in ESmooth | n∈N), μ = (μn :(1 + n)→n in ESmooth | n∈N) も定義します。

  • ψn:(n + n)→n の実体は、Rn×RnRn の足し算。
  • τn:n→n の実体 RnRn は、反ベクトル(xに対する-x)を対応させる写像
  • μn :(1 + n)→n の実体は、R×RnRn の(左からの)スカラー乗法。

(θ, ψ, τ, μ)は、ESmoothの各対象n(実体はRn)の上に、標準的なベクトル空間の構造を与えます。(θ, ψ, τ μ)を、圏ESmooth上のベクトル空間モダリティvector space modality)と呼びます。モダリティを定義するために、複数の“射の族”を使ってもかまいません。ベクトル空間モダリティでは、4つの族を使っています。

明白に書いていませんが、(θ, ψ, τ, μ)は、すべてのn(あるいはRn)において、ベクトル空間の公理を満たす必要があります(実際に満たします)。モダリティには、公理を添えてもいいのです(というか、ほとんど場合に公理も付きます)。

ESmoothの射は任意のなめらかな写像なので、ベクトル空間モダリティと整合するとは限りません。ベクトル空間モダリティと整合する射は、ユークリッド空間のあいだの線形写像です。ベクトル空間と整合する射が作るESmoothの部分圏は、行列の圏と圏同値(より強く圏同型)です。

圏論的モダリティの定義

自然変換に似ていても自然性(naturality)を持たないものを考え、それを使って改めてモダリティの定義をします。

Cを圏として、Mor(C)はCの射の集合とします。写像 ξ:|C|→Mor(C) を仮に非自然変換(non-natural transformation)と呼びましょう。これは、Cの対象で添字付けられた射の族です。S(X) := dom(ξX), T(X) := cod(ξX) と置くと、ξX:S(X)→T(X) と書けます。もちろん、S, Tは関手ではなく、関手に拡張する必要もありません。S, Tは関手である必要はありませんが、部分的に定義された関手のようなものです。さらに、ξ:|C|→Mor(C) に部分写像(未定義部分があってもいい)を許したときは、部分非自然変換(partial non-natural transformation)と呼びます。

[追記]非自然変換の定義について、別エントリー「非全域関手と非自然変換」に詳しく書きました。[/追記]

例えば、集合圏Set上の付点モダリティの θX:1→X は部分非自然変換(のX成分)です。X = ¥emptyset に対するθは定義されてないのでθは部分的です。一方、ESmooth上で定義されたθ, ξ, τ, μはいずれも全域的な非自然変換です。

C上で定義されたいくつかの非自然変換/部分非自然変換と、等式や可換図式で記述されたいくつかの公理(法則)を一緒にしたものを、圏C圏論的モダリティ、あるいは単にモダリティと呼びます。

モダリティが部分非自然変換を含む集まりで定義されているとき、そのことを強調したいなら部分モダリティ(partial modality)と呼びます。全域非自然変換だけで作られるモダリティは全域モダリティ(total modality)です。集合圏Setの付点モダリティは、空集合では定義されないので部分モダリティです。一方、ユークリッド空間のあいだのなめらかな写像の圏ESmoothの付点モダリティは全域モダリティです。

対称モノイド圏の余可換コモノイド・モダリティ

モダリティの重要な例として、対称モノイド圏の余可換コモノイド・モダリティ(cocommutative comonoid modality)を紹介します。余可換コモノイド・モダリティは、対称モノイド圏のすべての対象に余可換コモノイド構造を与えるものです。圏の射が余可換コモノイド・モダリティと整合する必要はありません。言い方を換えると、圏の射が余可換コモノイド構造に対する準同型になることは要求しないのです。

C = (C, ¥otimes, I, α, λ, ρ, σ) を対称モノイド圏とします。α, λ, ρはそれぞれ、結合律子(associator)、左単位律子(left unitor)、右単位律子(right unitor)、対称(symmetry)です(律子に関しては「律子からカタストロフへ」を参照)。対称モノイド圏Cの余可換コモノイド・モダリティの素材は、次の2つの全域非自然変換です。

  • δX:X→X¥otimesX in C
  • εX:X→I in C

δXは余乗法、εXは余単位です。これらは余可換コモノイドの公理を満たします。以下で、idXを単にXと書いています。

  • [余結合律] δX;(δX¥otimesX) = δX(X¥otimesδX)
  • [左余単位律] δX;(εX¥otimesX) = X
  • [右余単位律] δX;(X¥otimesεX) = X
  • [余可換性] δXX = δX

対称モノイド圏Cが、余可換コモノイド・モダリティ(δ, ε)を持つとき、Cの対象はすべて余可換コモノイド構造を持つことになります。しかし、Cの射が余可換コモノイド構造の準同型になることは全く保証されません。余乗法δXや余単位εXを保存(preserve, respect)しない射がたくさんあるかも知れないのです。

[追記]余可換コモノイド・モダリティの説明はコチラにもあります。[/追記]

僕のモダリティ経験

セリンガー(Peter Selinger)の1999年の論文"Categorical Structure of Asynchrony"に、対角付き(対称)モノイド圏(monoidal category with diagonals)という概念が出てきます。これは余可換コモノイド・モダリティを持つ圏と同じものです。セリンガー論文を読んだのは随分と前ですが、自然変換とはならない(かも知れない)射の族を使う方法は印象に残っています。

最近読んだ長健太(Kenta Cho)/バルト・ヤコブス*3(Bart Jacobs)の論文"Disintegration and Bayesian Inversion, Both Abstractly and Concretely"に、セリンガーの“対角”と同じ余可換コモノイド・モダリティが出てきます。

「ンン? 非同期通信/処理とベイズ確率って何か関係あるのだろうか?」と疑問に思いました。共通点があるとすれば、部分性(partiality)や非決定性(nondeterminism)です。試しに、非負実数係数のテンソルの圏に余可換コモノイド・モダリティを入れてみると、そのモダリティと整合する部分圏として部分性と確率的非決定性の両方がうまく定義できるようです。これが分かったとき、僕にとってはA-ha momentでした。


モダリティは、“対象達が持つ構造”の圏論的な定式化のひとつです。自然性を持たず、射を準同型として扱うことは出来ませんが、非自然であり部分的かも知れないことに注意すればとても便利な概念です。

非全域関手と非自然変換

| 12:30 | 非全域関手と非自然変換を含むブックマーク

圏論的モダリティ:圏上の非自然な構造達」への追記ですが、別エントリーにします。圏論的モダリティ(categorical modality)を定義するために、非自然変換(non-natural transformation)という概念を導入しました。この非自然変換の定義をここで詳しく述べます。

まず、部分的に定義された関手をpartial functorと呼ぶのですが、partial functorの訳語で悩みます。

partial = non-total なので「非全域」という言葉を使うことにします。ここでの「非全域」は「全域ではない」という意味ではありません。「必ずしも全域とは限らない」です。「非可換」というよく使う言葉も「必ずしも可換とは限らない」の意味なので、「非」のよくある用法だと思います。「非自然」も同様な解釈をします。

  • 全域関手は非全域関手の特別なもの。
  • 可換環は非可換環の特別なもの。
  • 自然変換は非自然変換の特別なもの。

よろしいでしょうか。

念のため、非全域関手をホムセット中心のスタイルで定義しておきます。Fが関手のとき、その対象部分(object part)をFobj、射部分(morphism part)をFmorとします。非全域関手では、FobjもFmorも非全域(部分的)になります。Fが非全域関手であることを詳しく言うと:

  1. C, D は圏とする。
  2. Fobj:|C|→|D| は非全域写像(部分写像)である。
  3. A, B∈|C| がFobjの定義域に入るとき、FmorA,B:C(A, B)→D(Fobj(A), Fobj(B)) が定義されるが、これも非全域写像である(必ずしも全域である必要がない)。
  4. A∈|C| がFobjの定義域に入っているなら、idAはFmorA,Aの定義域に入っている。
  5. 通常の関手と同様に、射の結合と恒等射を保存する。

対象Aに対するF(A)も、射fに対するF(f)も、定義されないことがあっても別にいい、ということです。定義されている範囲内で考えれば通常の関手と同じ扱いができます。

F, G:CD が非全域関手とします。α:|C|→Mor(D) という非全域写像が、FからGへの非自然変換だとは次のことです。

  • αA が定義されているなら、F(A)もG(A)も定義されている。
  • dom(αA) = F(A)、cod(αA) = G(A) である。

α::F⇒G と書くと、自然変換と区別が付かないので、α::F ?⇒ G とでも書けばいいかな。非全域関手であることも明示するなら、α::F ?⇒ G:C⊃→D とか。

Cの射 f:A→B in C が、非自然変換αと整合する(consistent, compatible)とは、次の図式が可換になることです。(図式内のα_AはαAのこと。)

F(A) -(α_A)→G(A)
|            |
F(f)          G(f)
↓            ↓
F(B) -(α_B)→G(B)

この可換図式が意味を持つには次の前提が必要です:

  • AもBも、αの定義域に入っている。
  • fはFA,Bの定義域にも、GA,Bの定義域にも入っている。


非全域関手や非自然変換のような変なものをなぜ考えるのでしょう? その答は「使うから」「役に立つから」です。

セリンガーの論文で非自然な構造(対角構造)を見たとき、僕も違和感を感じました。しかし、「非自然変換に整合する射」という形で既存の概念がエレガントに再定式化されるのです。特に役に立つのは、2つの非自然変換から構成される余可換コモノイド・モダリティです。余可換コモノイド・モダリティの事例はそのうち述べるつもりです。

*1:例えば、Robin Cockettの"Seely categories revisited"(http://pages.cpsc.ucalgary.ca/~robin/talks/seely.pdf)、Blute, Cockett, Seelyの"Differential categories"(http://aix1.uottawa.ca/~rblute/difftl.pdf)。

*2:モダリティの本来の意味については、例えば https://ncatlab.org/nlab/show/modality 参照。

*3:英語読みなら「バート・ジェイコブス」が近いかも知れません。