※ この記事はエイプリルフールとは無関係ですよ。
3月19日にやったセミナー、それとシリーズ3回全体を総括しなきゃ、とか思っている間に4月になってしまいました。「次はどうしようか？」とかもいずれ書くつもりですが、今日は、superstring04さんが、Kuwataさんとは別な雰囲気のまとめを書いてくれたので、それに応答します。
superstring04さん曰く：
「お絵描き分」高めで。
ということで、実際の絵がたくさん入ってます。テキストエディタで書くと証明図にならざるを得ませんが、紙と鉛筆を使うなら絵のほうが断然お奨めです。ワイヤーとオダンゴ（または箱）を実際につなげると、証明図では見えなかった事情も分かるようになります。例えば、A⊃B, B⊃C |- A⊃C とか A⊃C, A⊃B |- A⊃(B∧C) とかを絵で描いて、ヒモ（ワイヤー）を引っ張ったりずらしたりすると面白いですよ。
superstring04さんの絵を引用して、A⊃B と ¬A∨B の関係の話でもしようかと思いましたが、今日は止めときます。
superstring04さん曰く：
これが檜山さんの言うところのオダンゴ図
オダンゴの代わりに箱を描けばボックス＆ワイヤー図（boxes and wires diagram）です。僕が採用しているのは、ジョン・バエズ（John Baez）の描き方、オダンゴを小さくした図はストリング図と呼びます。
superstring04さん曰く：
ｆ＾はｘを引数として、得体の知れないものを返している。この得体の知れないものがλｙ．（２ｘ＋ｙ）に対応する。
ｆ＾＾は引数を取らず、しこたま得体の知れない λｘ．λｙ．(２ｘ＋ｙ) というものを返す関数、とわかる。
「得体の知れないナニカ」という認識はまったく正しいです。ラムダ式（小さなラムダ式）の実体が何であるかを詮索しても不毛なんです。Eと書かれたevalとかapplyと呼ばれる関数（高階関数）との関係性において初めてλが意味を持つわけで、基本等式が成立するなら、f^自体は紙のカードでもビット列でも記号でも空き缶でも何でもいいのです。
superstring04さん曰く：
オダンゴ図にタプルを導入しよう。
タプル構成（小さな赤い器具）と関数型の留め金（短い矢印）が分かりやすいです。タプル型も関数型も、2本のワイヤーを束ねてリボンを作る操作です。しかし、タプル（論理なら連言）と関数型（論理なら含意）は別な種類のリボンなので、なにか区別する必要があります。絵算の観点からは、A⊃B のリボンを180度ひねったリボンを B⊂A と書きたいのですが、集合の包含と紛らわしいのが難。A->B と B<-A ならいいかも。よく知られた論理では、A->B と B<-A を区別する必要はありませんが、A->B と B<-A を同一視できない論理もあります。
僕は、A->B と B<-A をいつでも（同一視できる場合でも）区別して、ひねり（half twist）も明示的に描いたほうがいいと思います。ひねりが入った圏はリボン圏*1と呼びます。ヒネリを推論規則にすると次のようになります。（含意を -> と <- で書きます。）
A->B
------[HalfTwist-1]
B<-AA<-B
------[HalfTwist-2]
B->A
A->B, A |- B が元祖MP（モダスポネンス）とするなら、変形版 A, B<-A |- B は次のように導かれます。
B<-A
--------[HT-2]
A A->B
-----------[Exch]
A->B A
----------[MP]
B
絵との対応では、B<-A, A |- B 、A, A->B |- B が自然です。
最後の図（下に引用）、これは、僕が「オダンゴ図と証明図を横に並べて描くとわかりやすいですよ」と言ったことを実行してくれたものです。
左の図から、ラムダ式 λx.λy.f・(x, y) を読み取るのは容易ですよね。そのとき x, y, f の型はそれぞれ：
- x:A
- y:B
- f:(A,B)->C
であることもわかります。x, yをラムダ抽象すれば、それらは自由変数ではなくなり、fだけが自由変数で残ります。λx.λy.f・(x, y) 全体は、((A,B)->C) という関数型のデータfから (A->(B->C)) という関数型のデータを作る操作を表しています。このことを反映して、右側は、((A∧B)⊃C) という論理式を仮定して (A⊃(B⊃C)) という論理式を証明する証明図になっています。fもラムダ抽象してしまえば、論理側では、((A∧B)⊃C)⊃(A⊃(B⊃C)) の仮定なしの証明が得られます。
めでたいですね :-)
