矢印のオーバーロードがひどい件： 所感

「矢印の混乱に対処する： デカルト閉圏のための記法」より：

一番ポピュラーな矢印記号である「$`\to`$」は、圏の射のプロファイル（域と余域の仕様）の区切り記号に独占的に使わせていただきます。

これはもちろん、僕の私的提案、つうか願望であって、矢印とかコロンのような使い勝手が良い記号は争奪戦になります。記号の使用に独占権はないので、結局は、異なる意味でオーバーロードになるのは必然です。しょうがない。

しょうがないのだけど、次のような区別は（何らかの方法で）して欲しい！

1. 平叙文〈declarative sentence〉と疑問文〈interrogative sentence〉は区別すべき。
2. プロファイルと値割り当て〈value assignment〉は区別すべき。
3. 評価演算子〈evaluation operator〉と結合的適用〈compositional application〉は区別すべき。

順番に補足説明をすると；$`\newcommand{\Ev}{\triangleleft}
\newcommand{\mrm}[1]{\mathrm{#1} }`$

平叙文 vs. 疑問文

$`A, B, C`$ が命題だとして、ターンスタイル記号 $`\vdash`$ はメタ命題の記述に使います。

$`\quad A, B \vdash C`$

これは、「$`A, B`$ を前提とすれば、$`C`$ が成立する」というメタな命題の表現です。事実の主張と言ってもいいでしょう。

それに対して、「$`A, B`$ を前提として、$`C`$ は成立しますか？」という疑問文は全然別です。疑問文は、質問文、問い合わせ文、問題文とか言っても同じです。ときに、「$`A, B`$ を前提として、$`C`$ が成立するかどうか考えなさい」とか「$`A, B`$ を前提として、$`C`$ が成立することを示しなさい」と命令口調が入るかも知れません。だとしても、事実の主張とは全然違います。

僕が $`\vdash?`$ という記号を提案するのは、「事実の主張と、質問を同じ構文で書くのはやめてくれ」と強く思うからです。（「メタ疑問文の書き方」参照。）

プロファイル vs. 値割り当て

関数を定義するとき、プロファイル（域と余域の仕様）と実際の計算法を分けて書いてみます。例えば：

$`\quad f:{\bf R}\times {\bf R} \to {\bf R}\\
\qquad x, y\mapsto x^2 + xy + 1`$

1行目がプロファイルの宣言で、2行目が計算法を示す値割り当てです。プロファイルの矢印は $`\to`$ で、値割り当ての矢印は $`\mapsto`$ です。

プロファイルと値割り当てをまとめて書くと：

$`\quad f:= ( x:{\bf R}, y:{\bf R} \mapsto x^2 + xy + 1 \;: {\bf R})`$

型判断と同じ形です。型判断は型付きの関数定義と同じことです。

もっとも型判断は、型付け〈typing〉を命題とみなして「事実の主張」をしているメタ命題とも解釈できるので、ターンスタイル記号 $`\vdash`$ を使うのも見当違いではありません。ただし、$`\vdash`$ を使う文脈と使用法が重要で、値割り当てなのかプロファイルなのか事実の主張なのか質問文なのか、なんだか分からない使い方は迷惑です。

評価演算子 vs. 結合的適用

ラムダ計算では、適用は単なる併置か、または空白が演算子記号に使われます。$`f\; a`$ の形です。が、これは「最も頻繁に使われる演算子は省略する」規則の事例です。評価演算子の明示的な記号を仮に $`\Ev`$ としましょう。$`f\; a`$ は次の省略形です。

$`\quad f\Ev a`$

中置演算子記号を前置の関数記号に直せば：

$`\quad f\Ev a = \mrm{ev}(f, a)`$

では、伝統的な適用の記法である丸括弧を使った $`g(x)`$ の意味はなんでしょう。これは、$`x;g`$ あるいは $`g\circ x`$ の別記法です。「$`x`$ は要素のはずだ」と思うかも知れませんが、集合の要素 $`x\in X`$ は、ポインティング写像 $`x:{\bf 1}\to X\text{ in }{\bf Set}`$ と同一視可能なので、$`g(x) = g\circ x = x;g`$ と見て差し支えありません。伝統的適用は射の結合です。

$`\mrm{ev}(f, a)`$ という書き方は、$`\mrm{ev}\circ \langle f, a\rangle`$ のことです。ここで：

• $`f: {\bf 1} \to [X \to Y]`$
• $`a: {\bf 1} \to X`$
• $`\langle f, a\rangle : {\bf 1}\to [X \to Y]\times X`$
• $`\mrm{ev} : [X \to Y]\times X \to Y`$

$`f`$ が $`F:X \to Y`$ のカリー化なら、次のベータ変換の等式が成立します。

$`\quad \mrm{ev}(f, a) = F(a)`$

同じことですが：

$`\mrm{ev}\circ \langle f, a\rangle = F\circ a`$

最後に「矢印の混乱に対処する： デカルト閉圏のための記法」よりもうひとつ引用：

僕やあなたが悪いとは限らない：

• 説明がうまくいかないときは用語法が悪いのかも知れない。
• 計算がうまくいかないときは記法が悪いのかも知れない。