指標〈signature〉と呼ばれる構文的形式は、数学ならば公理系の記述に使われます。例えば、群の公理系とか可換環の公理系とかを指標で書けます。ソフトウェア／プログラミング分野の言葉で言うなら、指標はインターフェイスです。
インターフェイスには、それを決めた人（設計者／策定者）がいます。インターフェイスの利用者とインターフェイスの実装者もいます（別人とは限らず同一人物のこともあります）。立場・役割りとして、設計者・利用者・実装者があるのです。
設計者・利用者・実装者という立場・役割りが存在することは、一般的な指標でも同様です。設計者・利用者・実装者それぞれの、異なる視点を理解しないで指標を見ていると、ボンヤリとした印象しか持てないでしょう。指標に向かい合うとき、自分は今どの立場・役割りから指標を見ているのかを強く意識しましょう。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\hyp}{\text{－} }
\newcommand{\In}{ \text{ in } }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\ot}{\leftarrow}
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Ent}{ \sqsubseteq }
%\newcommand{\hinfer}{ \rightrightarrows }% horizontal meta rule (infer)
%\newcommand{\vinfer}{ \downdownarrows }% vertical meta rule (infer)
%%
%\require{color} % Using
%\newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name
%\newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression
\newcommand{\T}[1]{\text{#1} }
`$
内容：
指標の構文
簡単な指標の事例を挙げます。
$`\T{signature }\T{Succ} \:\{\\
\quad \T{sort }U \\
\quad \T{operation }i : \mbf{1} \to U\\
\quad \T{operation }s : U \to U\\
\}`$
$`\T{Succ}`$ は、successor〈後者〉関数を持つ集合といったつもりからです。もっとも、後者関数 $`s`$ 以外に初期状態 $`i`$ も持ってますが。
指標に対する具体例を、その指標のモデル〈model〉といいます。上の指標 $`\T{Succ}`$ のモデルを挙げましょう。
$`\quad (\\
\qquad U := \mbf{N}\, ,\\
\qquad i := \lambda\, ().\,0 \, ,\\
\qquad s := \lambda\, (n\in \mbf{N}).\,n + 1\\
\quad )
`$
自然数の集合を台集合〈underlying set〉とするモデルです。
指標の構文は人により場合により千差万別です。上の指標 $`\T{Succ}`$ を、プログラミングっぽく次のように書くかも知れません。
$`\T{interface }\T{Succ} \:\{\\
\quad \T{type }U \\
\quad \T{function }i : \mbf{1} \to U\\
\quad \T{function }s : U \to U\\
\}`$
僕の好みを言えば、圏論的意味論をダイレクトに示唆する、以下のような構文が好きです。
$`\T{signature }\T{Succ} \:\{\\
\quad \T{0-mor }U \In \mbf{Set}\\
\quad \T{1-mor }i : \mbf{1} \to U \In \mbf{Set}\\
\quad \T{1-mor }s : U \to U \In \mbf{Set}\\
\}`$
0-射（0-mor と略記）は圏の対象で、1-射（1-mor と略記）は圏の射です。コロンの個数で射の次元は分かるので、宣言の先頭のキーワードは無くてもいいです。
$`\T{signature }\T{Succ} \:\{\\
\quad U \In \mbf{Set}\\
\quad i : \mbf{1} \to U \In \mbf{Set}\\
\quad s : U \to U \In \mbf{Set}\\
\}`$
指標の事例をもっと見たいなら、以下の過去記事を参照してください。
型理論では、違った用語と構文を使います。「GAT〈ガット〉の構文： スターリングの論文から」で紹介したスターリング風の構文なら次のようです。
$`\T{signature }\T{Succ} \:\{\\
\quad \T{sort }U : () \vdash \mbf{Sort} \\
\quad \T{operation }i : () \vdash U()\\
\quad \T{operation }s : (x :U() ) \vdash U()\\
\}`$
スターリングの構文に実用性を持たせる案は「実用になる型理論の記法」に書いています。
数式部分にLaTeX記法を使うのは致し方ないですが、プレーンテキストで済む部分はプレーンテキストで書く構文については「曖昧性を減らす： Diag構成を事例として // 指標の書き方」で述べています。
構文のバラエティは実にまったくウンザリしますが、どうでもいい書き方の違いを無視すれば、指標は宣言を並べたリストです。各宣言は原則として名前で識別できます。その名前は、ソート名〈型名〉、オペレーション名〈関数名〉、等式名などと解釈できます。名前が付いてなくても順番で識別できます； 「4番目に出現した等式」のように。
宣言により記述されるコトは、名前で指されるモノの種類や居住地〈アビタ | habitat〉の情報で、モノを特定する情報ではありません（名前は固有名詞とはならない）。つまり、名前で指されるモノをプロファイリングしているのです。よって、宣言に指定される情報をプロファイル〈profile〉ともいいます。
意味論的なことを一言添えると（まー、余談だね）； 指標のモデルの全体は多くの場合、自動的に圏になります。例えば、指標 $`\T{Succ}`$ のモデルを対象とする圏 $`\mrm{Model}(\T{Succ})`$ ができます。$`\mrm{Model}(\T{Succ})`$ の始対象は、我々が直感的に捉えている自然数〈natural number object〉になります。指標の“意味”を、モデル達の圏の始対象だと定義する意味論は始対象意味論〈initial object semantics〉といいます。
指標と立場・役割り
指標を表すのに、ギリシャ文字大文字を使うのが習慣です。その習慣に従い、$`\Sigma, \Psi, \Phi`$ などで指標〈公理系 | インターフェイス〉を表すことにします。
指標自体は構文的対象物〈syntactic object〉で、それだけでは意味も意義も持ちません。無味無臭で、文字通り味気ない“書かれたモノ”に過ぎません。指標の周辺に居る人々を考えることにより、指標に意味や意義が与えられます。
指標を最初に作り出して、それに（必要なら）意味を与える人を、指標の設計者〈designer〉または策定者〈formulator〉と呼ぶことにします。
設計者により作られた指標 $`\Sigma`$ には、利用者〈user〉がいます。$`\Sigma`$ を使って／もとにして、さらに新しい何かを作ろうとする人々です。一方、指標にモデルを与えようとする人々もいます -- 指標の実装者〈implementer〉と呼びましょう。
例えば、指標 $`\T{Succ}`$ の利用者Aさんは、$`\T{Succ}`$ が提供するソート〈型〉とオペレーション〈関数〉を使って、新しい関係（二項述語）を定義するかも知れません。
$`\T{define }\T{isNextOf} := \lambda\, (y, x\in U).\, y = s(x)`$
実装者Bさんは、指標 $`\T{Succ}`$ に対して次のようなモデル〈実装 | 具体例〉を定義するかも知れません。
$`\quad (\\
\qquad U := \{0, 1\} \, ,\\
\qquad i := \lambda\, ().\,0 \, ,\\
\qquad s := \lambda\, (s\in \{0, 1\}).\, \T{if } s = 0 \T{ then } 1 \T{ else } 0\\
\quad )
`$
Bさんのモデル〈実装 | 具体例〉に対して、Aさんが定義した $`\T{isNextOf}`$ を適用すると、次の論理式は成立します。
$`\quad \T{isNextOf}(0, 1)`$
「$`0`$ は $`1`$ の次」となります。それを知ったAさんは「いや、思ってたのと違う」と言うかも知れません。が、Bさんに何らかの落ち度があるわけじゃないです。Bさんは、ちゃんと指標 $`\T{Succ}`$ のモデル〈実装 | 具体例〉を作ってますから。
もし、Aさんが文句を付けるなら、指標 $`\T{Succ}`$ の設計者に言うべきでしょう。あるいは自分で 指標 $`\T{Succ}`$ を変更すべきです。例えば次のように*1：
$`\T{signature }\T{Succ} \:\{\\
\quad \T{sort }U \In \mbf{Set}\\
\quad \T{operation }i : \mbf{1} \to U \In \mbf{Set}\\
\quad \T{operation }s : U \to U \In \mbf{Set}\\
\quad \T{law }\T{i_is_not_next} : \top \to (\forall x\in U.\, s(x) \ne i) \In \mbf{Logic} \\
\}`$
ここで出てきた $`\mbf{Logic}`$ （圏の固有名です）が気になるなら、以下の過去記事を参照してください。
手っ取り早く解釈したいなら、二値ブーリアンの順序集合 $`\mbf{B}`$ を圏だとみなして、次のように思えばいいです。キーワード $`\T{law}`$ はお気持ち表明なので無視していいです。
$`\quad \T{law }\T{i_is_not_next} : 1 \to (\forall x\in U.\, s(x) \ne i) \In \mbf{B}`$
立場・役割りの明示
ひとつの指標 $`\Sigma`$ に対して、設計者・利用者・実装者は、それぞれに違った立場から違った態度を取ることになります。今自分が、どの立場・役割りから指標〈公理系 | インターフェイス〉を見ているのかを意識しないと、指標に対する態度がボンヤリしたものとなり、指標を理解することも使いこなすことも出来ません。自分が何をしているか分からなくなったり、前提と結論が混乱しグチャグチャになります。自分の立場・役割りを意識し続けましょう。
自分の立場 -- 自分と指標との関係性を明示的に表現するための書き方を準備します。それは短い文です。主語として一人称 We を使うとして、次の形があります。
- We can use $`\Sigma`$ （自分達は利用者の立場・役割りである）
- We should implement $`\Sigma`$ （自分達は実装者の立場・役割りである）
例えば、前節の利用者Aさんの場合ならば、Aさんは指標 $`\T{Succ}`$ の利用者であり、$`\T{Succ}`$ に基づいて新しい関係〈二項述語〉を定義したので、立場・役割りを明示した書き方は次のようになります。
$`\T{We can use }\T{Succ}\\
\T{We define }\T{isNextOf} := \lambda\, (y, x\in U).\, y = s(x)
`$
実装者Bさんの場合ならば：
$`\T{We should implement }\T{Succ}\\
\T{We define example }\T{Toggle} \text{ of Succ} := \\
\quad (\\
\qquad U := \{0, 1\} \, ,\\
\qquad i := \lambda\, ().\,0 \, ,\\
\qquad s := \lambda\, (s\in \{0, 1\}).\, \T{if } s = 0 \T{ then } 1 \T{ else } 0\\
\quad )
`$
$`\T{We can use}`$ は指標を仮定〈前提〉することを表明しているので、$`\T{assume}`$ でもいいでしょう。
$`\T{We assume }\T{Succ}\\
\T{We define }\T{isNextOf} := \lambda\, (y, x\in U).\, y = s(x)
`$
その他、キーワードの選び方とか文の書き方とかは、好みや拘りがあるかも知れませんが、別に書き方なんてどうでもよくて、指標に対する自分の立場・役割りを明示的に書こう、と言いたいのです。
「そんなのイチイチ書かなくても、ちゃんと意識しているから大丈夫」というなら、もちろん書かなくていいです。「自分が何をしているか分からなくなる、前提と結論が混乱してしまう」人はお試しください、ということです。
指標の階層〈レイヤー〉
指標 $`\Sigma`$ と、その設計者・利用者・実装者を、次のように図示することにしましょう。
$`\begin{matrix}
& \mrm{Designer} & \\
\mrm{User}\ot & \Sigma & \ot\mrm{Implementer}
\end{matrix}
`$
利用者と実装者は、指標 $`\Sigma`$ を境界面（文字通りインターフェイス）として仕切られます。
例えば、$`\Sigma`$ がWeb APIだとしましょう。Web API だろうが何だろうが、インターフェイスは指標の形式で書けます。API利用者は、HTTPプロトコル上のREST形式で利用するとか、そういう技術的な話はあるかもしれませんが、要するに、$`\Sigma`$ で記述された仕様に従ってAPIを呼び出して利用します。
Web API $`\Sigma`$ が、サーバー側でPythonで実装されているとしましょう。$`\Sigma`$ の実装のために、Pythonライブラリを利用するとします。そのライブラリのインターフェイス仕様（つまり指標）は $`\Psi`$ としましょう。すると、$`\Sigma`$ の実装者は $`\Psi`$ の利用者になります。
$`\begin{matrix}
& \mrm{Designer} & & &\\
\mrm{User}\ot & \Sigma & \ot\mrm{Implementer}& \mrm{Designer}& \\
& & \mrm{User}\ot & \Psi & \ot\mrm{Implementer}
\end{matrix}
`$
ある指標の実装者は、別な指標の利用者になり得るわけです。
ソフトウェア／プログラミングでは、指標 $`\Psi`$ は $`\Sigma`$ より“低水準”と言ったりしますが、語感がよろしくない*2ので、ここでは基盤的〈underpinning〉ということにします。$`\Sigma`$ は応用的〈applicative〉です。
つまり、幾つかの指標が、基盤的なものから応用的なものへと積み重ねられて階層〈レイヤー〉構造を形成することがあります。
数学の例を出すならば、指標 $`\T{Succ}`$ にいくつかの法則〈条件〉を追加すると、自然数に関するペアノの公理系になります。ペアノの公理系では、足し算さえ定義されていません。基盤的なペアノの公理系の上に、足し算・掛け算・全順序などを定義して、全順序半環〈totally ordered semiring〉の指標に対する（ペアノの公理系に相対的な）実装を構成できます。全順序半環を仮定すれば、通常の算術はできます。全順序半環の指標〈公理系〉の利用者は、足し算・掛け算・全順序を利用して、より高度な関数や定理を実装することが出来ます。
単純にレイヤーを積み上げるだけではなくて、より複雑な、有向グラフで表現できるような形でたくさんの指標達を編成することもあります。
気持ち・心構えも形式化する
「We can use …」「We should implement …」「We define …」のような文言は、通常は地の文として書かれます。実際は、地の文としてさえ書かれなくて、流れや文脈に意図が隠されているかも知れません。
「We can use …」「We should implement …」「We define …」などは、指標・宣言・定義などに向き合うときの気持ち・心構えを明示的に提示して、気持ち・心構えを変えるべきタイミングを教えてくれます。形式的に書かれた記述のなかでも、気持ち・心構えは頻繁にチェンジします。このチェンジが誰でもいつでもうまくいくとは限らないので、形式的な記述の一部として、気持ち・心構えの切り替えヒントを入れるのは望ましいと思います。
例えば、証明すべきターゲット命題は論理式による宣言として書けます。見た目は公理系の法則と区別ができません。単なる論理式 $`\varphi`$ ではなくて、We should prove $`\varphi`$ と書けば、そこで証明責務が発生したことが分かります。また、練習問題を提示する形式として「You should define …」や「You should prove …」が使えるでしょう。
自然言語の文では、平叙文、疑問文、命令文の区別があるのに、形式的記述ではそれらの区別が表現できなくて困ることがあります。形式的表現であるラムダ項や論理式にはコミュニケーションを正確にする効能がありますが、気持ち・心構えの切り替えヒントを書いたり、疑問文・命令文を提示したりするには表現力が不足です。形式的表現の幅をもう少し広げたいところです。
