2015-05-01

well-definedness と universal map

well-definedness 周りの議論ってわりと何してるのかわかりにくくない？と思って考えてたら universality のほうがわかりやすい気がしてきりしたので書いてみた。

以下 $A$ , $B$ は集合， $E$ は $A$ 上の同値関係。

well-defined とは

写像 $f: A/E \to B$ が well-defined であるとはどういうことか，ということから一応。

まず well-defined であるという述語は，写像そのものに適用されるものというよりは，その定義に適用されるものであることに注意する。確かに言葉の上では「この写像は well-defined である」などという言い方をするのだが，このような言明は普通，写像の定義に伴って表れるものであり，その実際の内容は「今述べた定義は確かに写像を一つ定めている」ということである。したがって意味的には well-defined とは数学的対象に関する概念ではなくその記述方法というメタなレベルのことがらに関する概念であるということになる。

では $f([a]) = e\{a\}$ を写像 $f$ の定義だとしよう。ここで $a$ は変数であり $[a]$ は $E$ に関する同値類を表す。右辺の $e\{a\}$ *1 は $a$ を含む式である。変数とは何かとか式とは何かとか言い出すと面倒なことになりそうなので，細かいことは言わないで素朴に解釈することにしてほしい。それと，別に式を使って等式の形で定義を述べなければならないわけではないが，話を簡単にするためにそうした。

これが well-defined であるとはどういうことか。写像 $f$ に渡されるものは $A/E$ の要素であり，すなわち同値類なのだから，少なくとも建前としてはまず同値類 $x \in A/E$ が与えられ（この時点では代表元は与えられていない）， $f(x)$ を定めなければならない。そのために同値類から代表元 $a \in x$ を取って云々，とやるのだから， $a$ のとり方を変えたときに式 $e$ が違う値になってしまうといけない。そのような問題が起きない，ということが well-defined であるということである。正確に書けば $a E a' \implies e\{a\} = e\{a'\}$ でなければならない。これが確かめられればさっきの $f$ が確かに写像として定義される，すなわち well-defined であるということが結論できる。こういう話であった。

写像の分解と見る

さっき $e\{a\}$ は「式である」と雑な言い方をしたが，要するに $a$ は $A$ の元を指示する変数であり， $e\{a\}$ は $B$ の元を表すのだから， $e\{a\}$ と書いたのは結局のところ写像 $e : A \to B$ であると思ってもよさそうである。（このあたりはずいぶんいい加減なようだが，そもそも大雑把な話をしているということで見逃してほしい）

そうるすとさっきやったことは見方を変えてこのように理解できる。写像 $e : A \to B$ を与え，それが性質 $a E a' \implies e(a) = e(a')$ を持つことを確認せよ。それができれば確かに $f: A/E \to B$ が定義されたことになる。これが商集合上の写像が well-defined であると言うときに行われていることである。

ついでに言うとこの $f$ は， $\pi : A \to A/E$ を射影として $f \circ \pi = e$ を満たす。つまり，最初に与えた写像 $e$ を射影によって分解することで欲しい写像を得ているのである。

よく見てみると，こちらの見方の中には「定義の記述」のようなものが現れないことがわかる。そうではなくて，いきなり定義しようとしている写像の定義域 $A/E$ を考えないで，まずは商をとる前の $A$ からの写像を定めよ，そしてそれがある性質を満たしていることを確認せよ，そうすれば望む写像が得られる，と言っている。つまり，いきなり商集合の上の写像を定義しようとするとそれがちゃんと定まるかどうかがわからないので「その定義は well-defined であるかどうか」というメタな話が出てくるのに対して，商をとる前の集合を相手にすることで「別のある写像が要求された性質を満たすかどうか」という数学的対象についての話に置き換わったわけだ。

メタレベルを意識しなくても理解が可能な分，後者の説明のしかたのほうがすっきりしていて分かりやすいように思われる。初学者にとってどうかはわからないが，僕にとってはこちらのほうが納得がいくように感じる。

普遍写像性

ところで，これに似たような状況は数学でよく出てくる。いわゆる普遍写像性というやつである。

その言葉でさっきの話をきちんと書くとこうなる。関手 $\Delta: \mathbf{Set} \to \mathbf{Setoid}$ を $\Delta(X) = (X, \Delta_X)$ （つまり集合をその上の普通の意味の等しさと組にして setoid とみなす）で定めたとき，setoid $(A, E)$ から $\Delta$ への universal arrow が射影 $\pi: A \to A/E$ である。

随伴関手の言葉にすると，上の $\Delta$ は setoid $(A, E)$ から商集合 $A/E$ を作る関手の右随伴であると言うことができる。すなわち $\mathbf{Set}(A/E, B) \simeq \mathbf{Setoid}( (A, E), \Delta(B) )$ である。また，この同型は $\pi: A\to A/E$ による引き戻しで与えられる。

普通の議論のしかたをこの表現と対応付けてみる。いま写像 $f : A \to B$ があり，これが $a E a' \implies f(a) = f(a')$ を満たすとする。これはすなわち， $f \in \mathbf{Setoid}( (A, E), \Delta(B) )$ を仮定するということに他ならない。このとき， $\bar f : A/E \to B$ であって， $\bar f \circ \pi = f$ を満たすものが一意的に存在する。これは， $\pi$ による引き戻しが全単射であるという上に述べた事実の単なる言い換えである。

*1:あまり標準的でない記法なのは他の括弧を使うと紛らわしかったため

2015-03-14

Extensional axiom of choice という公理があるらしい

二年前に直観主義と選択公理の話という記事を書いたのですが，それに近い内容の論文を 2006 年に Martin-Löf が書いていたこと知りました。"100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?" というタイトルの論文で，Springer から出版されています (http://link.springer.com/chapter/10.1007%2F978-1-4020-8926-8_10) が，同じ内容と思われる（確認してないけど） pdf が https://people.kth.se/~kurlberg/colloquium/2005/MartinLooef.pdf で公開されています。

この論文は，どうして選択公理は BHK 解釈のもとでは自然に成立するように思えるのに排中律を導くという非構成的性質を持つのか，ということを論じたもので，結論は「関数の存在はいえても，その外延性が保証できない，つまり等しい値に対して等しい結果を返すことが証明できないから」ということで上記の記事と一致しているようです。

Extensional axiom of choice

その論文中で導入されている extensional axiom of choice (ExtAC) という公理が面白かったので，それについて議論されていることをまとめておきます。技術的詳細には立ち入りません，というか以下の議論が正確にはどう形式化できるのかよく理解できてない部分があります。しかし詳細がわからなくても informal な説明としてはそれらしいものであると思います。

ExtAC は，普通の集合論の中ではただの AC と区別がつかないのですが，構成的型理論 (CTT) の中で考えると AC と同値ではない公理です。この ExtAC と AC の差を観察することで選択公理が成り立つ集合論が非構成的になる理由がわかる，という点が面白いところです。

ExtAC を考えるための前提として，型における等しさの概念は型そのものの定義とは別に与えられると考えることに注意が必要です。CIC のように inductive type をもつ型理論では identity type は一様に定義できますし，Martin-Löf 流の型理論でも同様のやり方で導入することができますが（propositional equality と呼んだりする），それとは別に等しさを考えるということです。別の言い方をすると，ただの型ではなく setoid を考えるということです。

いま I と S を型とし，その上の等しさが与えられたとして，それらを各々 $=_I$ , $=_S$ と書くことにしましょう。これらの等号については，それぞれ I と S の上の同値関係であることしか仮定しません。また，以下 A は $I \times S$ 上の述語でこれらの等号を respect する（つまり $i =_I j$ かつ $x =_S y$ なら $A(i, x) \leftrightarrow A(j, y)$ である）ものとします。

まず，通常の選択公理 AC は

$\forall (i : I) \exists (x : S) A(i, x) \rightarrow (\exists f: I \to S)(\forall i : I) A(i, f(i))$ *1

となります。これは等しさに言及しないバージョンで，この形のものは CTT で証明できるのでした。ただし， $i =_I j$ だからといって $f(i) =_S f(j)$ かどうかはわからないことに注意しましょう。等号は任意に与えた同値関係としたのだから，確かに CTT における AC の証明はこれを満たす f を与えるとは限らないでしょう。

ExtAC は以下のように定式化されます。

$\forall (i : I) \exists (x : S) A(i, x) \rightarrow (\exists f: I \to S)(\mathrm{Ext}(f) \wedge (\forall i : I) A(i, f(i)))$

ただし Ext(f) は f が外延的であることを表す述語で，次のように定義されます。

$\mathrm{Ext}(f) = (\forall i, j : I) (i =_I j \to f(i) =_ S f(j))$

また，正確には一番外側に $=_I, =_S$ を束縛する全称量化子（とそれらに関する諸々の条件）が付くと思いますが省略しています。

AC と違って，ExtAC は CTT では証明できません。論文中では，実は ZFC から CTT + ExtAC への翻訳が存在することが示されています（"ZFC is interpretable in CTT + ExtAC" と書いてありますが，そういうことでしょう）。ということは，ラフな言い方をすると，集合論的な意味での AC に相当する型理論の公理は AC ではなく ExtAC であることがわかります。

証明の詳細をきちんと確かめていないのですが，だいたいどういうことかというと，集合論では集合の商をとることができるのがポイントになっているようです。このことは，与えられた同値関係の意味での同値性を，集合としての等しさに置き換えることができるということを意味します。もし述語 A が与えられた同値関係を保てば，A は商集合の上の述語としても well-defined ですから，先に商をとったうえで AC を使うことで ExtAC 相当のことができるのでしょう。

補足しておくと，通常の集合論においては等しさの概念は論理に組み込まれているものを使いますから，どんな関数も等しさを保存するということは集合論がその上に乗っているところの一階述語論理のレベルで保証されています。したがって，そもそも外延的でない関数など存在するはずがないので，Ext(f) は恒真であり，そのような述語は何を言っていないのと同じです。だから当然，ExtAC 相当のものを集合論で考えても，それはただの AC と同値です。したがって両者は集合論においては区別できません。

このように AC と ExtAC を区別したうえで議論をすると，集合論において選択公理がどのようにして構成的でない結論を導いているのかが見えやすくなります。両者の差は Ext(f) を要求するかどうかにあるわけだから，その違いが効いているということです。つまり Ext(f) を満たすような f を構成的に与えることはできないのです。これで最初に述べたように，選択関数が作れないのは選択できないからではなく外延性が保証できないからである，という結論に到達しました。

二年前の記事では同じ事情を「多価でもよいなら選択関数は存在する」という形で表現したのですが，今回紹介した Martin-Löf の議論はその別表現と言うことができるでしょう。

*1:ここでは量化子は他の結合子よりも強く結合することにします

2015-02-27

世界が 11 次元だとすると重箱の隅は 1024 個もあるのでつつき放題

日常

何がきっかけか忘れたのですが，一般に n 次元の重箱には隅が 2^(n-1) 個あるのだなということを思ったので，たいした話ではありませんが書いてみることにしました。

n 次元重箱とは，n 次元立方体の境界から一つの側面の内部を除いた図形である。具体的には，例えば $\mathbb R^n$ の点であって少なくとも一つの座標が 0 または 1 である点の集まりから，第 n 座標のみが 1 であるような点をすべて除いてできると考えてよい。その場合，重箱の隅とは，第 n 座標が 0 であり，その他のすべての座標が 0 または 1 であるような点のことである。

そうすると，隅の集合は $\{0, 1\}^{n-1} \times \{0\}$ だから $2^{n-1}$ 個ある。だから例えば通常の 3 次元重箱には隅が 4 個あり（これはわれわれがよく知っている重箱の隅の個数と一致する），11 次元なら 1024 個ある。

2015-02-22

数遊び

日常

ある日の夜，寝ようとして布団に入った瞬間に，どういうわけか 676 という数字が浮かんできた。

見覚えのある数字だ。でもどこで見たのだろうか。平方数か何かだろうか。そういえば 24 の二乗はそんな感じの数だった気がする。そこで計算してみると $24^2 = 4 \times 12^2 = 4 \times 144 = 576$ ，ちょっと違う。

試しに素因数分解でもしてみようと思う。676 = 700 - 20 - 4 で右辺に出てくるのは 4 の倍数だから，676 は 4 で割り切れる。そこで試しに割ってみると 676 = 4 * 169 となる。169 は知っている。13 の二乗である。

ということは $676 = (2 \times 13)^2 = 26^2$ なのか。そういえばそうだったような気がする。

そうすると 576 と 676 はいずれも平方数なのだ。そんなことがあるだろうか？というのは，平方数は疎らにしか存在しないように思えるので，両者の間隔がちょうど 100 というきりのいい数になるということはそれほどありそうにない。*1

それではなぜ $26^2 - 24^2 = 100$ なのか。計算してみればそうなる，というのは論理的に正しいが，論理的に正しい証明が必ずしも納得をもたらすわけではない。

そういえば，24 と 26 の間には 25 があり，100 は 25 の倍数である。たぶんここから何かわかるのではないか。

平方数が奇数の和であることを思い出そう。つまり $n^2 = \sum_{k=1}^n (2k-1)$ である。そうすると $25^2 = 24^2 + 49$ と $26^2 = 25^2 + 51$ がわかるから（これは $(x \pm 1)^2 = x^2 \pm 2x + 1$ を使っても確かめられる），確かに $26^2 - 24^2 = 49 + 51 = 100$ でなければならないとわかった。少し納得した。

こんなことを考えているから眠れない。

*1:もちろんありそうにないからといってありえないという根拠にはならないし，そもそもありそうにないという感覚はよくある認知バイアスの一例である。例えば 1 以上 1000 以下の整数をランダムに選ぶとき，100 というきりのいい数字が出る確率が，623 のようなきりのよくない数が出る確率に比べて低いわけではない。同様に，二つの平方数を持ってきて差を計算したらちょうど 100 になるという出来事が，単にそれがきりのいい数だというだけで他の数が出てくるのに比べてありそうにないことだと主張することはできない。しかし僕の頭はこのような判断を一瞬で下せるほどにはよく働かなかった。

2015-02-14

掛け算の順序を区別するなら割り算は二つ必要

joke 日常

掛け算記号の左右の役割は異なるので順番を入れ換えてはいけないという立場がある。左側は「一単位あたりいくつ」を表し，右側は「何単位分あるか」を表すのであり，それらを逆に書いてはいけないのだという。例えば，2×3=6 と書いたらそれは「三人がそれぞれ二つずつみかんを食べた」という状況は表すが「二人がそれぞれ三つずつみかんを食べた」という状況は表さない，ということだと理解している。

その立場を貫こうとすると，掛け算記号の左側を求めるための割り算と右側を求めるための割り算の二つが別々のものとして導入されねばならないように思う。2×3 と 3×2 で意味が異なるのだったら，□×3=6 と 2×□=6 のそれぞれにおいて □ に入る値を求めようとするとき，両者において用いられるべき演算が同じである理由はない。□ はそれぞれ異なる役割を担う位置に置かれているのだから，それを求めるのにも異なる演算が用いられると考えるのは道理であるし，実は同じ演算で求まるのですと言われてもそう簡単に納得できるようには思えない。実際それらを区別する用語はあって，前者を等分除，後者を包含除と呼ぶ。

しかし，両者を概念として区別することはあっても，例えば異なる記号で表すなど，構文的に区別しているのを見たことはない。これはどうしてだろうか。掛け算の左右を区別するのと同じように，二つの割り算も構文的に区別するべきではないか。そうしないと混乱の元であるのに，横着をして両者をごっちゃにしてはいけない。

というわけだから，□×3=6 の □ を求めるための演算と，2×□=6 の □ を求めるための演算を区別するために，いま仮に前者であるところの等分除を／で表し，後者であるところの包含除を＼で表すことにすれば

□×3=6 ⇔ □=6／3

であり，また

2×□=6 ⇔ □=2＼6

のように書くことができる。こうすれば見た目にも別々の演算であることが明らかで，わかりやすいのではないか。

最後に参考文献をひとつ挙げておこう。

Residuated Lattices: An Algebraic Glimpse at Substructural Logics: An Algebraic Glimpse at Substructural Logics (Studies in Logic and the Foundations of Mathematics)

作者: Nikolaos Galatos,Peter Jipsen,Tomasz Kowalski,Hiroakira Ono
出版社/メーカー: Elsevier Science
発売日: 2007/04/25
メディア: Kindle版
この商品を含むブログを見る

2015-02-02

Coq 8.5 を入れてみた

先日 Coq 8.5 がリリースされたので入れてみた話。

coq 自体のコンパイルは問題なくできたけど，その後 ssreflect のコンパイルに失敗した。make すると

Error: The files /usr/local/lib/coq/parsing/pcoq.cmi
       and /usr/local/lib/coq/lib/compat.cmi make inconsistent assumptions
       over interface Compat

と言われる。問題の compat.cmi はタイムスタンプを見ると Coq の前のバージョンのものらしいことがわかる。どうもソースコードのディレクトリ構成が変わっているようで，新しい compat.cmi は別のディレクトリに存在している。それで Coq を make install したときに上書きされずに古いものが残って，何らかの理由でそれが間違って参照されているようだ。

試しに

sudo rm -fr /usr/local/lib/coq/

してから coq をインストールし直してみると，今度は ssreflect の make に成功した。

mathcomp もコンパイルし直さないといけない。試しに make -j16 とかやってみたら 20 分ちょっとでコンパイルが終わった。

2014-12-19

風呂場でする遊び

日常

さっきシャワーを浴びながら考えていたことなど。

8 って 9 - 1 だから平方数（以下，平方数に 0 は含めないことにする）の差だなーということをまず思った。なんで 8 のことを考えていたかは省略する。というかよく覚えていない。

平方数の差はたくさんあるので，これだけだとそんなに面白くない。もうちょっと強い条件はなにか考えられないだろうか。

例えば平方数の差で表せる正の数の中で 8 はどれくらいの位置にいるだろうか。そういう数の中で一番小さいのは 3 である。その次は 5 である。その次ぐらいじゃないか？と思ったが，よく考えたら 7 = 16 - 9 だから違った。

しかし以上のことから，平方数の差で表せる正の数のうち平方数の差で表せる最小の数番目に小さい数は 7 であることがわかった。8 はその次。

7 までに現れる数はすべて奇数だったので，8 の特徴付けとして「平方数の差で表せる最小の正の偶数」というものが考えられることもわかる。

考えてみれば 3 以上の奇数は必ず平方数の差で表せるのだった。そして偶数が平方数の差になることは，それが 4 の倍数かつ 4 より大きいことと同値である。いずれも証明は難しくないので読者への演習問題とする。