面積問題への対策（あるいは無策） (A21)

昨日、Lambda基本リーズニング（「含意導入規則」と呼ばれることが多い）に関して、ワイヤーベンディング描画法を説明しました。描画法を考えた当事者の意図・目的を理解しないと、「変な絵」「ワケワカメな図」になってしまいます。

描画法／記号法／表記法を考えた当事者の意図・目的で、けっこう多いのが「面積問題への対策」です。面積とは、紙面・画面の広さのことだと思ってください。グラフィカルなフル・リーズニング図は、とてもとても面積を消費するので、そのままでは描けません。そこで、より少ない面積で描ける描画法／記号法／表記法が開発されたのです。

紙のページの場合、巨大な絵の印刷は物理的に無理で、縮小すると読めなくなります。コンピュータ画面なら、スクロールやズーミング、折りたたみ／展開などにより事情は改善します。さらにアニメーションがあれば、劇的な効果があるはずです。

が、実情はツールが整備されてません。

• アニメーションとしての証明

フレーゲ（『概念記法』が1879年）に始まり、ゲンツェンのイノベーションを経た現在の論理は、よく整備されたきれいな体系になっています。にもかかわらず、適切な伝達手段（メディアとツール）がありません。貧弱な伝達手段とお粗末な手法により伝達される結果として、グチャグチャで汚い体系として受け止められる可能性があります。音響カプラを経由してYouTube動画を観ると、たぶん酷い映像になるでしょう。それと同じです（って、同じじゃない）。

悲しいかな、効果的な対策はなく、現時点で出来ることは、伝達する側も受け取る側も“根性を出す”ことだけです。手間を厭わず、広い面積の絵を何枚も提示する、自分で描いてみることです。

檜山は根性を出したくないし、根性に自信もないので、極端な面積節約は控えても、やはり手間は節約したい。

• 「アニメーションとしての証明」で言う「パラパラ漫画」方式、「紙芝居」方式で書く。
• 絵が少なめな「紙芝居」になるかも知れないが、「小説」方式（テキストのみ）にならないようには気をつける。
• 絵は、ノートに乱雑に手描きしたものをスキャンして使う。汚いけどカンベンしてね。

お約束

推論図を「全部乗せ」で描くときは、

推論図の名前またはテキストによる式 : プロファイル
（プロファイルはシーケント形式で書く）

  ここにグラフィカルな推論図
  （スパイダー＝ノード・ワイヤー図）

これは「全部乗せ」なので、名前、テキスト式、プロファイルは省略されるかも知れません。また、本体である推論図が省略されることもあります。要するに、どれも省略される可能性を持ちます。

多くの人は、一番面積をとる推論図本体を省略したがります。檜山は、他を省略しても出来るだけ本体は省略したくないと思っています。（あくまで「出来るだけ」ね。）

横棒記法に関しては：

• 原則として、推論の横棒は一本棒（'---'）、リーズニングの横棒は二本棒（'==='）。
• 両方一度に使わないときは、リーズニングでも一本棒（'---'）を使うときがある。
• 推論／リーズニングを表すラベルは、横棒の右側。ラベルも出来るだけ省略しない。（あくまで「出来るだけ」ね。）

手描きのときに一番多く使いそうな描画法は、

• 推論図はグラフィカルに（スパイダー＝ノード・ワイヤー図）として描く。
• リーズニングは横棒記法（一本棒または二本棒）として書く。

例えば（ほんとに汚えー）：

プロファイルだけ抜き出して書けば：

  B, A → A, B   C → C
 ======================= Prod
  B, A, C → A, B, C           A, B, C → D
 ============================================ Comp
      B, A, C → D
    ================= Lamb
      A, C → B⇒D