指標フラグメントを利用した記法

指標テレスコープがあるとする。$`\newcommand{\Within}{\sqsubseteq}
\newcommand{\conc}{\mathop{\#} }
\newcommand{\dmid}{\mathrel{\|} }
%`$

$`\quad \Sigma_1 \Within \Sigma_2 \Within \cdots \Within \Sigma_n`$

それ自身が指標でなくても、なんらかの指標を前置して指標が得られる構文的対象物〈syntactic object〉を指標フラグメントと呼ぶ。実際の記述では指標フラグメントは頻繁に利用する。指標フラグメントを書けないなら差分記述のありがたみが無くなる。

指標フラグメントを $`\Phi, \Phi_1, \Psi`$ のように書くことにして、指標や指標フラグメントの連接は $`\conc`$ で書く。先の指標テレスコープは次のように書ける。

$`\quad \Sigma_1 \Within \Sigma_1\conc\Phi_1 \Within \cdots \Within \Sigma_1\conc\Phi_1\conc \cdots \conc \Phi_n`$

次の記法を使う。

$`\quad (\Delta \Within \Sigma) = (\Delta \mid \Phi)\\
\text{where }\\
\quad \Phi = \Sigma\setminus \Delta
`$

同じことは次のようにも書ける。

$`\quad (\Delta \mid \Phi) = (\Delta \Within \Sigma) \\
\text{where }\\
\quad \Sigma = \Delta \conc \Phi
`$

手続きのプロファイルを書くとき次を使う。

$`\quad \Sigma \dmid \Phi \to \Psi`$

これは次の略記、二重縦棒は、その左側を余域側にもコピーすると考える。

$`\quad \Sigma \mid \Phi \to \Sigma \mid \Psi`$

だが、$`\Sigma \to \Sigma`$ 部分が恒等なので省略している。とにかく、省略が話を分からなくしている!