気軽に引き算するな

昼から晩までずっと,研究で開発したライブラリとその使用例を整理していた.まあ,結構綺麗な使用例ができたでしょう.

ところで,Ackermann関数が原始再帰的でないことを証明するときに使う

Lemma ack_inc :
  forall c1 c2 : nat , exists c3 : nat , forall x : nat ,
        ack c1 (ack c2 x) <= ack c3 x.

だけれども,形式化しようとするとなかなか鬱陶しい.というのも,とある教科書 (有川緑本) にのってる証明だと, c_3 \max\{c_1 - 2, \, c_2 - 1\}として具体的に構成しているのだけれども,自然数上の証明なのに -が出てきているので,形式化しようとするととても鬱陶しい.

というのも,自然数上の引き算  - は,実はモーナス(monus)とよばれるもので解釈することが多く,(整数範囲で引き算を計算して)負になったら0に切り上げられる.つまり, m \geq n ならば,  m - n はそのまま(整数範囲の引き算と同じように)  m - n なのだが, m \lt nならば, m - n 0 になるわけである.まあこれは自然な定義な気がするのだが,実は,例えば  \forall n . S(n - 1) = n が成り立たない (実際, n = 0 のとき, S(0 - 1) = S(0) = 1 \neq 0 である) という致命的な欠点がある.これが形式的な証明の時に結構困るのである (有川緑本の証明は, - がモーナスだと思うと破綻しているので,形式化の際に修正する必要が出てきた).

まあ,自然数上の命題の証明で,気軽にマイナス使うなということで.

閑話休題.とある一覧表を見ていたら,超気になる題目が.というのも,私自身がトライポフォビアな気がするので1


  1. たとえば,夏に,生い茂った植物たちとかお花畑とかをみていると,背筋から首筋あたりが固まってうごかなくなることがある.特に,ひまわり畑が絶対ダメで,写真を見るだけでゾッとしてくる.工業製品の集合体は問題ないのだが,とにもかくにも植物の集合がダメ.私の前で,お花畑の写真などはあまり見せないでほしい,ほんとお願いします.