短い説明は、「証明のやり方」。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\LL}{\langle} % List Left
\newcommand{\LR}{\rangle} % List Right
\newcommand{\T}[1]{\text{#1} }
\newcommand{\hinfer}{ \rightrightarrows }% horizontal meta rule (infer)
\newcommand{\num}[1]{\:\text{ - - }#1 } % numbering, labeling
`$
同じ意味の言葉は揃える
呼び名が揃ってないと、どうしても違ったものに見てしまう。言霊は恐ろしい。
| 一般の場合 | 特殊ケース |
|---|---|
| 関数 | 定理 |
| 組み込み関数（関数記述不要） | 公理＝組み込み定理（定理記述不要） |
| 計算〈無名関数〉 | 証明〈無名定理〉【名詞】 |
| 関数{の}?記述 | 定理{の}?記述 |
| 関数を定義〈記述〉する | 定理を証明する【動詞】 |
| 関数{記述}?のヘッド | 定理{記述}?のヘッド |
| 関数{記述}?のボディ | 定理{記述}?のボディ＝狭義の証明 |
| 関数のプロファイル | 定理のステートメント |
| 関数のドメイン | 定理のの仮定 |
| 関数のコドメイン | 定理の結論 |
| 関数{記述}?の引数変数 | (適切な言葉が無い) |
| 関数{記述}?の戻り値変数 | (適切な言葉が無い) |
できるだけ呼び名・言い方を揃える。
- {関数 | 定理}記述は、名前、ヘッド、ボディからなる。これは、割り当て〈assignment〉の名前、型、項である。
- {関数 | 定理}記述のヘッドには、{関数 | 定理}のプロファイルを書く。
- {関数 | 定理}のプロファイルの{ドメイン | 仮定}は：
- ボディで引数変数を使うなら引数変数名を書く。
- ボディをポイントフリースタイルや絵図で{書く | 描く}なら引数変数名は不要。
- 引数変数名は番号でもよい。
- 番号である引数変数名は省略しても自動挿入されると考えてよい。
- {関数 | 定理}のプロファイルの{コドメイン | 結論}は：
- {戻り値 | 結論トークン}がひとつなら、戻り値変数は不要。だが、有ってもよい。
- {戻り値 | 結論トークン}が複数なら、戻り値変数は必要。
- 戻り値変数名は番号でもよい。
- 番号である戻り値変数名は省略しても自動挿入されると考えてよい。
- {関数 | 定理}は、一般には{多引数 | 多仮定}・{多戻り値 | 多結論}だが、{戻り値 | 結論}はひとつの場合が多い。人間は、一度に複数の{戻り値 | 結論}を扱うことは不得意。
例題
「関数を定義〈記述 | 作成〉せよ」と「定理を証明〈記述 | 作成〉せよ」は同じタイプの問題。次の関数〈定理〉を例題として考える。
- 実数の二乗は正
- 偶数の和は偶数
- 一次方程式の解
- 因数分解された二次方程式の解
- 奇数の和は偶数
以上の日本語をそのまま関数名〈定理名〉に使う。関数〈定理〉のプロファイルは：
- 区切り記号矢印は、通常の矢印。
- 複数の引数、複数の戻り値はカンマで区切り、$`\LL\;\LR`$ で囲む。が、リスト囲みカッコはしばしば省略される。
- ひとつの引数選言は $`(x:X)`$ または $`(x\in X)`$ または $`(X \num{x})`$ 。囲み丸括弧はしばしば省略される。
- 複数の宣言をまとめて書いてよい、 $`(x, y, z\in X)`$ のように。
- 暗黙の引数〈仮定〉達を $`\Gamma`$ で表す。$`\Gamma`$ は計算の環境（大域変数やロードされたライブラリ）に相当。
関数〈定理〉のプロファイルは以下のとおり。
$`\T{実数の二乗は正} :\;
\Gamma \cdot (x\in {\bf R}) \to (x^2 \ge 0)\\
\T{偶数の和は偶数} :\;
\Gamma \to \forall n, m\in {\bf N}.( \mrm{even}(n) \land \mrm{even}(m) \Imp \mrm{even}(n + m))\\
\T{一次方程式の解} :\\
\quad \Gamma \odot \LL (a, b, x:{\bf R}), (a\ne 0 \num{1}), (ax + b = 0 \num{2})\LR \to (x = -\frac{b}{a})\\
\T{因数分解された二次方程式の解} :\\
\quad \Gamma \odot \LL (a, b, x \in {\bf R}), ( \alpha: (x - a)(x - b) = 0 )\LR \to (x = a \lor x = b)\\
\T{奇数の和は偶数} : \\
\quad \Gamma \odot \LL (n : {\bf N}), (m : {\bf N}), (\alpha : \mrm{odd}(n)), (\beta : \mrm{odd}(m))\LR \\
\qquad \to (\gamma : \mrm{even}(n + m) )
`$
問題： 上記のプロファイルを持つ関数〈定理〉を記述せよ。記述のボディ〈狭義の証明〉を書く。そのとき、組み込み関数〈公理〉や定義済み関数〈既存定理〉を使ってよい。関数・計算〈定理・証明〉の変形操作・組み合わせ操作〈リーズニング〉を使ってもよい。
次は使ってよい。
- すべての実数は、非負または非正
- 二つの非負実数の積は非負
- 非負実数の反数は非正
- 偶数の定義
- 計算と、分配法則などの計算法則
注意事項とコツ
- 定理〈関数〉の有名さ〈知名度〉、重要さ、名前が文字列か番号か？ などは気にしない。
- 略記、省略にイチイチ反応しないで、柔軟に対処。
- 定理の名前として、結論命題やその要約が使われることがある。これで、定理〈関数〉を命題〈型〉と思ってしまうかもしれないが、ここので定理は命題ではない。名前と証明が付いた命題が定理。
- 注意： ここでの用語選択基準は、カリー／ハワード／ランベック対応がスムーズに語れること。
- 図のノード形状、マーカー、ラベリングなどの描画方式は常にローカルな約束。その場その場の都合で決める。
- 型〈命題〉はワイヤーのラベルだが、最初は枠で囲むのがよい。慣れれば囲みは不要。
- 関数〈定理〉ノードは横棒や黒丸で描く。
- 組み込み関数〈公理〉、組み込み多相関数〈証明規則〉も関数ノード。
- 関数〈定理〉と関数のドメイン〈結論命題〉は別物だが、言葉では区別しにくいので注意。定理・証明のプロファイルを常に書くようにすれば大丈夫だろう。
- メモ書きでは、$`\land`$ の代わりにカンマでもよい。
- メモ書きでは、束縛変数の型宣言は省略してもよい。
- 公理や暗黙の仮定にある定理は、いきなり出現するノードとして描く。
- univ-to-exam と mp は多用するので、素早く描ける工夫をしたほうがいいかも知れない。
- 定義による置き換えや、論理的同値による置き換えは当然に使う。
- 変数への代入も当然に使う。
- 結合〈composition〉とテンソル積〈{tensor}? product〉のリーズニングは明示的に書く必要はない。導出ツリー〈リーズニングツリー〉では書くけれど。
- CURRYでベンドする〈曲げる〉予定の仮定はそれとわかるようにマークしておく。
- 計算図〈証明図〉が描き終わったら、別な色で、ワイヤーとノードを描画してトポロジーを確認する。特に、リーフ（ポートまたはノード）を確認する。
役に立つテンプレート
バックワード・リーズニングは、先に使うテンプレートを決めることだと解釈できる。
- ANDテンプレート： 連言命題が欲しいとき。直積コドメイン、デカルトペア。
- CASEテンプレート： 宣言命題を処理したいとき。直和ドメイン、デカルトコペア。
- CURRYテンプレート： 含意命題が欲しいとき。指数コドメイン、カリー化。
- FORテンプレート： 全称命題が欲しいとき。パイ型コドメイン。依存カリー化。
- EX-USEテンプレート： 存在命題を処理したいとき。シグマ型ドメイン。依存カリー化の双対。
- law-apply証明規則 ： 既存のパックされた法則〈定理〉をモダスポネンスと共に使いたいとき。評価関数。
法則〈定理〉は、プロファイルが次の形になるようにパックすることが多い。仮定〈ドメイン〉は空だが、暗黙の前提はあるだろう。
$`\quad a: \LL\LR \to \forall x\in X.(P(x) \Imp Q(x))`$
暗黙の前提と定理〈関数〉のボディも書くと：
$`\quad a: \Gamma \to \forall x\in X.(P(x) \Imp Q(x))\\
\quad a := \lambda\, \Gamma.(\cdots \text{証明項または証明図} \cdots)
`$
キーワードを使ってそれらしく書けば：
$`\T{theorem } a: \Gamma \to \forall x\in X.(P(x) \Imp Q(x))\\
\T{begin}\\
\quad \cdots \text{証明項または証明図} \cdots\\
\T{end}
`$
名前が無いなら：
$`\T{proof } : \Gamma \to \forall x\in X.(P(x) \Imp Q(x))\\
\T{begin}\\
\quad \cdots \text{証明項または証明図} \cdots\\
\T{end}
`$
ヘッド（プロファイル | ステートメント）を省略するなら：
$`\T{proof } \T{begin}\\
\quad \cdots \text{証明項または証明図} \cdots\\
\T{end}
`$
