雑記　契約と例外、数学屋と物理屋

お皿洗いしながら考えていたことをだらだら書きます。

物理屋が書く文章、なんか妙に毎回読みにくいと思ってしまうのですが、そういえばと思うパターンがありました。

議論の中で前提が増えることがある。気がする (偏見)。

つまり…話の途中に「この δ は十分小さいので」「ここは線形と近似できるので」って入ってくる気がする。気の所為かもしれないけど。

数学的証明の気持ちだと前提に全部情報を乗っけてから、それだけを使って帰結を導くわけで、そういう言い方をされると「ならここはまだ証明 (=計算) のフェーズではない」ように思える。

でも「以上によって解くことができた」みたいに言われるから、あれ、今までのはなんだったんだろう、みたいな混乱がある。

最初から必要な前提を全部並べて書いてくれれば素直に証明 (=計算) として読めるのに、って。

(偏見で書いています。)

この差はどこから来たのかという違いで。数学はモデルを仮定してから性質を出すけど、物理はモデルを作る事自体を含めて解くこととされている印象がある。

「こういう (自然言語で記述された) 問題をどう考える？」という問に対して、「こう考えるとこうなるだろう」と答えることが物理の世界なのかなと思う。知らんけど。

もちろん数学もそういうことはするけれど、「問題のモデル化」は早々に終えてしまう印象がある。ここが違うと別分野になっちゃったりするし。

で、すごい雑なことを言うと、数学の証明は M(X) → Y (X のモデルから Y を導き出す) のに対し、物理だと X → S(Y) (概念 X を Y という方向性で解釈する) というフォーカスをしているのかもしれない。

わぁこれはなんとやらだ！

って主張したいわけじゃないけど、まぁ本質的にはここは近い活動なんだろうとは思った。

そんな戯言を考えていたところで思い出した話題があってですね。

プログラムを書くときに「例外」ってちょこちょこ出てくると思うんですよ。そのまま、例外的な状況のことね。

それを対処する方法として「例外機構」というものがあって、要は「こんなのは無理です！」って伝える方法を人類は考えたのでした。

function sqrt(x) {
  if(x < 0) throw むりだよ;
  ...
  return こたえ;
}

まぁ別に所謂 exception の仕組みじゃなくても良い。実際現代では例外機構 (大域脱出を指しています) よりも値として例外を扱うことのほうが良いとされてると思う。

function sqrt(x) {
  if(x < 0) return {error: むりだよ};
  ...
  return {success: こたえ};
}

値の扱いがちょっと面倒になるけど、それはモナドにしてbindを仕込めばいいので大したことではない。

大事なのはこれらが矢印の右側の仕組みだということで。即ちインプットを受け入れた上で、後になってからダメだったと伝えているというわけです。

だけど、当然もっと前から言えたほうが嬉しいじゃないですか。そうすると契約の概念が出てくるんだと思うんです。

function sqrt(x: NonNegative) {
  ...
  return こたえ;
}

つまりインプットの段階で表明し、相手にはこの条件を満たすように契約する。最初からそうできるならそのほうがいいじゃないですか。

で、これは左側のやり方なわけですね。

そして右側による解決、左側による解決、どちらも表現しているものは一緒なはずなのです。そうですよね。

あぁじゃあこれもなんとやらなのか――って思う前に、このやり方なら数学的に記述すれば厳密なチェックをさせることができますね。

つまり… F,G が随伴函手対であるなら F(X) → Y と X → G(Y) がちょうど一対一対応できて、X と Y について自然でなければならないのでした。

本当にちゃんと書くと、私が今考えたい問題は $\mathbf{Set}$ における自己函手 $X\mapsto X\sqcup 1$ の左随伴です。

そして、そんな函手は存在しないのです。

何故なら函手の性質を満たせないからですね。解きたい問題によって与える制約を変えなきゃいけないからです。

制約を式で書くことはもちろんできて、 $g:X\to Y\sqcup 1$ に対して $F_X = \{x\in X\mid g(x) \ne \mathrm{inr}(*)\}$ を定義してあげればどうにか $f:F_X \to Y$ という写像を構成できます。しかしこれは本質的に $g$ に依存した定義なので、あの美しい構造にはならないのです。