非形式的な説明：証明と主張
以下の文章（引用ではない）内の「証明」「主張」は専門用語ではない。非形式的に使用している言葉。主張は assertion, declaration, claim, statement, judgement, thesis など。
証明とは、主張の正しさを保証するものである。その主張に至る過程も含めて、主張の根拠を提示しない限りは、正しい主張として受け入れることはできない。
主張の正しさの保証・根拠で重要なのはその過程であり、過程が正しくないなら、保証・根拠にはならない。もちろん、出発点となる主張の正しさも必要である。
肝は主張の定式化だろう。主張＝命題 となりがちだし、それは当然だが、うまくない。
| 非形式的 | 絵図 | テキスト | テキストの形 |
|---|---|---|---|
| 主張の要旨 | ストリング図のプロファイル | シーケント | Γ→Δ |
| 説明付きの主張 | ストリング図 | リッチシーケント | Γ-(F)→Δ |
| 主張が形成される過程 | ムービーフィルム | リーズニング図 | 横棒記法の図 |
| 前もって正しい主張 | 基本スパイダー | 名前付きシーケント | Γ-(f)→Δ |
過程は二重線横棒記法で書くことにする。過程を構成する素過程〈{基本 | アトミック | プリミティブ}過程〉は三種に分類される。
- put モノを置く
- combine モノ達を組む
- replace モノを別なモノで{置き}?換える（「変える」は使わない）
これらの素過程を実行するには、
- 事前に、置いてよいモノが決まっている。（組み込み基本スパイダー）
- 事前に、組み方（操作法）が決まっている。（ストリング図コンビネータ）
- 事前に、置き換えてよい代替物〈alternative | replacement〉が決まっている。（ストリング図同値関係の集まり）
言葉としては「組む」と「置き換える」の区別が微妙だが、実際は：
- 「組む」ときは、組むためのコンビネータが存在している。
- 「置き換える」ためには、同値関係が存在している。
コンビネータと同値関係の“関係”は：
- 同値関係は可逆コンビネータを生成する。
- コンビネータはプロファイルを変えてよいが、同値置き換えではプロファイルを変えない。
- プロファイルを変えない可逆コンビネータは同値関係と同じもの。あるいは、同値関係を生成する。
- 変形同値〈deformation equivalence〉で、まとめて扱うことが出来る。
過程〈プロセス〉の例：
何もない 何もない
===========[2を置く] ===========[3を置く]
2 3
===========|============[一緒にする]
2 3
=======[足し算で組む]
2+3
=======[同じ値で置き換える]
5繰り返し言うと：
- 置く、「置」
- 組む、「組」
- 換える、「換」 （換はswap, permutation, transposeの意味もあるが）
置いてよいモノ（組み込み基本スパイダー）と組み方（組み込み基本コンビネータ）のリスト〈一覧表〉は別エントリーにする。→証明と主張： 一覧表 - 檜山正幸のキマイラ飼育記 メモ編
