一貫性条件と一貫性要求と逆一貫性問題

まとめは「一貫性のまとめ」にある。

「一貫性公理」は曖昧でヤバいから使用禁止とする。次を使う。

  • 一貫性の基本射〈elementary morphism〉
  • 基本射が同型なら基本同型射〈elementary isomorphism〉
  • 一貫性条件: 基本射の組み合わせに対する等式の組
  • 一貫性: 基本射の任意の(しかし合法な)組み合わせは、やせた圏となる。
  • 一貫性定理: 一貫性条件を満たす圏は一貫性を持つ。
  • 一貫性要求: 一貫性定理が成立することの要求。
  • 一貫性問題: 与えられた一貫性条件が、一貫性を導くか? という問題。YESと答えるには一貫性定理を証明する。

この前提で、逆一貫性問題と、逆一貫性問題の文脈での一貫性定理を考える。

  • 逆一貫性問題: 一貫性定理を成立させる一貫性条件を見つけよ。
  • 逆一貫性問題の検証: 一貫性問題の解候補として選んだ一貫性条件が、実際に一貫性を導くことの証明。

コンテナと遷移系

コンテナ〈ファミリー〉の演算と特別な射:

  • {{ディリクレ}?{テンソル}?}!積 $`\otimes`$ : コンテナ&レンズ演算〈(0 | 1)-オペレーター〉、遷移系の演算とも考えられる。
  • ジョイン $`\triangleleft, \triangleright`$ : 遷移系の演算、遷移系だけ考えると結合になる。反図式順と図式順。データベース・テーブルのジョインに類似。
  • ピボット: 米田単位 y への射〈レンズ〉。
  • トートロジー{射 | レンズ} : ジョインを実現する特殊なレンズ。トートロジー・ピボットはオウム返し。
  • 内部セッション: 遷移系の一部と考えられる仮想ワイヤー。よくある図法で、⊂ の形になる。この曲がったワイヤーのラベルは状態空間。余トートロジー射の特殊なもの。
  • セッション: 余トートロジー射の特別なもの。
  • インターフェイス: レンズ対象=コンテナ
  • ラッパー、アダプター、(スタックの)レイヤー: レンズのこと。応用分野ごとの名前。

一貫性のまとめ

Wikipedia にある程度従うことにして:

  • {一貫性の}?基本射〈elementary morphisms〉: 注目する生成射。
  • 一貫性〈coherence〉: "various compositions of elementary morphisms are equal." であること。圏が持つそういう性質が一貫性。「一貫性{を持つ | を満たす | が成立する}」と表現する。
  • {一貫性条件 | 一貫性制約} : 一貫性を保証する条件(少数の等式)。
  • 一貫性定理: 「一貫性条件が満たされるなら、一貫性が満たされる」という形の定理。
  • 一貫性要求: 一貫性定理が成立することを、公理として要求すること。

諸悪の根源は「一貫性公理」で、一貫性条件か一貫性要求か不明! 一貫性条件だけでは一貫性は成立しない。一貫性条件+一貫性定理で、圏の一貫性が結論できる。一貫性定理公理に位置付けたのが一貫性要求。「一貫性公理」は避けて、一貫性要求公理と言えばよいし、それが安全。

続・一貫性の用語法

一貫性の用語 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き(別タブ)。

次で良いように思う。違っていたら訂正する。

  1. 基本スパイダー射〈elementary spider morphism〉 = 一貫性射(法則射を含む)
  2. 生成スパイダー射 = 基本スパイダー射
  3. 基本スパイダー射は同型でないときもある。二項演算的な射とか。
  4. スパイダー射 = 基本スパイダー射から適当なドクトリン(主にモノイド圏ドクトリン)で生成された部分圏の射
  5. スパイダー部分圏 = 基本スパイダー射から適当なドクトリンで生成された部分圏
  6. 一貫性公理 = スパイダー部分圏の2-射〈等式〉、または2-射の集合
  7. 一貫性定理 = スパイダー部分圏がやせた圏であるという主張

対象を0-生成射、基本スパイダー射を1-生成射、一貫性公理を2-生成射とするコンピュータッドが出来る。このコンピュータッドが痩せた圏を生成することが一貫性定理のようだ。

ややこしいのが、一貫性定理の内容の主張を公理として要求するとき、一貫性定理公理となる。が、おそらく、これも一貫性公理と呼んでいるので、上記箇条書きの一貫性公理とコンフリクトしている。要注意だ。

ボックス&ストライプ付きストリング図

k-オペレータはk-射に作用するオペレータ、関手は (0 | 1)-オペレータ。

絵図要素 圏論 射の次元
ワイヤー 対象 Cの0-射
ノード Cの1-射
ボックス 1-オペレータ Cの射ではない
細いストライプ 0-オペレータ Cの射ではない
ストライプ 関手 Cの射ではない
ストリング図の書き換え 高次射 Cの2-射

ボックス/ストライプの内部には C とは別な圏の対象・射が描かれるかもしれない。

オペレータの例:

名前 次元
カリー化 1-オペレータ
ベキ集合型構成子 0-オペレータ
ぺき集合反変関手 (0 | 1)-オペレータ
反カリー化 1-オペレータ
デカルト・ペアリング (1, 1)-オペレータ
結合 (1, 1)-オペレータ
デカルト積 (0, 0 | 1, 1)-オペレータ
デカルト積型構成子 (0, 0)-オペレータ
双対対象 0-オペレータ
双対射 1-オペレータ
共役射 1-オペレータ
プレ結合〈引き戻し〉 1-オペレータ
ポスト結合〈押し出し〉 1-オペレータ
トレース 1-オペレータ
不動点 1-オペレータ
マルコフ圏条件化 1-オペレータ
ベイズ反転 1-オペレータ
デカルト微分 1-オペレータ
モナドの拡張 1-オペレータ

SSH関連 (3) known_hosts

関連記事:

  1. SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編
  2. SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編
  3. SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編 この記事


~/.ssh/known_hosts は、クライアントして接続する先のサーバーに関する情報。物理的なテキスト1行で1エントリーになってるが、行は長くなる。Powershellからcutを使ってフィールドを表示できる。削除には ssh-keygen -R ホスト名またはIPアドレス が使える。

PS> cut '-d ' -f1 .\known_hosts
  • 第1フィールド: ホスト名またはIPアドレス、あるいは両方
  • 第2フィールド: 暗号化方式
  • 第3フィールド: 公開鍵データ、Base64エンコード、最後のイコール記号は(あれば)パディング文字

行のフォーマットは authorized_keys ファイルでも似たようなもので、暗号化方式とBase64の公開鍵データ。

sshでリモートホストに接続すると、ローカルにある known_hosts の公開鍵を使ってホスト認証をする。ただし、次の仮定がある。

  • クライアントは、接続先ホストの公開鍵をローカルの known_hosts に持っている。

これは「ニワトリ卵・問題」になる。

unknown host に接続したとき、そのリモートホストの公開鍵が送られてきても、本物かどうかの確認のしようがない。実際に使われる方法は:

  1. リモートホストが公開鍵のフィンガープリント(ハッシュ値)を送る。
  2. ユーザー(人間)が、そのフィンガープリントが目的のリモートホストの公開鍵のフィンガープリントであることを、何らかの方法で確認する。
  3. 確認が済んだら、そのリモートホストを信用する。

二番の手順を実行する手段がほとんどない。電話やメールで確認すればいいが現実的ではない。

ちなみに、フィンガープリントは ssh-keygen -l -f 秘密鍵ファイル(例: id_rsa) で取れる。

SSH関連 (2)

関連記事:

  1. SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編
  2. SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編 この記事
  3. SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編


C:\WINDOWS\System32\OpenSSH\ssh.exe と C:\WINDOWS\System32\OpenSSH\ssh-keygen.exe に関して言えば、$env:USERPROFILE\.ssh\ を見てることが分かった。それは、ssh-keygen -R daphnia.org を実行して分かった。

> ssh-keygen -R daphnia.org
# Host daphnia.org found: line 1
C:\Users\m-hiyama/.ssh/known_hosts updated.
Original contents retained as C:\Users\m-hiyama/.ssh/known_hosts.old

バックアップファイルが $env:USERPROFILE\.ssh\.ssh\known_hosts.old だった。

だが、$env:HOME/.ssh/ にある id_rsa(秘密鍵ファイル)とid_rsa.pub(公開鍵ファイル)を使いたいので、C:\Users\m-hiyama\.ssh\config を次のようにする。

Host daphnia.org
  HostName <IP-Addr>
  User <Usser-Name>
  IdentityFile C:\Users\m-hiyama\Work\.ssh\id_rsa

次のようにしてホストに公開鍵ファイルを送る。

PS> cat ~\.ssh\id_rsa.pub | ssh User-Name@daphnia.org sh -c "cat - >> ~/.ssh/authorized_keys" 
パスワードプロンプト+入力

ここで、Powershell の '~' は $env:HOME を参照する。したがって、C:\Users\m-hiyama\Work\.ssh\id_rsa.pub ファイルが送られる。

sshでログインするには、ssh User-Name@daphnia.org とする。実体としてのサーバが同じでも、IPアドレスや別名でサーバを指定するとパスワード要求されてしまう。

~/.ssh/config ファイルのフォーマットは調べればわかるだろう。

.ssh/known_hosts の作り方だが、configエントリーのHostNameに書かれた名前をキーにして作成される。今回は、IPアドレスを書いておいたので、ホスト名は.ssh/known_hostsに書き込まれない。コマンドライン・インターフェースとしては、エントリータイトルが使われ、.ssh/known_hostsのキーはHostNameフィールドの値が使われる、という例によってハマりやすい仕様。

SSH関連

関連記事:

  1. SSH関連 - (新) 檜山正幸のキマイラ飼育記 メモ編 この記事
  2. SSH関連 (2) - (新) 檜山正幸のキマイラ飼育記 メモ編
  3. SSH関連 (3) known_hosts - (新) 檜山正幸のキマイラ飼育記 メモ編


困っていること で述べたように、~/.ssh/ が二箇所ある。

さらに、拡張子が、.key, .ppk, なし, .pub のファイルがある。記憶はないが:

  1. .ppk は PuTTY〈パティ〉 のファイルらしい。PuTTYgen で生成されるらしい。PPK〈PuTTY Private Key〉形式。
  2. デフォルトないしは習慣では、秘密鍵を id_rsa.ppk、公開鍵を id_rsa.pub にするらしい。
  3. .keyファイルは、"-----BEGIN RSA PRIVATE KEY-----" で始まっている。openssl コマンドとか ssh-keygen コマンドで生成されたらしい。フォーマットは「PEM〈Privacy Enhanced Mail〉形式」というらしい。
  4. Proc-Type: と DEK-Info: というヘッダがある場合は decrypt されてないPEM形式。ヘッダなしで裸のBase64なら decrypt 済みということらしい。が フォーマットの変更があってナニヤラ、https://dev.classmethod.jp/articles/openssh78_potentially_incompatible_changes/ 参照。
  5. 現状のローカルケースでは、.key がヘッダ付きPEM形式、拡張子なしが裸のPEM形式、.ppk がPPK形式。
  6. 公開鍵は、秘密鍵から modulus と publicExponent だけを抜き出したものらしいので、.ppk とか .key(PEM形式)から、.pub(公開鍵部分)を生成することは出来るだろう。
  7. known_hosts も二箇所に2つある。
  8. ~/.ssh/known_hosts はユーザーレベル。サーバレベルのファイルとして、/etc/ssh/known_hosts 。
  9. ssh ではじめて特定ホストに接続しようとしたときに、~/.ssh/known_hosts にエントリが追加される。エントリーごとの情報は、相手サーバの fingerprint。
  10. ~/.ssh/known_hosts は、当該ユーザーがssh接続しようとしている先のホストを“ホスト認証”するために使われる。
  11. ssh-keygen -R 〈ホストにIPアドレスか名前〉 で特定のknown_hostsエントリーを消せる。
  12. known_hostsエントリーがなくても、「初めての接続」状態になるだけ。実害はない。が、パスワードによるユーザー認証になるので、それが原因でトラブルになる可能性がある。

詳細をチェックするのは面倒だが:

  1. .key と .ppk は消したい。
  2. 接続しないサーバの ~/.ssh/known_hostsエントリーは消したい。
  3. 秘密鍵ファイル id_rsa はひとつだけにしたい。
  4. 公開鍵ファイル id_rsa.pub のマスターはひとつだけにしたい。
  5. ローカルの id_rsa.pub を接続先サーバに何らかの方法で転送して、~/.ssh/authorized_keys にアペンドする。

wt(Windows Terminal) + SSH

内容:

設定ファイル(JSON)

wt の設定ファイルの場所がややこしい!

  • $env:LocalAppData\Packages\Microsoft.WindowsTerminal_8wekyb3d8bbwe\LocalState\settings.json

順番に辿るなら:

> cd $env:local[TAB]
(補完: cd $env:LOCALAPPDATA)
> cd Packages
> cd .\Microsoft.WindowsT[TAB]
(補完: cd .\Microsoft.WindowsTerminal_8wekyb3d8bbwe\)
> cd LocalS
(補完: cd .\LocalState\)
> code .

ConoHa の設定エントリーなら次のよう。

{
    "backgroundImage": null,
    "colorScheme": "Solarized Light",
    "commandline": "ssh XXX@XXX(ip addr)XXX",
    "guid": "{d2c4024c-bdae-5a30-81ff-877fed55010a}",
    "icon": "C:\\Users\\m-hiyama\\Pictures\\2021-08\\ConoHa-Co.jpg",
    "name": "ConoHa"
},
目的

ターミナルタブを開いときに実行されるコマンドは ssh コマンド(C:\WINDOWS\System32\OpenSSH\ssh.exe)。

現状パスワードを聞かれるので、パスワードをスキップする設定にする。https://zaki-hmkc.hatenablog.com/entry/2020/09/03/083634 によると、次のいずれか:

  1. パスフレーズなし秘密鍵を作成し、それを、デフォルトの鍵ファイル名(おそらく ~/.ssh/id_rsa)にする(デフォルトは諸悪の根源だから使う気はない)
  2. パスフレーズなし秘密鍵を作成し、それを、.ssh/config に設定
  3. パスフレーズなし秘密鍵を作成し、それを、JSON設定ファイルの commandline 項目に指定のsshコマンドラインの-iオプションに指定
基本

まず、基本概念や問題点を列挙する:

  1. 鍵ペア: SSHクライアント用の秘密鍵、SSH サーバー用の公開鍵のペア
  2. 秘密鍵と公開鍵を作成する際にパスフレーズとコメントを埋め込むことができる。が使う必要はない。特に今回は入れない!
  3. Windowsデフォルト設定において: [Administrators] グループのみ、公開鍵 (authorized_keys) の場所が OpenSSH デフォルトの .ssh\authorized_keys ではなく、設定ファイル C:\ProgramData\ssh\sshd_config の設定により決まる。
  4. さらに、設定ファイルにおけるデフォルトの AuthorizedKeysFile は $env:PROGRAMDATA\ssh\administrators_authorized_keys
  5. 全ユーザーで設定を合わせたい場合は、事前に、管理者権限で設定ファイルの最終2行(AuthorizedKeysFile)をコメントアウトしてからサービスを再起動しておく必要がある。
  6. SSH鍵ペアは、ssh-keygen コマンドで作れる。
  7. ssh-keygen -q でメッセージを表示しない。-C "" でコメントなし、-N "" でパスフレーズなし。
  8. sshコマンドの -t オプションには暗号化方式を指定、RSA、DSA、ECDSA、Ed25519、SSH-1(RSA) などがある。https://gigazine.net/news/20200828-ssh-encryption-algorithm/ によると、EdDSA(Ed25519)推奨。DSA やECDSA は使わないらしい。RSA, SSH-1 は論外。
  9. ssh-keygen -f ファイル名 で、生成する秘密鍵ファイルを明示的に指定。
  10. ssh-keygenコマンド実行後、ホームフォルダー配下に .ssh フォルダーが作成され、その配下に鍵ペア(のファイル)が生成される。
  11. 生成されるファイル名は id_rsa と id_rsa.pub 。id_rsa が秘密鍵、id_rsa.pub が公開鍵。
  12. cmd.exe からなら、コマンドライン: ssh-keygen.exe -q -t ed25519 -C "" -N "" -f id_rsa
  13. Powershell ではssh-keygen.exe -q -t ed25519 -C '""' -N '""' -f id_rsahttps://qiita.com/overflowfl/items/14a2486df85fd7efac85より)
  14. サーバー側での公開鍵ファイル名のデフォルトは authorized_keys、mv id_rsa.pub authorized_keys して使う。
  15. Windowsがサーバーのとき、 icacls authorized_keys /remove Everyone でアクセス権限変更。
  16. SSHクライアントは、サーバー上の authorized_keys に対応する秘密キーを自マシンに保持している必要がある。サーバー側で鍵ペアを生成したなら、(秘密鍵)サーバ → クライアント の転送; クライアント側で鍵ペアを生成したなら、(公開鍵)クライアント → サーバ の転送が必要。
  17. サーバ → クライアント の転送なら sftp などで当該の id_rsa をローカルに持ってくる。

今回は、クライアントマシン側でキーフレーズなしの鍵ペアを生成して、公開鍵をサーバ側に送る。

  1. Powershell で、ssh-keygen.exe -q -t ed25519 -C '""' -N '""' -f id_rsa
  2. サーバ側の公開鍵の送り先は、~/.ssh/authorized_keys 。ただし、もともとあるファイルを潰さないように、cat id_rsapub >> ~/.ssh/authorized_keys でアペンドする。
  3. ファイル転送に使う方法は何でもいいが、https://zaki-hmkc.hatenablog.com/entry/2020/09/03/083634 にあったのは以下の対話。
PS> cat .\.ssh\id_rsa_nopass.pub | ssh user@host sh -c "cat - >> ~/.ssh/authorized_keys" 
(サーバからのパスワード要求) password: (これは仕方ない)
秘密鍵ファイル名のコマンドライン指定

ローカルの秘密鍵ファイル名を指定する方法なら、wtの設定JSONファイル内で:

{
    "backgroundImage": null,
    "colorScheme": "Solarized Light",
    "commandline": "ssh XXX@XXX(ip addr)XXX -i 秘密鍵ファイルのフルパス(バックスラエスケープに注意)",
    "guid": "{d2c4024c-bdae-5a30-81ff-877fed55010a}",
    "icon": "C:\\Users\\m-hiyama\\Pictures\\2021-08\\ConoHa-Co.jpg",
    "name": "ConoHa"
},

この方法なら、他の設定は必要ない。

設定ファイルに秘密鍵ファイル名を指定
  • $env:USERPROFILE\.ssh\config に秘密鍵ファイルの名前と置き場所を指定
Host <Host-Nickname>
  HostName <IP-Addr>
  User <User-Name>
  IdentityFile <PathToIdRsaFile>
困っていること

sshコマンドが C:\WINDOWS\System32\OpenSSH\ssh.exe 以外、あるいは別なシェルから使う場合で状況が違って、.ssh の実際の場所が

  1. $env:USERPROFILE\.ssh\
  2. $env:HOME\.ssh\config 異なる場所

の2つがある。どっちがどっちかワケワカラナクなっている。他のコマンドでも同じ混乱が起きている。

演繹拡大の定式化

公理系を演繹的に拡大するメカニズムの定式化に:

  1. 閉包システム〈closure system〉
  2. 単純伴意システム〈simple entailment sysmte〉
  3. バンチ伴意システム〈bunched entailment sysmte〉
  4. 双対バンチ伴意システム〈dual bunched entailment sysmte〉

伴意関係を |- とすると:

  • 単純伴意システム: 文の集合 |- 文
  • バンチ伴意システム: 文の集合 |- 文の集合 、 左右の意味は連言
  • 双対バンチ伴意システム: 文の集合 |- 文の集合 、 右の意味は選言(ゲンツェン流)

双対バンチ伴意システムがゲンツェン流で難しい。

SSL証明書更新〈renew〉手順

クライアントにて:

  1. Windows Termina wt を起動。
  2. ConoHa への接続のタブを開く。
  3. ログインする。

接続情報は非常に分かりにくい場所にある。PowerShell構文で:

  • $env:LocalAppData\Packages\Microsoft.WindowsTerminal_8wekyb3d8bbwe\LocalState\settings.json

"8wekyb3d8bbwe" もこのまま。ヒドイ。JSONファイルは見ればわかる。他の情報は、~/servers.txt(UTF-8) にある。

サーバー側 手動の場合:

  1. certbot certificates で現状確認。
  2. systemctl stop nginx でNginxを止める。
  3. certbot renew --dry-run で実行シミュレーション
  4. certbot renew で実行。
  5. systemctl start nginx でNginxを起動。

実際の記録:

# certbot certificates
Saving debug log to /var/log/letsencrypt/letsencrypt.log

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Found the following certs:
  Certificate Name: www.chimaira.org
    Serial Number: 31f953e4f025ac1e00ed78a83abbaa852b6
    Key Type: RSA
    Domains: www.chimaira.org
    Expiry Date: 2022-09-04 12:21:55+00:00 (VALID: 13 days)
    Certificate Path: /etc/letsencrypt/live/www.chimaira.org/fullchain.pem
    Private Key Path: /etc/letsencrypt/live/www.chimaira.org/privkey.pem
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
# systemctl stop nginx
# certbot renew --dry-run
Saving debug log to /var/log/letsencrypt/letsencrypt.log

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Processing /etc/letsencrypt/renewal/www.chimaira.org.conf
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Account registered.
Simulating renewal of an existing certificate for www.chimaira.org

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Congratulations, all simulated renewals succeeded: 
  /etc/letsencrypt/live/www.chimaira.org/fullchain.pem (success)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
# certbot renew
Saving debug log to /var/log/letsencrypt/letsencrypt.log

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Processing /etc/letsencrypt/renewal/www.chimaira.org.conf
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Renewing an existing certificate for www.chimaira.org

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Congratulations, all renewals succeeded: 
  /etc/letsencrypt/live/www.chimaira.org/fullchain.pem (success)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
# systemctl start nginx

多圏類似構造 分類

  • 色付き/色無しは無意味で誤解をまねくリスクがあるので使わない。
  • 対称/(非対称) : 対称作用を持つか? 対称構造の忘却で非対称になる。
  • モノイド/(非モノイド) : モノイド積を持つか? モノイド積の忘却で非モノイドになる。
  • ワイド/ナロー : 多結合の幅が1か1以上。ワイド性の忘却でナローになる。

単純組み合わせで8種類の多圏ができる。

  1. 非対称・非モノイド・ナロー多圏 = ナロー多圏
  2. 非対称・非モノイド・ワイド多圏 = ワイド多圏 (= 多圏)
  3. 非対称・モノイド・ナロー多圏 = モノイド・ナロー多圏 ?
  4. 非対称・モノイド・ワイド多圏 = モノイド・ワイド多圏 = モノイド多圏*
  5. 対称・非モノイド・ナロー多圏 = 対称ナロー多圏 = サボ多圏
  6. 対称・非モノイド・ワイド多圏 = 対称ワイド多圏 = 対称多圏 = プロペラッド
  7. 対称・モノイド・ナロー多圏 ?
  8. 対称・モノイド・ワイド多圏 = 対称モノイド多圏 = PROP〈プロップ〉*

実際に使うのは:

  1. モノイド多圏=非対称・モノイド・ワイド多圏 (モノイド圏から複アロー構成)
  2. 対称モノイド多圏=対称・モノイド・ワイド多圏(対称モノイド圏から複アロー構成)

複圏に関しては:

  1. 非対称・非モノイド・ナロー複圏 = ナロー複圏
  2. 非対称・非モノイド・ワイド多圏 = ワイド複圏 、ナロー複圏から作れる
  3. 非対称・モノイド・ナロー複圏 = モノイド・ナロー複圏、多圏になってしまう
  4. 非対称・モノイド・ワイド複圏 = モノイド・ワイド多圏、多圏になってしまう
  5. 対称・非モノイド・ナロー複圏 = 対称ナロー複圏、
  6. 対称・非モノイド・ワイド複圏 = 対称ワイド多圏、対称ナロー複圏から作れる
  7. 対称・モノイド・ナロー複圏、多圏になってしまう
  8. 対称・モノイド・ワイド複圏、対称・モノイド・ナロー複圏から作れる、多圏になってしまう

結局意味があるのは:

  1. 非対称複圏
  2. 対称複圏

複圏であることを保存するなら:

  1. 非対称複圏+ペアリング
  2. 対称複圏+ペアリング

ペアリングにはワイヤー二項演算が必要。

余複圏も意味を持つ気がする。

論理フレームワークと証明

次のようなメタ記号を使う。$`\newcommand{\TS}{\mathrel{\,|\!-} }
\newcommand{\TTS}{\mathrel{\,||\!-} }
\newcommand{\TTTS}{\mathrel{\,|||\!-} }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\In}{\text{ in } }
\newcommand{\cat}[1]{\mathcal{#1} }
%`$

  1. $`\TS_N`$ 自然演繹システムで証明可能
  2. $`\TTS_S`$ シーケントシステムで証明可能
  3. $`\TTTS_\Phi`$ メタシーケント・システム(論理フレームワーク)で証明可能

$`\Gamma`$ は論理式のリストとする。次は、$`\Gamma`$ を仮定して、論理式 $`P`$ が証明可能なこと。

$`\quad \Gamma \TS_N P`$

システム $`N`$ で演繹定理が成立するなら、次と同じ。

$`\quad \TS_N (\land)^*(\Gamma) \Imp P`$

ここで、$`(\land)^*`$ は二項演算をリスト引数化したもの。

自然演繹に対応するシーケント計算があったして、次のメタ定理が欲しい。

$`\quad (\TTS_S \Gamma \to P) (\Iff) (\Gamma \TS_N P)`$

これらのセマンティクスは:

  • $`(\TTS_S \Gamma \to P) (\Iff) (\exists d : \Gamma \to P \In \cat{N}. \text{True} )`$
  • $`(\Gamma \TS_N P) (\Iff) (\exists d : \Gamma \to P \In \cat{N}. \text{True} )`$

論理フレームワークを $`F`$ とすると、次のメタ定理が欲しい。

$`\quad ( \mathscr{K} \TTS_F \Gamma \to P) (\Iff) (\TTS_S \Gamma \to P)`$

また、メタシーケント計算システム $`\Phi`$ があって、次のメタ定理が欲しい。

$`\quad (\TTTS_\Phi \mathscr{K} \Rightarrow (\Gamma \to P)) (\Iff)
( \mathscr{K} \TTS_F \Gamma \to P)
%`$

セマンティクスは:

$`\exists d: \Gamma \to P \In \mathscr{K}^{*\Phi}
%`$

$`\mathscr{K}^{*\Phi}`$ は、生成系 $`\mathscr{K}`$ から作った自由$`\Phi`$複圏。次も成立する。

$`\quad \mathscr{K}^{*\Phi} = \cat{N}`$

型理論と論理

長谷川真人さんの "Classical Linear Logic of Implications"https://www.kurims.kyoto-u.ac.jp/~hassei/papers/clli.pdf

加法的〈非線形〉コンテキストと乗法的〈線形〉コンテキストを持つ型判断〈typing judgement〉

$`\quad \Gamma ;\Delta \vdash M:\sigma`$

を考える。具体的には、

$`\quad x_1:\sigma_1, \cdots, x_m:\sigma_m ;\, y_1:\tau_1, \cdots,y_n:\sigma_n \vdash M:\sigma`$

これの意味は:

  1. シーケント $`!\sigma_1, \cdots, !\sigma_m ,\, \tau_1, \cdots, \sigma_n \vdash \sigma`$ の証明が $`M`$ 。
  2. 命題 $`!\sigma_1 \otimes \cdots \otimes !\sigma_m \otimes \tau_1 \otimes \cdots \otimes \sigma_n \multimap \sigma`$ の証明が $`M`$

二種類の含意を持つが、それは型理論的にアロー型と解釈する。

型理論 論理
アロー型構成子 含意演算
ペア型構成子 連言演算
命題
型のインスタンス 命題の証明〈保証〉
プロファイル シーケント
型コンテキスト 平坦バンチ
型判断 定理記述
証明〈導出〉

多圏類似構造

"Shapely monads and analytic functors" by Richard Garner, Tom Hirschowitz

これが多圏類似構造のテキストとして非常によい。

多圏類似構造の分類を絵算〈グラフィカル計算〉との関係で論じている。多射の図がどうなるかと、どう繋げるかで分類できる。分類基準は:

  1. 多射の図に不連結を許すか?、これは「モノイド積構造を許すか?」
  2. 繋げるワイヤーは1本か、任意のn本か?
  3. 対称群が作用するのか、しないのか?
  4. 対称群の作用を、対称射〈置換射〉として記述するか、作用のままなのか?
  5. 基本スパイダー=基本ジャンクション〈{primitive | elementary} wiring junction〉を持つか、どの程度持つか?

図の連結性・不連結性は目から鱗。もし、不連結な図を許さないとすると、ワイヤーのリストや多射のリストは多射ではなくて、別な概念レベルに置かなくてはならない。これは複射の場合も同じ、つうかより鮮明。ツリーとヘッジを別な概念レベルで考える必要がある。

ガーナー/フーショウィッツは対称群が作用する多圏類似構造を次のように分類している。

モノイド積なし モノイド積あり Δ! あり
1:1 結合 i
n:n 結合 ii' ii iii
  • i は多圏〈色付き対称多圏〉サボ多圏〈Szabo polycategory〉
  • ii' はプロペラッド〈色付きプロペラッド〉 モノイド積なし
  • ii はPROP〈色付きPROP | 対称モノイド・色付きプロペラッド〉
  • iii はローヴェア・セオリー〈色付きデカルトPROP | ローヴェア多圏〉

色付きはいちいち言わないことにして、我々はモノイド構造を前提にしたいので:

  • サボ多圏 (使わない)
  • 対称モノイド多圏
  • デカルト・モノイド多圏 = ローヴェア多圏