基本的な事項:
- 証明は、上下にポート(境界上のドットか、どこにも繋がってない短いワイヤーで描く)を持つボックスである。
- 証明には、順行〈forward〉と逆行〈backward〉がある。しばしば、証明の順逆〈forward or backward〉をワイヤーの向きで描くが、誤解を招くし、誤解している人も多い。ワイヤーには向きを付けず、ポート極性で表すほうがいいだろう。
- ひとつのボックスに順行と逆行が混じったボックスもあるが、最初は考えないほうが混乱が少ない。
- 順行証明の上側ポートを前提、下側ポートを結論と呼ぶ。
- 逆行証明の上側ポートをゴール、下側ポートをサブゴールと呼ぶ。用語に統一性や対称性がまったくないが、そういうことは多いのでイチイチ気にしないで受け入れる。
- 前提には暗黙の前提と明示的前提がある。暗黙の〈背景の | 共通の | 基礎の〉前提は通常描かない。
- サブゴールには暗黙のサブゴールと明示的サブゴールがある。暗黙の〈背景の | 共通の | 基礎の〉サブゴールは通常描かない。
- 暗黙の前提は、背景エリアから突如現れるワイヤーで描く。
- 暗黙のサブゴールは、背景エリアに溶けて失くなるワイヤーで描く。
既存のボックス達を加工したり組み合わせて新しいボックスを作る。ボックス自体を証明と呼んだので、ボックスに対する操作〈演算〉はリーズニングと呼ぶ。
リーズニング:
- 併置(テンソル積)
- 反転(ダガー演算)
- 直列ワイヤー結合(単に「結合」)
- ベンディングワイヤー結合
- ボクシング〈ドリルアップ〉
- アンボクシング〈ドリルダウン〉
- カリー化〈関数抽象〉
- And統合〈有限デカルト・タプリング〉
- Or分解〈有限デカルト・コタプリング〉
- Forall統合〈一般デカルト・タプリング〉
- Exists分解〈一般デカルト・コタプリング〉
キャンバスに描かれているストリング図がまさに証明そのもの。リーズニングは、証明をオペランドとするオペレーション〈コンビネータ〉である。リーズニングと証明が混乱している状況をよく見るが、ストリング図を描いてる限りそのような混乱が起きることは(ほぼ)ない。ただし、キャンバス/絵(モノ)と絵を描く・作る制作行為・行動を区別できない人は混乱の可能性がある。モノと行為を区別できない人は、今更でも区別するトレーニングしよう。
素材(ワイヤーとボックス)と道具(リーズニング)一式が入った集合を「ツールボックス」とか呼ぶと「ボックス」被りでまた混乱するから、ツールバッグ〈tool bag〉と呼んでおこう。ツールバッグは、ソフトウェアで言えばライブラリーモジュール。
製品: ツールバック 折りたたみ https://www.monotaro.com/p/3262/1626/
画像: https://jp.images-monotaro.com/Monotaro3/pi/full/mono32621626-210423-02.jpg(拡張子は.jpgだが、実際はwebp画像)
証明の構成過程〈construction process〉は:
- 描画ツールバッグのなかに、使っていい素材/道具/キャンバスなどが入っている。
- 白紙のキャンバスを準備する。
- ツールバッグのなかの素材と道具を使ってストリング図を描く。
- 出来た絵をボクシングして、ボックスとしてツールバッグにしまってよい。後で使える。
- 道具を組み合わせて新しい道具を作ってもよい(リーズニングのプログラミング)。
- 出来た道具は、ツールバッグにしまってよい。後で使える。
- そういう作業を繰り返して目的のストリング図を描く。
- すべての作業工程の記録は動画、あるいはアニメーションとして残すのが良いのだが、現時点ではテキスト記述しか使えないから無理(泣)。
アニメーションが使えないからパラパラ漫画〈紙芝居〉方式で描いた絵:
もし、証明の構成過程がグラフィックスとアニメーションとして記録できるなら、学習や教育はとんでもなく加速するだろうに ‥‥‥ そのような方向での進化が遅い、遅過ぎる! つうか進化してない!!(ひたすら泣く)