論理、型理論、圏論において、用語・記法のコンフリクト〈競合 | かち合い〉がひどすぎてホトホト困っている、という話は過去に何度もしています。以下の過去記事に、事情や愚痴を書いています。
特に気になるのが次のコンフリクトです。$`\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow}
\newcommand{\BR}[1]{ \big[\!\big[ {#1} \big]\!\big] } % BRacket
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\In}{\text{ in } }
`$
- 矢印記号 '$`\to`$'
- 圏論の射のプロファイル（域と余域）の区切り記号
- 論理のシーケントの区切り記号
- 型理論（むしろ、関数型言語だが）の関数空間型〈指数型〉を作る型形成〈type former〉記号
- 二重矢印記号 '$`\twoto`$'
- 圏論の2-射のプロファイル
- 論理の含意記号
- コロン '$`:`$'
- 圏論のプロファイル宣言の区切り記号
- 型理論の居住関係〈inhabitation relation〉の関係記号
- ターンスタイル記号 '$`\vdash`$'
- 論理の証明可能性を表す記号
- 型理論の型判断形式の区切り記号
これらに関して、次のように調停することにしました。
- 矢印記号 '$`\to`$' ： 関数型〈指数型〉の型形成記号は、裸の '$`\to`$' ではなくて、$`[\hyp \to \hyp]`$ を使う。射のプロファイルとシーケントのコンフリクトは実害が少ないのでそのまま。
- 二重矢印記号 '$`\twoto`$' ： 原則そのままとするが、含意記号は $`[\hyp \twoto \hyp]`$ または $`(\hyp \twoto \hyp)`$ を推奨。
- コロン '$`:`$' ： 混乱しそうな場合は、型理論の居住関係は $`\hat{:}`$ とする。型理論の文脈では普通のコロンでかまわない。
- ターンスタイル記号 '$`\vdash`$' ： 論理の証明可能性は $`\Vdash`$ に変更する。
$`f:A \to B`$ が型理論の宣言である場合、圏論の記法と混同しそうなときは
$`\quad f\mathrel{\hat{:}} [A \to B]`$
とします。これをデカルト閉圏 $`\cat{C}`$ で解釈すると：
$`\quad \BR{f} : \mathbf{1} \to [\BR{A}, \BR{B}] \In \cat{C}`$
微妙に違ってきます。この微妙な違いがうまく表現できないと困るので、上記のように調停したいのです。
ターンスタイル記号 '$`\vdash`$' に関しては、論理のほうが古くからこの記号を使用してきたと思いますが、型理論でのターンスタイルの使用があまりに激しいので、致し方なく '$`\vdash`$' は型理論に譲って、論理では '$`\Vdash`$' を使うことにします。
上記の調停案は、一定期間は実際に使ってみての案です。これで決まり、ということではないですが、ある程度はうまくいくだろうと思っています。
