檜山正幸のキマイラ飼育記 メモ編 このページをアンテナに追加 RSSフィード

この「はてなダイアリー」は、
2019年1月18日の記事を最後に更新を停止します。
しかし、
「檜山正幸のキマイラ飼育記 メモ編」は保存され、新規ブログに移行します。
新しい「檜山正幸のキマイラ飼育記」と関連ブログについては、
こちらの記事 をごらんください。
連絡は hiyama{at}chimaira{dot}org へ。

2019-01-22(火)

ブログ移転のお知らせ

18:50 |

この「はてなダイアリー」は、2019年1月18日の記事を最後に更新を停止します。しかし、「檜山正幸のキマイラ飼育記 メモ編」は保存され、新規ブログに移行します。

新しい「檜山正幸のキマイラ飼育記」と関連ブログについては、こちらの記事 をごらんください。

連絡は hiyama{at}chimaira{dot}org へ。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20190122

2019-01-18(金)

メイヤー系とコ/モナド

| 14:23 |

記法:

  • コ/モナドモナドまたはコモナド
  • A : 上付きのチェックマーク(のつもり)は、文字修飾子。使い途はボールドなどと同じ。Aに対する演算子ではない。モナドを表す文字・語への文字修飾に使う。

ベックの分配系は4種類あって、

  1. モナドモナド分配系 (M, A, δ)
  2. モナド・コモナド分配系 (M, A, δ)
  3. モナドモナド分配系 (M, A, δ)
  4. モナド・コモナド分配系 (M, A, δ)

3,4番の分配系を混合分配系と呼ぶ。1,2番は非混合分配系〈unmixed distributive system〉。

分配系の一番目の構成素(コ/モナド)に対して、そのアイレンベルク/ムーア圏を作る。二番目の構成素(コ/モナド)は、そのアイレンベルク/ムーア圏上のコ/モナドに持ち上がる。Yを二番目のコ/モナドとして、持ち上げをY↑δと書く。Y↑δに対して再びアイレンベルク/ムーア圏を作る。

以上の手順で出来た圏を分配系のアイレンベルク/ムーア圏とする。

非混合分配系の場合は複合コ/モナドが作れて、それのアイレンベルク/ムーア圏を作ればいいが、混合分配系の場合は複合系が作れない! 上記の持ち上げ方式だと、混合系を経由しないでアイレンベルク/ムーア構成ができる。

  • ベック分配系(4種類) --(アイレンベルク/ムーア構成)→ アイレンベルク/ムーア圏

複合系が要らないので、自由にアイレンベルク/ムーア構成ができて、第一コ/モナドと第二コ/モナドの区別もシッカリできる。複合系を一般化してもアイレンベルク/ムーア構成は出来るかも知れない。

コマンド・クエリー分離されたメイヤー系は、コマンド・モナドのスタンピングによるモナドと、値の余代数スタンピングによるコマンドが作る、モナド・コモナド分配系になる。よって、そのアイレンベルク/ムーア圏が作れる。アイレンベルク/ムーア圏の対象は、モノイドが作用する状態空間(ラベル付き遷移系)に、クエリー構造を付けたもの。クエリー構造がコモナドの余代数であることから、副作用なし(余単位律)と内部生(余結合律)が出てくる。

メイヤー分配系の単一複合系は作れないので、持ち上げによって階層的に(繰り返しにより)定義するしかない。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20190118

2019-01-17(木)

律子と制約と一貫性

| 13:31 |

「一貫性」という言葉が曖昧だから整理する。

まず、律子〈rator〉は法則を与える2-射(あるいはもっと高次の射)のこと。律子が満たす等式を制約等式〈constraint equation〉または等式的制約〈equational constraint〉または単に制約〈constraint〉と呼ぶ。ここまでは特に「一貫性」という言葉は出てこない。

が、制約を一貫性制約と呼ぶことがある。ちょっと違うような気がする。一貫性は、「律子+制約」がある状況で、律子達で作った自由圏がやせていることだろう。つまり、一貫性、あるいは「一貫性がある/を持つ」のような言い方は、「律子+制約」が作る構造に対する形容詞なのだと思う。

よって、一貫性制約の意味は、「一貫性を持つ『律子+制約』の制約」だろう。一貫性を持つようにうまく定義されている制約、という感じか。

一貫性定理は、特定の「律子+制約」構造が実際に一貫性を持つことを主張する定理。

一貫性法則〈coherence law〉が一番意味不明で、制約等式のことか、一貫性定理のことか不明。

形式/非形式とレイヤー構成

| 14:46 |

大分類 非形式 形式化データ 備考
計算 対象式 対象式(項) もともと形式化されている
論理 命題 論理式 文字列または構文解析木
論理 推論 推論図 仮定と結論がある
論理 リーズニング リーズニング図 ツリー状ノード・ワイヤー図

すべての形式化データは、ノード・ワイヤー図で表現される。推論図は2次元的な構造を持ち、その構文解析木がリーズニング図(の木)で与えられる。レイヤーは多いが、やってることは同じことの繰り返し。

すべてのデータはグラフ/ツリーなので、グラフ/ツリー処理言語があれば操作可能。実質的にツリーだと思ってよいので、ツリー処理言語。ツリー処理言語を使った計算をツリー算術と呼ぶ。

ツリー算術は計算レイヤーに落ちるので、レイフィケーション構造を作れる。レイフィケーション構造=ゲーデル構造。プログラミング的に言うと、レイフィケーション構造はリフレクションライブラリ/メタプログラミングライブラリ/メタオブジェクト・プロトコール。

シーケントの役割、使い所

| 14:50 |

形式/非形式とレイヤー構成 - 檜山正幸のキマイラ飼育記 メモ編にシーケントが出てこないが、シーケントは構文形式なので、幾つかの使い途がある。

  1. 基本推論図は、ひとつのシーケントで表現可能で、基本推論図とそのシーケントは同一視してもよい。
  2. 一般の推論図のプロファイルはシーケントで表現できる。
  3. 省略したリーズニング図は、シーケントと基本リーズニング図で出来ている。

2019-01-11(金)

随伴の方向の事例

| 12:07 |

随伴に関する注意事項 - 檜山正幸のキマイラ飼育記 (はてなBlog)に関連して:

次の例は、http://www.math.uchicago.edu/~may/VIGRE/VIGRE2011/REUPapers/Berger.pdf から。ここ(以下のコピーのところ)で初めて記号'-|'が出てきている。

随伴系の方向はペアの右の関手に合わせている(しばらく考えると分かる)。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20190111

2019-01-10(木)

問題集11「小学生でも…」の解答と補足説明 (A23R11)

| 13:46 |

※この記事は「記事23 問題集11の解答」

問題集11とは、次の記事(の問題部分)のことです:

上記記事への追記で次の文言を入れました。

「全部乗せで、完全にグラフィカルなリーズニング図」を描くのはムチャクチャ大変だわー。ゴメン、そこまでやんなくていいわ。真面目にやると、どの程度の労力と面積が必要かの見当がついたら、あとはテキトーに手を抜いていいです。

やっぱり、ガッツリ完全に描画はシンドすぎる。このシンドさを実感すれば、どうして省略記法しか使われないか、の理由も明らかでしょう。

内容:

  1. ゲンツェンのLKシーケント計算をご存知の方への注意
  2. とりあえず描くぞ
  3. プロファイルを調べてみると
  4. 連言命題を構成する/連言命題を分解する基本推論

ゲンツェンのLKシーケント計算をご存知の方への注意

検索などでたまたまここに辿り着いた人が誤解するのも困るので、毎回この節を挿入することにします。

  1. '⇒'は含意〈条件法〉の論理結合子で、'→'がシーケントの左右を区切る記号である。
  2. ゲンツェンのLKシーケントでは、左辺のカンマは連言的に、右辺のカンマは選言的に解釈をする。ここでのシーケントでは、出現位置の情報を使わずに、カンマは常に連言的であり、選言的な区切り記号に縦棒'|'を使う。
  3. (x∈R, n∈N) のような書き方は、集合論の命題ではなくて、自由変数の型宣言(のリスト)である。自由変数の型宣言のリストをコンテキストと呼ぶ。
  4. 暗黙のコンテキストを使う場合もあるが、できるだけ、シーケント内に明示的にコンテキストを書き込むようにしている。
  5. NK/NJの証明図を推論図、LK/LJの証明図をリーズニング図と呼んで区別している。両方を同時に使うことがある。推論規則は、基本推論/基本リーズニングと呼ぶ。
  6. LK/LJのように、公理(基本推論)がひとつではなくて、けっこうたくさんの公理がある。その代わり、推論規則(基本リーズニング)の数を減らすようにしている。

とりあえず描くぞ

全体を一度には描けない(面積の関係で)ので、いくつかの部分に分けます。描き方は、「面積問題への対策(あるいは無策) (A21) // お約束」に従います。が、全部乗せしません。

この図1を、テキストの式とプロファイルで書くと:

                ☆
            ---------- Ent
 f:A,B→C   dup:C→C,C                                 ☆
 ---------------------- Comp                      ------------- Ent
   f;dup:A,B→C,C          g:C,C→D      h:A→C,D  swap:C,D→D,C
 ---------------------------------- Comp ------------------------ Comp
           f;dup;g:A,B→D                  h;swap:A→D,C
          ------------------------------------------------ Prod
          (f;dup;g)¥otimes(h;swap):A,B,A→D,D,C

これも、グラフィカルな図と同じ情報を持ちます。欠点は、テキストの式だと2次元の構造が見えなくなることです。リーズニング名の代わりに演算子記号を使うのもいいかも知れません(Entは省略)。

                ☆
            ----------
 f:A,B→C   dup:C→C,C                                 ☆
 ---------------------- ;                          -------------
   f;dup:A,B→C,C          g:C,C→D      h:A→C,D  swap:C,D→D,C
 ---------------------------------- ;    ------------------------ ;
           f;dup;g:A,B→D                  h;swap:A→D,C
          ------------------------------------------------ ¥otimes
          (f;dup;g)¥otimes(h;swap):A,B,A→D,D,C

マイク・シュルマン〈Mike/Michael Shulman〉はこれと同じ描画法を使ってます*1。ただし、左右は逆です(その他、細かい違いはあります)。

話を戻して、図1のプロファイルだけなら:

            ☆
          ------- Ent
  A,B→C   C→C,C                                 ☆
 ----------------- Comp                       ---------- Ent
     A,B→C,C           C,C→D        A→C,D   C,D→D,C
    --------------------------- Comp  ------------------ Comp
            A,B→D                      A→D,C
          -------------------------------------- Prod
                      A,B,A→D,D,C

次に、図1を一部に埋め込んだ図2。図1をはめ込む部分が目立ち過ぎだわ。斜線とピンクでキタネー。

図2のプロファイルだけ:

                  ☆          ☆
 〜〜〜         ------- Ent ------ Ent
  図1           D,D→D       C→C
 〜〜〜         ------------------ Prod
 A,B,A→D,D,C       D,D,C→D,C
 ------------------------------- Comp
         A,B,A→D,C

ここまでで、もとの絵の左側ができました。念の為、もとの絵を再掲。

次は、右側のほうを作っていきます。アレッ、図3で、C, Dのスワップとiのラベルが間違ってる、直さん(描き直すの面倒だから)。

プロファイルだけなら(間違いは修正):

   ☆
 --------- Ent
  C,D→D,C    D,C→A
 -------------------- Comp
       C,D→A
      --------- Lamb
       D→C⇒A

これで、絵の左側と右側が出来たので、Sumリーズニングで選言的に併置します。あのさー、ピンクの塊が目立ち過ぎなんだけど、、、なんでこんな描き方しちゃったかなー (後悔)。

以上で、絵の構成過程であるリーズニング図が出来上がりです。注釈の区切り線や囲み線が描いてあれば、最後の絵からリーズニング図を(ほぼ)一意的に再現できます。

これは、括弧付けをきちんとした式から構文解析木が一意的に構成できることと同じです。構文解析木については「整数式の構文解析木 (A4P3)」に解説と練習問題があります。ちなみに、今回の絵の“括弧付けをきちんとした式”は:

  • ( ( ((f;dupC);g)¥otimes(h;swapC,D) );(codupD¥otimesidC) ) ¥oplus ( Λ(swapC,D;i) )

この式の構文解析木がリーズニング図なわけです。

プロファイルを調べてみると

プロファイルだけなら一枚の絵に書けるかな? できるだけ圧縮するため、Ent, Prod, Comp, Lamb を、E, P, C, L の一文字にして、空白も空けないで詰めます。

         ☆
       ------E
A,B→C C→C,C                  ☆
-------------C               -------E
 A,B→C,C     C,C→D  A→C,D C,D→D,C    ☆     ☆      ☆
 -------------------C ---------------C ------E ----E --------E
       A,B→D           A→D,C         D,D→D  C→C  C,D→D,C D,C→A
       -------------------------P      ------------P ---------------C
                      A,B,A→D,D,C     D,D,C→D,C       C,D→A
                      ---------------------------C      -------L
                             A,B,A→D,C                 D→C⇒A

これ、最下段を書いてません。最下段まで描くと、次のようになっちゃうのです。

   :::          :::
   :::          :::
 ------------    ---------
  A,B,A→D,C      D→C⇒A
 ----------------------------- Sum
      A,B,A | D → D,C | C⇒A

最下段の推論図(=もとの推論図)のプロファイルに、カンマと縦棒の入れ子ができちゃうのです。括弧で包んでみると:

  • ((A,B,A) | D) → ((D,C) | C⇒A)

こういう入れ子が、絶対にダメってわけじゃないのですが、リーズニングの計算を(極度に)複雑にしてしまうために禁止してます。もともと、推論図からリーズニング図に移行した動機が「計算が簡単になるから」*2なので、計算が複雑になる要因を許すと元も子もないのですわ。

対策として、図2のところを次の図2'のように修正します。

これは何をやっているのかと言うと; もとの図の左側のプロファイルが A,B,A → D,C だったのを、論理式のリストを単一論理式にしてしまうのです。

  • 連言的リスト A,B,A を、単一論理式 A∧B∧C にする。
  • 連言的リスト D,C を、単一論理式 D∧C にする。
  • すると、A∧B∧A → D∧C というプロファイルの推論図になる。

ゲンツェンの(オリジナルの)システムだと、基本リーズニングが20個以上あり、こういうことを一発で出来る基本リーズニングも最初から備えているのだけど、基本リーズニングを6個に減らしてしまったので、次のような手順が必要です。

 (A∧B)∧A→A,B,A  A,B,A → D,C        ☆
 -------------------------------C  ---------E
           (A∧B)∧A→D,C          D,C→D∧C
           ---------------------------------C
                   (A∧B)∧A→D∧C

このリーズニング図(のプロファイルのみ略記)の最上段左の (A∧B)∧A→A,B,A は、基本推論ではないので、これも次のようにして作る必要があります。

                             ☆         ☆
                         -----------E  ----E
         ☆              A∧B → A, B  A→A
 --------------------E  --------------------P
 (A∧B)∧A → A∧B, A   A∧B, A → A, B, A
 ------------------------------------------C
         (A∧B)∧A → A, B, A

基本リーズニングがたった6個じゃ不便だろう? って。いやっ、全然平気。マクロ・リーズニング(ユーザー定義のリーズニング)やマクロ推論(ユーザー定義の推論)をどんどん足していけば、システムの能力はいくらでも上がります。小さなコアのプログラミング言語でも、ライブラリで能力を足せるのと同じです。

僕が基本リーズニングを減らしている(代わりに基本推論がけっこう多い)のは、カリー/ハワード対応と圏論的意味論の観点を重視してるからで、趣味の問題とも言えます。

連言命題を構成する/連言命題を分解する基本推論

前節で、A, B → A∧B と A∧B → A, B というプロファイルの基本推論が出てきました。これはγ〈小文字ガンマ〉という名前で呼びたいと思います。

  • γA,B:A, B → A∧B
  • γA,B-1:A∧B → A, B

γA,Bとその逆であるγA,B-1は頻繁に登場するので、描画時に名前ラベルを使わないで、アイコン〈シルシモノ | マーカー〉を使います。γA,Bは、次のどちらか、

γA,B-1は次のどちらかで描くことにします。

これらの推論(図)は、もちろん最初からシステムに備わる基本推論です。

*1https://mikeshulman.github.io/catlog/catlog.pdf の p.40(ノンブル〈表示のページ番号〉は37)

*2:圏論の言葉を使うと、推論図からリーズニング図への以降は、モノイド圏の厳密化〈strictification〉をしていることです。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20190110

2019-01-09(水)

小学生でも分かる論理計算 (A22P11)

| 15:58 |

※この記事は「記事22 問題集11」

伝達側が、省略なしに描いた絵を提示する労(と面積)を厭わず、学習者も絵を描く練習をするなら、専門家にも難解と言われるゲンツェン流の論理計算も、
内容的には小学生レベル
だと思います。

このこと(「絵を使えば簡単だぞ!」)をもっと過激に指摘しているのはボブ・クック〈Bob Coecke〉です。クックによれば、量子力学も絵で教えれば
幼稚園児レベル
だそうです。

クック達(Oxford Quantum Group)は、絵で計算・証明を行うソフトウェア(QuantomaticとGlobular)を開発し公開してますが、それらの描画機能はイマイチで、絵は汎用お絵かきソフト(VisioとかBlender、TeXパッケージなど)で描いているようです。

量子テレポーテーションの絵:

*1

ロッカーでもあるクック先生の文言はけっこう“煽り”が入っているので、文字通りに「幼稚園児」は若干眉唾ですが、僕(檜山)が言っている「小学生」はたぶん可能だと思います。良いUIのソフトウェアがあれば、小学校低学年でも遊んでくれるでしょう。

*2

内容:

  1. ゲンツェンのLKシーケント計算をご存知の方への注意
  2. 基本リーズニングの概要
  3. 基本推論
  4. 基本リーズニングの絵
  5. 練習問題

ゲンツェンのLKシーケント計算をご存知の方への注意

検索などでたまたまここに辿り着いた人が誤解するのも困るので、毎回この節を挿入することにします。

  1. '⇒'は含意〈条件法〉の論理結合子で、'→'がシーケントの左右を区切る記号である。
  2. ゲンツェンのLKシーケントでは、左辺のカンマは連言的に、右辺のカンマは選言的に解釈をする。ここでのシーケントでは、出現位置の情報を使わずに、カンマは常に連言的であり、選言的な区切り記号に縦棒'|'を使う。
  3. (x∈R, n∈N) のような書き方は、集合論の命題ではなくて、自由変数の型宣言(のリスト)である。自由変数の型宣言のリストをコンテキストと呼ぶ。
  4. 暗黙のコンテキストを使う場合もあるが、できるだけ、シーケント内に明示的にコンテキストを書き込むようにしている。
  5. NK/NJの証明図を推論図、LK/LJの証明図をリーズニング図と呼んで区別している。両方を同時に使うことがある。推論規則は、基本推論/基本リーズニングと呼ぶ。
  6. LK/LJのように、公理(基本推論)がひとつではなくて、けっこうたくさんの公理がある。その代わり、推論規則(基本リーズニング)の数を減らすようにしている。

基本リーズニングの概要

口頭で「5種類」と言ったような気がしますが、基本リーズニング〈primitive reasoning〉(システムに組み込みのリーズニング)は6種類です。「縦/横」は描画方向↓→で描く場合のことです。

番号 名前 フルスペル 一言説明
1 Comp composition 結合、縦に繋げる
2 Prod product 論理積(連言)的な横併置
3 Sum sum 論理和(選言)的な横併置
4 Lamb lambda ラムダ抽象の論理版
5 Diam diamond ∀限量子に関わるリーズニング
6 Squa square ∃限量子に関わるリーズニング

Comp, Prod, Sum は2つの推論図から1つの推論図を作り出します。Lamb, Diam, Squa は1つの推論図から1つの推論図を作り出します。この他に、変数とコンテストを操作するリーズニングがあります(今回は触れない)。

リーズニングの働きに対応する演算子記号があります。lambda, diamond, squareは、演算子記号の形からの命名です。

番号 リーズニング名 演算子記号
1 Comp ;
2 Prod ¥otimes
3 Sum ¥oplus
4 Lamb Λ (大文字ラムダ)
5 Diam
6 Squa

このなかで、最初の4つ、Comp, Prod, Sum Lamb は、次の理由で扱いが容易です。

  1. 変数・コンテストに関する操作がない(変数・コンテストを考えなくてもいい)。
  2. リーズニング下段の図(出力側)から、リーズニング上段の図(入力側)を再現可能。

Diam, Squa は、次の理由で難しいです。

  1. 変数・コンテストに関する操作が伴う。
  2. リーズニング下段の図から、リーズニング上段の図を再現するのが困難(たいていは不可能)。

今回は、比較的に簡単な Comp, Prod, Sum Lamb だけを説明します。Lambに関しては、既に詳しく説明しています、「Lambdaリーズニングと演繹原理〈演繹定理〉 (A20)」参照。

基本推論

基本リーズニングは、与えられた推論図の組み合わせ・変形を行う操作です。素材となる推論図が(描画方向↓→なら)上段になります。では、最初の推論図はどこから持ってくるのでしょう? “最初から在る”とみなす推論(図)を、基本推論〈primitive inference〉とか組み込み推論〈builtin inference〉と呼びます。

シーケントとスコット・ブラケット (A10P8) // 組み込み推論を表すシーケント」に基本推論を列挙しています。

これらの基本推論には、名前が付いてます。歴史的な経緯から、ひとつの基本推論に幾つもの名前があります。例えば、プロファイルが A, A⇒B → B である基本推論は、「モーダスポネンス」、「三段論法(たぶん誤用)」、「eval(ラムダ計算から)」、「apply(ラムダ計算から)」、「ε(evalのeと、圏論の余単位から)」などと呼ばれます。

Xの恒等〈identity〉、Xの複製〈duplication〉、XとYの入れ替え〈swap〉などは、いちいち名前を書かないで、単なるワイヤー、ワイヤーの分岐、ワイヤーの交差で描きます。「スパイダーパズル (A17P10) // 汎用のスパイダー」参照。

基本リーズニングの絵

単一の命題は、A, B などのラテン文字で表します。命題のリスト(連言的リスト、または選言的リスト)は、Γ, Δ などのギリシャ文字で表します。リストの項目〈要素 | 成分〉が1個の場合は、単一の命題と同一視していいので、正確に言えば:

  • 単一の命題、または複数の項目を持つリストはギリシャ文字で表す。
  • ギリシャ文字であっても、単一の命題かも知れない。

リストを、絵では二重線や太い線で表す人もいますが、ここでは単一の命題とリストを特に区別しないで、実線ワイヤーで描きます。

補助線、あるいは注釈線を赤で描くことにします。注釈線は、通常は省略します。ただし、

  • Sumに対する注釈線(区切り線)がないと、ProdとSumの結果を区別できない。よって、Sumに対する注釈線、または注釈線に代わる何らかの目印が必要。
  • Comp, Prodの注釈線(区切り線)は、なくてもよいが、ないと一意的にリーズニング図を再現することは出来なくなる。一意性を気にしないなら省略可能。
  • Lambの注釈線(囲い)は、なくてもいい。

[追記]

完全に一意的な再現はやっぱり難しいなー。注釈の区切り線の長さを変えるとか、注釈として囲い枠を付けるとか、ゴチャゴチャと書き込めば一意的な再現が確かに可能ですが、そこまで注釈線を書き込むのが面倒過ぎる。

[/追記]

結合 Comp 基本リーズニング

上段の2つの推論図を縦に繋げます(あくまで、描画方向↓→での話)。左が上、右が下になります。繋いだ場所に、注釈の区切り線を横に入れます。

積 Prod 基本リーズニング

上段の2つの推論図を横に並べます。並べた中間に、注釈の区切り線を縦に入れます。

和 Sum 基本リーズニング

上段の2つの推論図を横に並べます。意味は、選言的な併置なので、積〈Prod〉とは違います。並べた中間に、注釈の区切り線を縦に実線で入れます。区切り線でなくても、積と区別するための何らかの目印が必須です。

ラムダ Lamb 基本リーズニング

Lambdaリーズニングと演繹原理〈演繹定理〉 (A20)」参照。囲いの注釈線はなくてもかまいません。とりあえず、曲げるワイヤーは一番左に限ることにします。こう制限しても、swapでワイヤーを入れ替えられるので心配は要りません。

練習問題

Comp, Prod, Sum, Lamb だけしか使ってないなら、最後の推論図(出来上がり)から、構成過程であるリーズニング図が再現できます。注釈線までちゃんと描いてあれば、一意的に再現できます。

[追記]

先の追記で書いた事情で、完全に一意的な再現は難しいですね。結合律 (f;g);h = f;(g;h) の左右の違いのような差は生まれますが、それは同一視するなら、まーまー一意的です。

[/追記]

問題1: 下の推論図に対して、その構成過程であるリーズニング図を描いてください。全部乗せで、完全にグラフィカルなリーズニング図です。「全部乗せ」とは、フレーム(四角い枠)内に次を書き込むことです。

  1. 推論の名前、またはテキストによる式(演算子記号を使う)
  2. 推論図のプロファイル(シーケントとして書く)
  3. グラフィカルな推論図

ワイヤーだけ、ワイヤーの分岐、ワイヤーの交差、ワイヤーの合流は次の記号で表します。

  1. idX
  2. dupX
  3. swapX, Y
  4. codupX (coは、sin, cos のcoと同じく、「相棒」を示す。)

[追記]

「全部乗せで、完全にグラフィカルなリーズニング図」を描くのはムチャクチャ大変だわー。ゴメン、そこまでやんなくていいわ。真面目にやると、どの程度の労力と面積が必要かの見当がついたら、あとはテキトーに手を抜いていいです。

それと、上の図をそのままリーズニング図にすると、論理計算〈シーケント計算〉としてはちょっと具合が悪い点もありますね。解答のときに補足します。→ 解答例と修正と解説は、「問題集11「小学生でも…」の解答と補足説明 (A23R11)

[/追記]

問題2: 完全なリーズニング図から、プロファイル(シーケント形式)だけを抜き出して、一本棒の横棒記法の図を作ってください。それが、論理の本でよくみる(例えば↓)シーケント証明図です。

*3

「ゲンツェン流のシーケント計算が分からない」理由(の多く)は、何をどう扱っているかを知らないままに省略記法だけを機械的にいじるハメになるからです。

2019-01-08(火)

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

| 15:39 |

昨日、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

2019-01-07(月)

Lambdaリーズニングと演繹原理〈演繹定理〉 (A20)

| 12:45 |

Lambdaリーズニングとは、'|'の形のワイヤーを'∩'の形にひん曲げる操作です。アンケートに「Lambdaリーズニングが分からない」とあったのですが、まー、分かりにくいでしょう。

「なんでワイヤーが曲がるのだろう?」と考えても、そりゃー分かりませんぜ。天然・自然に曲がるべき必然的理由があるとか、曲がる現象が観測できる、とかではありません*1。描画の約束事として、「ワイヤーを曲げて描こう」と人間(誰かさん)が決めたのです。なので、その約束の意図を理解する必要があります。問題は、「なぜ、あんな描き方がいいと思ったのか?」です。

内容:

  1. 演繹原理〈演繹定理〉
  2. フル・リーズニング図を描かないために
  3. ワイヤーベンディングと留め金
  4. ターンバックノードとワイヤーストレッチング

演繹原理〈演繹定理〉

演繹定理〈deduction theorem〉と呼ばれる原理があります。「定理」と呼ばれてはいますが、むしろ、演繹システムが必ず満たすべき性質、要請と捉えるべきでしょう。なので、ここでは演繹原理と呼ぶことにします(世間では「演繹定理」だけどね)。実際に定理(メタ定理)として証明(メタ証明)可能なときもあるし、演繹システムに最初から(設計段階で)この性質を組み込んでしまうこともあります。

今、A, B1, ..., Bn (n = 1 でもよい)が仮定で、C が結論である推論Fがあったとします。スパイダー〈ノード・ワイヤー図〉で描けば下図のようです。

Fがグニョグニョしているのは、ものすごく複雑な推論図でも構わないからです。これは、

  • A, B1, ..., Bn から C が(推論Fで)結論できる

ということです。このことを、横書きテキストとしては、

  • A, B1, ..., Bn |-(F)→ C

と書くことにします(一時的な記法)。

A, B1, ..., Bn |-(F)→ C という推論が認められる(やってもよい、存在する)なら、B1, ..., Bn |-(F')→ A⇒C という推論も認めるべき、というのが演繹原理です。逆も同様なので、

  • 演繹システムにおいて、A, B1, ..., Bn |-(F)→ C という推論が認められる (⇔) B1, ..., Bn |-(F')→ A⇒C という推論が認められる

どちらか一方だけの推論がシステム内で認められ(存在し)、もう一方は禁止されている(存在しない)なんてことがあってはいけないのです。

演繹原理に従わない演繹システムは使い物にならないことが経験上分かっているので、最初から基本リーズニング(システムに組み込みのリーズニング=推論図の基本変形操作)に入れてしまいましょう。

この基本リーズニングは、(カリー/ハワード対応により)ラムダ計算ではラムダ抽象に相当するので、Lambdaとネーミングしました。ネーミングで意味や機能が変わったりしません(ヒルベルトの言葉を思い出せ)。逆方向(下から上)も最初から基本リーズニングに入れてもかまいませんが、別な方法で逆向きリーズニングを有効にすることが多いかな(後述)。

今の例では、一番左のAを結論側に持ってきましたが、必ずしも左端でなくてもかまいません。例えば、

[追記]一番左にしかLambdaリーズニングを許さないとしても、ワイヤーの入れ替え(swap)操作を認めれば、入れ替えによりワイヤーを一番左に持ってこれるので、差支えはありません。[/追記]

フル・リーズニング図を描かないために

入れ子のグラフであるグラフィカルなリーズニング図をフルで描くと手間と面積がかかり過ぎます。フル・リーズニング図を描かないで済ませる工夫がいろいろされてきました。「絵図の描き方と省略法 (A16) // 省略法」にも書きましたが、基本は:

  1. 最後の1枚の推論図だけで済ませる。
  2. 推論図を描かずにプロファイル(シーケントとして書く)で済ませる。

ここでは、「最後の1枚」方式を考えます。ラストシーンの静止画からムービーのストーリー全体を想像せよ、ってわけです。

1枚の推論図に、リーズニング図を再現できるだけの情報を詰め込みます。そのためには、

  • リーズニング・ステップの下段の推論図だけから、上段の推論図を再現できなくてはならない。

また、

  • テキスト記法によるラベルや注釈に、できるだけ頼らない(絵だけで表現する)

ほうが望ましいです。

[追記]

現実的な話をすると、ラストシーンからムービー全体を想像するのは難しいです。ある程度練習しないと出来ないです。そして、1枚の推論図を生成するリーズニング図が一意には決まらないので、想像する人によって違ったリーズニング図が出来上がります。それら複数のリーズニング図は、同じ推論図を生成するという意味で同値なんですが、同値性の話は難しいです(面白いとも言えるが)。

それに、リーズニング図全体の情報を1枚の推論図に詰め込むので、当然ながら、ゴチャゴチャした絵になります。

そんなこんなで、僕は「最後の1枚」方式は推奨しません。「プロファイルで済ませる」方式のほうが、まだしも理解しやすいと思います。

[/追記]

さて、先の例(下に再掲)で、下段の絵だけから、しかもテキストラベルは最小にして上段の絵を再現するには、どんな絵の描き方をすればいいでしょうか?

ワイヤーベンディングと留め金

前節の問題意識で工夫・開発された描画法(絵を描くお約束)がワイヤーベンディング〈ワイヤー曲げ描画法〉です。留め金〈clasp〉を一緒に使うと直感に訴える描画が可能です。留め金を使いだしたのは、おそらく(確証はないが)ジョン・バエズ〈John Baez〉です。

下段の絵から上段の絵を再現するために、上段の絵に一切手を加えずに、そのまま下段に降ろします。しかし、上段の仮定にあったワイヤーの1本は下段で消えます。ホントに消したらダメです(再現用情報が失われる)。ワイヤーを曲げてしまえば、上段の情報を温存して、仮定(上側に突き出たワイヤー群)からは除外できます。

曲げたワイヤーは、下から出るワイヤー(上段では結論)に留め金で止めておきます。

これならば、留め金を外せばすぐさま上段の絵が再現します。ワイヤーが、曲がるけど硬い、プラスチックファイバーのような素材でできてるとします。すると、留め金を外すとビヨ〜ンと戻るでしょう。

  • 曲げて留め金で止める。
  • 留め金を外すとビヨ〜ンと戻る。

映像的でビビッドなイメージが描けるのが、この描画法のメリットです。なお、留め金は必要に応じて何個も描きます。そうでないと、ワイヤーの併置と誤解される危険があります。

ターンバックノードとワイヤーストレッチング

留め金を外す操作を基本リーズニングに入れてもいいのですが、よく使われるのは、留め金でまとめられたワイヤーの片方をもう一度上に向かわせるターンバックノード〈turnback node〉です。

このターンバックノードは、ラムダ計算ではevalであり、論理ではモーダスポネンスになります。eval/モーダスポネンスは非常に有名な計算/推論です。古来より使われてきたeval/モーダスポネンスにより、ワイヤーを再度曲げ戻すわけです。

ラムダ抽象/演繹定理で'∩'状に曲げ、eval/モーダスポネンスで'∪'に曲げ戻すと、結局は何もしないのと同じになります。これを絵に描くと:

ニョロニョロに曲がったワイヤーの引き伸ばし〈ストレッチング〉は、ラムダ計算ではベータ変換〈beta reduction〉と呼ばれます。論理では推論図/リーズニング図の変形〈rewrite | move | deformation | transform〉のなかで最もポピュラーなものですが、名前はないようです。

言いたいことは、次のような推論図は無駄があるから、「∩#1 含意記号の導入」と「モーダスポネンス」は取り除いてもいい、ということです。

          #1
         ---
       A  B  C
      〜〜〜〜〜
       ナニヤラ
      〜〜〜〜〜
          C
      ---------- ∩#1 含意記号の導入
  B     B⇒C
 ---------------- モーダスポネンス
        C

ラムダ計算におけるストレッチングは、「ベータ変換」と呼ばれる次の計算規則(式の還元法)です。記号'・'がevalを表します(詳細は割愛)。

  • (λx.E)・F ⇒β E[F/x]

余談ですが、ニョロニョロを引き伸ばすという操作は、驚くほど多様な場面で登場して、双対性/随伴などの概念を統制しています。

紙面節約のために工夫された描画法という動機から説明したし、実際そうなんですが、「曲がったワイヤー」には、便宜的約束を超えた本質的な意味もあるようです。


眺めるだけでいい参考記事:

*1:実は、天然・自然の摂理で、あるいは数学のイデア界の法則で曲がるのかも知れません。この記事の最後の段落を参照。

2018-12-31(月)

リテラチャー

| 14:17 |

リテラチャーは、セオリーのk-レイヤーの構成素 - 檜山正幸のキマイラ飼育記 メモ編で初めて出てくる概念。基本的な関係は、

  • Lk = k-Lit(Σk+1)
  • Σk in Lk

ここで、

  1. Lkは、k次元レイヤーにいるリテラチャー
  2. Σk+1は、(k + 1)次元レイヤーにいる特定された指標
  3. k-Lit(-) は、(k + 1)-指標からk次元のリテラチャーを作り出す構成〈construction〉
  4. リテラチャーとは、指標または仕様を対象とするℓ-圏。特定された指標(または仕様)は、リテラチャーから選び出す。
  5. リテラチャーLkは、ℓ-圏だが、ℓの値はハッキリしない。ℓはkに依存するかも知れないし、定数かも知れない。
  6. リテラチャーは、インスティチューション用語の指標圏と同義。高次セオリー構造からインスティチューションを作るときは、リテラチャーを指標圏として使う。
  7. アンビエントと特定されたインスタンス」の関係は「リテラチャーと特定された指標」の関係と似ている。意味論側が「アンビエント/特定インスタンス」で、構文側が「リテラチャー/特定された指標」である。
  8. セオリーを指定・特定・定義するとは、すべての次元=レイヤーに渡って、リテラチャーから指標を特定し、アンビエントからインスタンスを特定する行為をすること。
  9. 次元のレイヤーと特定・生成の関係により梯子のような構造が出来る。セオリーの梯子〈ラダー〉と呼んでいいだろう。

定義と仕様

| 14:46 |

次のようなシーケントスタイルの定義は、

For C in Cat, D in 0Cat
For FO : C.Obj → D.Obj in Set
For FM(A, B in C.Obj) : C(A, B) → D(FO(A), FO(B)) in Set
Define
  F : C → D in Cat // F is-a-functor
  :⇔
  F = (FO, FM)
  SuchTaht
  ...
End

仕様としてまとめられる。

specification functor := {
 dom in 0Cat as C,
 cod in 0Cat as D,
 obj-part : C.Obj → C.Obj in Set as FO,
 hom-part(A, B in C) : C(A, B) → D(FO(A), FO(B)) as FH,
! laws
 ...
}

仕様と定義は同じだが、仕様のほうがモジュール化されている。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20181231

2018-12-30(日)

高次射の定義の形式化

| 16:39 |

随伴に関する注意事項 - 檜山正幸のキマイラ飼育記 (はてなBlog)で書いた、「構造か命題か」の問題があるので、構造としての随伴対は、adj(L -| R) と書いて、L -| R は命題として使うことにする。

ほんとは絵で描くのが良いのだが、なんとかアスキーで定義を書いてみる。ネタは、"バスケス-マルケス 2015"(https://arxiv.org/abs/1510.04724)の付録の定義群。

随伴系を対象とする2圏を 2Adj と書いて、随伴系(0-射)のあいだの射(1-射)を定義してみる。ここで:

  • v⇒ : 二重圏の2-射をストリング図で垂直方向(ペースティング図では斜め方向)に考えたもの。
  • v= : 二重圏の明示的等号である2-射(可換四角形)を垂直方向に考えたもの。
  • α ←(v-inv)→β : αとβは互いに垂直方向に逆。
  • α ←(mate)→β : αとβは互いにメイト対応している。
  • L~ は、もとの論文ではオーバーライン
For L:X→C, L~:Y→D, R:C→D, R~:D→Y
Given L -| R, L~ -| R~
For J:C→D, K:X→Y, λ:: L*T v⇒ K*L~ : X→D
Given (R*K:: v= J*R~ :C→Y) ←(v-inv)→ (J*R~ v= R*K :C→Y) ←(mate)→ (λ:: L*T v⇒ K*L~ :X→D)
Define
  Ψ:adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Ψ = (J, K,λ)
End

次のように書いても同じ。

For L:X→C, L~:Y→D, R:C→D, R~:D→Y
Given L -| R, L~ -| R~
Define
  Ψ:adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Ψ = (J, K,λ)
Where
 J:C→D, K:X→Y, λ:: L*T v⇒ K*L~ : X→D
 SuchThat (R*K:: v= J*R~ :C→Y) ←(v-inv)→ (J*R~ v= R*K :C→Y) ←(mate)→ (λ:: L*T v⇒ K*L~ :X→D)
End

一応これで、随伴系のあいだの1-射 Ψ:adj(L -| R) → adj(L~ -| R~) in 2Adj は定義される。絵を描かないとピンとこないと思うが。

次に2-射 Γ::Ψ ⇒ Ψ' : adj(L -| R) → adj(L~ -| R~) in 2Adj を定義する。Ψ'の構成素は、Ψの構成素(名)にすべてダッシュを付けたやつとする。

For α::J v⇒ J':C→D, β::K v⇒ K':X→Y
Given (λ;β)*L~ = (L*β);λ' :: L*T v⇒ K'*L~ : X→D
Define
  Γ::Ψ ⇒ Ψ' : adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Γ = (α, β)
End

あるいは、

Define
  Γ::Ψ ⇒ Ψ' : adj(L -| R) → adj(L~ -| R~) in 2Adj
  :⇔
  Γ = (α, β)
Where
  α::J v⇒ J':C→D, β::K v⇒ K':X→Y
  SuchThat (λ;β)*L~ = (L*β);λ' :: L*T v⇒ K'*L~ : X→D
End

ある程度は形式化した書き方が出来る。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20181230