推論規則〈inference rule〉と型つけ規則〈typing rule〉の両方を含むシステムで使いやすいものがないかな、と探していました。僕が思う“使いやすい”とは：
- 意味論〈セマンティクス〉はハイパードクトリン。
- カリー／ハワード／ランベック対応と相性がよい。
- 自然演繹としてもシーケント計算としても使える。
これらの条件をまーまー満たすシステムを見つけたので紹介します。これから紹介する推論規則／型つけ規則は、次のバーケダル*1／ビージャック*2の論文にあるものを僅かに変更したものです。
- Title: A Taste of Categorical Logic — Tutorial Notes
- Authors: Lars Birkedal (birkedal@cs.au.dk), Aleš Bizjak (abizjak@cs.au.dk)
- Date: July 10, 2017
- Pages: 41p
- URL: https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf
$`\require{color}
\newcommand{\KW}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Arr}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
%`$内容：
- 記法に関する注意
- 構文論と意味論
- カリー／ハワード／ランベック対応
- 規則の書き方
- ファイバー方向複圏構造の基礎
- ベースとファイバーの関係
- 論理記号の導入・消去
- ベース方向複圏構造の基礎
- ベース方向複圏その他
ハブ記事：
記法に関する注意
ターンスタイル記号 '$`\vdash`$' は、証明可能性〈導出可能性〉を表すメタ述語記号としても、シーケントの区切り記号としても使われます。このオーバーロードは混乱・誤解をまねくリスクがありますが、広く採用されているので、ここでもシーケントの区切り記号に '$`\vdash`$' を使います。区切り記号としてのターンスタイルは、特に何かを主張するものではなくて、単に“区切りに使う変な矢印”です。
バーケダル／ビージャックのテキストに従い、論理式は $`\varphi, \psi, \chi`$ などのギリシャ文字小文字で表します。論理式を並べたリストを命題コンテキスト〈proposition context〉と呼び、ギリシャ文字大文字 $`\Theta, \Xi`$ などで表します。命題コンテキスト内の論理式には名前〈ラベル〉を付けてもかまいません。次の一番目はラベルなしの命題コンテキスト、二番目はラベル付きの命題コンテキストです*3。
- $`\Theta = (\varphi_1, \cdots, \varphi_n)`$
- $`\Theta = (A_1: \varphi_1, \cdots, A_n:\varphi_n)`$
ターンスタイル記号の左に命題コンテキスト、右に単一の論理式を配置した記号的表現がここで扱うシーケント〈sequent〉です。シーケントは次の形です。
$`\quad \Theta \vdash \psi`$
左側の命題コンテキストを展開して書けば：
- $`\quad (\varphi_1, \cdots, \varphi_n) \vdash \psi`$
- $`\quad (A_1: \varphi_1, \cdots, A_n:\varphi_n) \vdash \psi`$
リストを囲む丸括弧はしばしば省略されます。
- $`\quad \varphi_1, \cdots, \varphi_n \vdash \psi`$
- $`\quad A_1: \varphi_1, \cdots, A_n:\varphi_n \vdash \psi`$
$`(\varphi)`$ と $`\varphi`$ は同一視され、リストの連接記号にもカンマが流用されます（そういう習慣なのです）。
さて、論理式には自由変数（自由な対象変数〈個体変数〉）が登場するでしょう。それらの自由変数の型を指定するために型コンテキスト〈{type | typing} context〉を使います。型コンテキストは次の形です。
$`\quad (x_1:\sigma_1, \cdots, x_n:\sigma_n)`$
ここで、$`x_1, \cdots, x_n`$ は変数記号で、$`\sigma_1, \cdots, \sigma_n`$ は型項〈type term〉です。型項は型を表す記号的表現ですが、その意味論は後述します。
型項はギリシャ文字小文字 $`\sigma, \tau, \rho`$ などで表します。型コンテキストはギリシャ文字大文字 $`\Gamma, \Delta`$ などで表します。これもバーケダル／ビージャックに従っています。
型コンテキストを伴ったシーケントは次のように書きます。
$`\quad \Gamma \mid \Theta \vdash \psi`$
以下常に、$`\Theta, \psi`$ 内に出現するすべての自由変数記号は、$`\Gamma`$ で型宣言されていると仮定します。
$`M`$ が値を表す項のとき、型判断〈{type | typing} judgement〉は通常次の形に書きます。
$`\quad \Gamma \vdash M:\tau`$
しかし、ターンスタイル記号をさらにオーバーロードするのはキビしい（僕が耐えられない）ので、型判断の構文は次のように変更します。
$`\quad M:\Gamma \to \tau`$
型判断とシーケントの意味論を、ハイパードクトリン（「述語論理： ベース圏と論理代数の圏」に簡単な説明があります）により行うとき、普通の矢印はベース圏〈base category〉の射、ターンスタイルはファイバー〈fibre | fiber〉の射と区別できて混乱が少なくなります。
構文論と意味論
構文論と意味論をごく手短に説明します。
型項は、基本型〈{primitive | basic} type〉を表す記号から、型構成子記号〈type constructor symbol〉を使って組み立てます。ここで使う型構成子記号は：
- '$`\times`$' ： 直積型〈ペア型〉を構成する。
- '$`\Arr`$' ： 指数型〈アロー型 | 関数型〉を構成する。
- '$`+`$' ： 直和型〈タグ付きユニオン型 | バリアント型〉を構成する。
記号 '$`\Arr`$' は論理記号の含意〈implication〉とオーバーロードしているので注意してください（指数型と含意はカリー／ハワード／ランベック対応で対応します）。
基本型のなかでも特に基本的な型は次の記号で表します。
- $`1`$ ： 終対象型〈ユニット型 | シングルトン型〉
- $`0`$ ： 始対象型〈エンプティ型 | ネバー型〉
なお、バーケダル／ビージャックは直和型と始対象型は扱っていません。カリー／ハワード／ランベック対応をより徹底するために追加しました。
値を表す項（単に項〈term〉と呼ぶ）は、基本関数を表す記号から型付きラムダ式〈型付きラムダ項〉の構文で組み立てます。項 $`M`$ が型コンテキスト $`\Gamma`$ のもとで型 $`\tau`$ を持つことを、
$`\quad M: \Gamma \to \tau`$
と書くのでした（型判断）。
型項と項の意味は、ハイパードクトリン $`(\cat{C}, \cat{L}, \mrm{Pred})`$ のベース圏により与えます。特に $`\cat{C} = {\bf Set}`$ とした場合が標準的です。型構成子記号 '$`\times`$'、'$`\Arr`$'、'$`+`$' は、常識的な直積、指数、直和で解釈できます。項の解釈は関数〈写像〉ですが、複数引数単一戻り値になるので複関数〈multifunction〉と呼びましょう。今詳しくは述べませんが、
- 関数〈function〉は、圏 $`{\bf Set}`$ の射
- 複関数〈multifunction〉は、圏 $`{\bf Set}`$ から作った複圏〈multicategory〉の複射〈multimorphism | multiarrow〉
- 多関数〈polyfunction〉は、圏 $`{\bf Set}`$ から作った多圏〈polycategory〉の多射〈polymorphism | polyarrow〉*4
です。
今回の定式化では、複圏（オペラッド〈operad〉ともいう）と複射〈複アロー〉を使っています。潜在的に多圏と多射〈多アロー〉も使っているのですが、表立って多圏・多射が現れないようにしています。
型項と項の意味はスコットブラケット $`\left[\!\left[ - \right]\!\right]`$ を使って記述します。以下は、バーケダル／ビージャックからのコピー（PDFからの画像）です。バーケダル／ビージャックの $`\to`$ を我々は $`\Arr`$ 、$`\vdash`$ を $`\to`$ としています。直和型と始対象型は含まれませが、見当はつくでしょう。
シーケント（命題コンテキストと結論である論理式）の意味は、ハイパードクトリンのファイバー方向の圏によって意味を与えます。$`\left[\!\left[ \Gamma \right]\!\right] = X`$ とすると、次のシーケントの意味は $`\mrm{Pred}[X]`$ のなかの射になります。
$`\quad \Gamma \mid \Theta \vdash \psi`$
カリー／ハワード／ランベック対応
型項と項は、ハイパードクトリンのベース圏に意味を持ちます。一方、命題、命題コンテキスト、シーケントはハイパードクトリンのファイバー方向の圏に意味を持ちます。ベース方向の圏とファイバー方向の圏（たくさんある）は別な圏ですが、そっくりな構造を持ちます。「そっくりだ」という主張がカリー／ハワード／ランベック対応です。
この後で、推論規則〈inference rule〉と型つけ規則〈typing rule〉を列挙しますが、それらはカリー／ハワード／ランベック対応で次のように対応します。
| 一般概念 | ファイバー方向 | ベース方向 |
|---|---|---|
| 恒等射 | IDENTITY-PROP | IDENTITY |
| 複結合 | CUT | MCOMP |
| 破棄射 | WEAK-PROP | DEL |
| コピー射 | CONTR-PROP | COPY |
| 対称射 | EXCH-PROP | SYMM |
| 終射 | TRUE | FIN, UNIT |
| 始射 | FALSE | INI |
| デカルト積 | AND-I | PROD, PAIRING |
| 第一射影 | AND-E1 | PROJ1 |
| 第ニ射影 | AND-E2 | PROJ2 |
| デカルト余積 | OR-E | COPROD, COPAIRING |
| 第一入射 | OR-I1 | INJ1 |
| 第ニ入射 | OR-I2 | INJ2 |
| 無限デカルト積 | ALL-I | - |
| 成分〈射影〉 | ALL-E | - |
| 無限デカルト余積 | SOME-E | - |
| 余成分〈余射影〉 | SOME-I | - |
| カリー化 | IMP-I | ABS |
| 適用 | IMP-E | APP |
規則の書き方
バーケダル／ビージャックからの推論規則のコピー（PDFからの画像）は以下です。
推論規則の記述にほとんど常に使われる横棒を使う方式です。が、これをうまくレイアウトするのは大変なので、英語風キーワード（緑色）を使うことにします。
$`\KW{If we have }\text{横棒の上段}\\
\KW{Then using } \text{規則の名前}\\
\KW{We have }\text{横棒の下段}
%`$
横棒の上段が複数あるときは $`\KW{And}`$ で並べます。
型つけ規則も同じ記法で記述します。項の実際の構成を省略するので、型つけ規則は（通常より）簡略に書けます。
ここから先は推論規則と型つけ規則の列挙です。個々の規則の解説はまた別の機会に。
ファイバー方向複圏構造の基礎
IDENTITY-PROP
ファイバー方向恒等射の存在
$`\KW{If we have nothing}\\
\KW{Then using }\text{IDENTITY-PROP}\\
\KW{We have }\Gamma \mid \varphi \vdash \varphi
%`$
CUT
ファイバー方向複結合の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{And } \Gamma \mid \Xi, \varphi \vdash \psi\\
\KW{Then using }\text{CUT}\\
\KW{We have }\Gamma \mid \Theta, \Xi \vdash \psi
%`$
WEAK-PROP
ファイバー方向破棄射の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{WEAK-PROP}\\
\KW{We have }\Gamma \mid \Theta, \psi \vdash \varphi
%`$
CONTR-PROP
ファイバー方向コピー射の存在
$`\KW{If we have } \Gamma \mid \Theta, \varphi,\varphi \vdash \psi\\
\KW{Then using }\text{CONTR-PROP}\\
\KW{We have }\Gamma \mid \Theta, \varphi \vdash \psi
%`$
EXCH-PROP
ファイバー方向対称射の存在
$`\KW{If we have } \Gamma \mid \Theta, \varphi, \psi, \Xi \vdash \chi\\
\KW{Then using }\text{EXCH-PROP}\\
\KW{We have } \Gamma \mid \Theta, \psi, \varphi, \Xi \vdash \chi
%`$
ベースとファイバーの関係
WEAK-TYPE
射影多関数による引き戻し
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{WEAK-TYPE}\\
\KW{We have }\Gamma, x:\sigma \mid \Theta \vdash \varphi
%`$
CONTR-TYPE
コピー多関数による引き戻し
$`\KW{If we have } \Gamma, x:\sigma, y:\sigma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{CONTR-TYPE}\\
\KW{We have } \Gamma, x:\sigma \mid \Theta[x/y] \vdash \varphi[x/y]
%`$
EXCH-TYPE
対称多関数による引き戻し
$`\KW{If we have } \Gamma, x:\sigma, y:\rho \mid \Theta \vdash \varphi\\
\KW{Then using }\text{EXCH-TYPE}\\
\KW{We have } \Gamma, y:\rho, x:\sigma \mid \Theta \vdash \varphi
%`$
SUBSTITUTION
任意の複関数による引き戻し
$`\KW{If we have } \Delta, x:\sigma, \Delta' \mid \Theta \vdash \psi\\
\KW{And } M: \Gamma \to \sigma\\
\KW{Then using }\text{SUBSTITUTION}\\
\KW{We have } \Delta, \Gamma, \Delta' \mid \Theta[M/x] \vdash \varphi[M/x]
%`$
論理記号の導入・消去
TRUE
ファイバー方向終射の存在
$`\KW{If we have nothing}\\
\KW{Then using }\text{TRUE}\\
\KW{We have } \Gamma \mid \Theta \vdash \top
%`$
FALSE
ファイバー方向始射の存在
$`\KW{If we have nothing}\\
\KW{Then using }\text{FALSE}\\
\KW{We have } \Gamma \mid \Theta, \bot \vdash \psi
%`$
AND-I
ファイバー方向デカルト積の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{And } \Gamma \mid \Theta \vdash \psi\\
\KW{Then using }\text{AND-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi \land \psi
%`$
AND-E1
ファイバー方向第一射影の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi \land \psi\\
\KW{Then using }\text{AND-E1}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi
%`$
AND-E2
ファイバー方向第ニ射影の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi \land \psi\\
\KW{Then using }\text{AND-E2}\\
\KW{We have } \Gamma \mid \Theta \vdash \psi
%`$
OR-E
ファイバー方向デカルト余積の存在
$`\KW{If we have } \Gamma \mid \Theta, \varphi \vdash \chi\\
\KW{And } \Gamma \mid \Theta, \psi \vdash \chi \\
\KW{Then using }\text{OR-E}\\
\KW{We have } \Gamma \mid \Theta, \varphi\lor \psi \vdash \chi
%`$
OR-I1
ファイバー方向第一入射の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{OR-I1}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi\lor \psi
%`$
OR-I2
ファイバー方向第ニ入射の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \psi\\
\KW{Then using }\text{OR-I1}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi\lor \psi
%`$
IMP-I
ファイバー方向カリー化
$`\KW{If we have } \Gamma \mid \Theta, \varphi \vdash \psi\\
\KW{Then using }\text{IMP-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi\Imp \psi
%`$
IMP-E
ファイバー方向適用射の存在
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi \Imp \psi\\
\KW{And } \Gamma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{IMP-E}\\
\KW{We have } \Gamma \mid \Theta \vdash \psi
%`$
ALL-I
ファイバー方向無限デカルト積の存在
$`\KW{If we have } \Gamma, x:\sigma \mid \Theta \vdash \varphi\\
\KW{Then using }\text{ALL-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \forall x:\sigma.\varphi
%`$
ALL-E
ファイバー方向無限デカルト積の成分 $`M/x`$
$`\KW{If we have } \Gamma \mid \Theta \vdash \forall x:\sigma.\varphi\\
\KW{And } M:\Gamma \to \sigma\\
\KW{Then using }\text{ALL-E}\\
\KW{We have } \Gamma \mid \Theta \vdash \varphi[M/x]
%`$
SOME-E
ファイバー方向無限デカルト余積の存在
$`\KW{If we have } \Gamma, x:\sigma \mid \Xi, \varphi \vdash \psi\\
\KW{And } \Gamma \mid \Theta \vdash \exists x:\sigma. \varphi\\
\KW{Then using }\text{SOME-E}\\
\KW{We have } \Gamma \mid \Theta, \Xi \vdash \psi
%`$
SOME-I
ファイバー方向無限デカルト余積の余成分 $`M/x`$
$`\KW{If we have } \Gamma \mid \Theta \vdash \varphi[M/x]\\
\KW{And } M : \Gamma \vdash \sigma\\
\KW{Then using }\text{SOME-I}\\
\KW{We have } \Gamma \mid \Theta \vdash \exists x:\sigma. \varphi
%`$
ベース方向複圏構造の基礎
IDENTITY
ベース方向恒等射の存在
$`\KW{If we have nothing}\\
\KW{Then using }\text{IDENTITY}\\
\KW{We have } \Gamma, x:\sigma \to \sigma
%`$
MCOMP
ベース方向複結合の存在
$`\KW{If we have }\Gamma, x:\sigma, \Gamma' \to \tau\\
\KW{And } \Delta \to \sigma\\
\KW{Then using }\text{MCOMP}\\
\KW{We have } \Gamma, \Delta, \Gamma' \to \tau
%`$
DEL
ベース方向破棄射の存在
$`\KW{If we have }\Gamma \to \tau\\
\KW{Then using }\text{DEL}\\
\KW{We have } \Gamma, x:\sigma \to \tau
%`$
COPY
ベース方向コピー射の存在
$`\KW{If we have }\Gamma, x:\sigma, y:\sigma \to \tau\\
\KW{Then using }\text{COPY}\\
\KW{We have } \Gamma, x:\sigma \to \tau
%`$
SYMM
ベース方向対称射の存在
$`\KW{If we have }\Gamma, x:\sigma, y:\rho \to \tau\\
\KW{Then using }\text{SYMM}\\
\KW{We have } \Gamma, y:\rho, x:\sigma \to \tau
%`$
ベース方向複圏その他
FIN
ベース方向終射の存在
$`\KW{If we have nothing}\\
\KW{Then using }\text{FIN}\\
\KW{We have } \Gamma \to 1
%`$
INI
ベース方向始射の存在
$`\KW{If we have nothing}\\
\KW{Then using }\text{INI}\\
\KW{We have } \Gamma, x: 0 \to \tau
%`$
PROD
ベース方向デカルト積の存在
$`\KW{If we have } \Gamma \to \sigma\\
\KW{And } \Gamma \to \tau\\
\KW{Then using }\text{PROD}\\
\KW{We have } \Gamma \to \sigma \times \tau
%`$
PROJ1
ベース方向第一射影の存在
$`\KW{If we have } \Gamma \to \sigma \times \tau\\
\KW{Then using }\text{PROJ1}\\
\KW{We have } \Gamma \to \sigma
%`$
PROJ2
ベース方向第ニ射影の存在
$`\KW{If we have } \Gamma \to \sigma \times \tau\\
\KW{Then using }\text{PROJ2}\\
\KW{We have } \Gamma \to \tau
%`$
COPROD
ベース方向デカルト余積の存在
$`\KW{If we have } \Gamma, x:\sigma \to \rho\\
\KW{And } \Gamma, y:\tau \to \rho \\
\KW{Then using }\text{COPROD}\\
\KW{We have } \Gamma, z:(\sigma + \tau) \to \rho
%`$
INJ1
ベース方向第一入射の存在
$`\KW{If we have } \Gamma, z:(\sigma + \tau) \to \rho\\
\KW{Then using }\text{INJ1}\\
\KW{We have } \Gamma, x:\sigma \to \rho
%`$
INJ2
ベース方向第ニ入射の存在
$`\KW{If we have } \Gamma, z:(\sigma + \tau) \to \rho\\
\KW{Then using }\text{INJ1}\\
\KW{We have } \Gamma, y:\tau \to \rho
%`$
ABS
ベース方向カリー化
$`\KW{If we have } \Gamma, x:\sigma \to \tau\\
\KW{Then using }\text{ABS}\\
\KW{We have } \Gamma \to \sigma \Imp \tau
%`$
APP
ベース方向適用射の存在
$`\KW{If we have } \Gamma \to \sigma \Imp \tau\\
\KW{And } \Gamma \to \sigma\\
\KW{Then using }\text{APP}\\
\KW{We have } \Gamma \to \tau
%`$
*1:バーケダルは英語読み https://www.howtosay.co.in/pronounce/birkedal-in-english/ から。北欧の人名らしく、原音は https://www.howtopronounce.com/danish/birkedal または https://ja.howtopronounce.com/birkedal
*2:https://ja.howtopronounce.com/bizjak
*3:一部だけラベルを付けるでもかまいません。ここらへんは何でもありで自由です。
*4:"polymorphism" は「多相」と被る〈コンフリクトする〉のであまり使われません。
