2015-06-22

多項式の微分は積の微分から出てくる

多項式を微分すると指数が係数に出てくるのって，積の微分の公式 $(fg)' = f' \cdot g + f\cdot g'$ と $x' = 1$ を使って

$(x^2)' = x' \cdot x + x \cdot x' = x + x = 2x$
$(x^3)' = (x^2)' \cdot x + x^2 \cdot x' = 2x^2 + x^2 = 3x^2$

とかやると出てくる。

ということに，多項式を計算機上でいじることについて考えていて初めて気付いた。

2015-06-19

積分

日常

ぼくにとって，数学といえば積分らしい。

それはきっと昔からそうで，ぼくにとって「積分」という言葉と積分記号は特別なものなのだろうと思う。例えば，あなたが誰かに向かって数学の話をしているところを想像して下さいと言われたら，黒板かホワイトボードに積分記号を書いているところを思い浮かべそうな気がする。普段は解析を使うようなことをあまりしないから，積分という概念自体はそれほど身近なものとはいえなくなっている気がするけど，そうなってから何年も経ってもやはりぼくにとって積分の特別さは変わらないものらしい。

どうして積分なのか，ということは，長い間気にしたことがないどころか，積分というものが頭の中の目立つ場所に居座っていることに気付いてすらいなかった。数年前にようやく，どういうきっかけだったか忘れたが，どうやらぼくの頭には積分という言葉が頻繁に浮かんできているようだということに気がついた。その後もそれがなぜなのかを考えた記憶はほとんどない。ところがこの間突然，これもきっかけは忘れてしまったが，もしかしたらあれではないかという記憶に思い当たった。中学の数学の授業中に積分の話を少しだけ聞いたことがあって，それが高校生になって実際に積分を学ぶまでずっと気になっていたのだ。

その中学の授業中に聞いた話というのは，扇形の面積が「半径×弧長÷2」になるということを習ったときに余談として出てきたものだ。この面積の式は三角形のそれと似ているけど，これは偶然ではなくて，細い三角形が無数に並んでいるとみなして計算すればこうなると理解できるということ。それから，今のは厳密ではない説明だけど，積分というのがあって，それを使うとこのアイデアはもっと厳密な議論に落とし込むことができるのだということ。その二つのことを聞いたのだと思う。

それ以上の説明は聞かなかったから，積分というものがどういうものなのかはわからなかった。でも，その時に出てきた「積分」という言葉はそれ以来ずっと覚えていたし，何か気になる，という気持ちを持ち続けていた。過去を思い返してみると，数学に対する興味は昔からあっても，具体的な数学の概念に対して興味を持ったことはそれまでにはなかった気がする。だからもしかすると「よくわからないけどおもしろそうだ」とかいうことを思ったのはそれが最初だったのかもしれない。そういうことがあったから，ぼくの頭の中では「積分」という言葉やあの記号が何か数学の魅力の象徴のようなものとして位置付けられているのだろうか。

2015-06-11

Lean をインストールしてみた

Lean 本体

最初，github にあるソースを自分でコンパイルしようとしたらうまくいかなかった。apt-get で入るので始めからそうすればよかった。

https://leanprover.github.io/download/ に環境ごとのインストールのしかたが書いてある。

Emacs の lean-mode

Emacs のモードがけっこうちゃんとしているみたい。インストールのしかたは https://github.com/leanprover/lean/blob/master/src/emacs/README.md に書いてある。

なんかいろんなパッケージに依存しているらしいけど，Installation のセクションの最初に書いてあるコードを何も考えずに *scratch* に貼り付けて評価したら全部勝手に入った（多分）。最近は elisp のパッケージ管理のための仕組みも整備されてきているようだけど，時代に追いつけていないのでよくわからない。

あとは，本体を apt-get で入れたので Case 2 に書いてあるやつを見て適当にいじって init.el に設定を書いた。

;;; lean-mode
(when (file-exists-p "/usr/share/emacs/site-lisp/lean/")
  (add-to-list 'load-path "/usr/share/emacs/site-lisp/lean/")
  (autoload 'lean-mode "lean-mode" nil t)
  (setq lean-rootdir "/usr")
  (add-to-list 'auto-mode-alist '("\\.h?lean$" . lean-mode)))

lean-rootdir をちゃんとセットしないと lean-mode の挙動がなんかおかしなことになった。lean のプロセスを起動してそれとやりとりしようとしてうまくいってないように見えた。

ドキュメント

https://leanprover.github.io/documentation/ に置いてある tutorial がかなり充実してそう。

まだ Chapter 4 までしか目を通していない（しかも斜め読み）けど，説明は丁寧そうなので証明支援系にそんなに慣れてなくても読めるかも。Curry-Howard 同型の説明とかもしてる。

2015-05-23

普通に日本語を話す

日常

「普通においしい」「普通に嫌い」「普通に言う」などの表現に違和感がある。自己の判断を述べる際に，なぜわざわざ「普通に」と付けるのか。どういう意味で普通だと言っているのかよくわからないし，そもそもそんな疑問が浮かぶ以前に，響きに違和感がある，とも思う。

でもここで正しい日本語がどうのという話をする気はない。

「やっぱり」という言葉がある。この言葉をまったく使わないという人はあまりいないと思うし，よく耳にする言葉だが，それはどういう意味かとあらためて考えてみると，これもまたはっきりしない。

「やっぱり」とは何か，ということについては森本哲郎『日本語表と裏』に面白いことが書いてある。日本人はとかくみんなと同じでなければならないと思いがちで，周りと異なる存在になることを恐れる。そういう傾向を持っているから，何か意見を述べるときにも単に自分はこう思いますと言うだけではなくて，これは異質な意見でも何でもなくて，自分はみんなと同じことを考えているのですと言いたがる。そこで「やっぱり」と付けることで，世間一般の人たちがそう思っているのと同じように，自分もそう思います，というニュアンスを出すのではないか。そんなようなことが書かれている。

普通に，と言うのもそういう意識があるからじゃないだろうか，と思うと腑に落ちる気がした。やっぱり日本語なのだ。

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 個ある。