代数的意味論（コンピュータ科学）

代数仕様のシグネチャは、その形式的な構文を定義します。「シグネチャ」という言葉は、楽譜における「調号」の概念のように使われます。

署名は一連の${\displaystyle S}$ソートと呼ばれるデータ型のファミリー${\displaystyle \Sigma }$各セットには、ソートを関連付ける演算記号（または単に記号）を含む集合があります。${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$種類に関連する演算記号の集合を表す${\displaystyle s_{1},~s_{2},~...,~s_{n}\in S}$種類${\displaystyle s\in S}$。

例えば、整数スタックのシグネチャについては、2つのソートを定義します。${\displaystyle int}$そして${\displaystyle stack}$、および以下の演算記号群：

${\displaystyle {\begin{aligned}\Sigma _{\Lambda ,~stack}&=\{{\rm {new}}\}\\\S​​igma _{int~stack,~stack}&=\{{\rm {push}}\}\\\S​​igma _{stack,~stack}&=\{{\rm {pop}}\}\\\S​​igma _{stack,~int}&=\{{\rm {depth}},{\rm {top}}\}\\\end{aligned}}}$

どこ${\displaystyle \Lambda }$空文字列を表します。

代数​${\displaystyle A}$ソートと演算記号をセットと関数として解釈します。${\displaystyle s}$セットとして解釈される${\displaystyle A_{s}}$これは、${\displaystyle A}$ある種の${\displaystyle s}$、そして各シンボル${\displaystyle \sigma }$で${\displaystyle \Sigma _{s_{1}s_{2}...s_{n},~s}}$関数にマッピングされます${\displaystyle \sigma _{A}:A_{s_{1}}\times A_{s_{2}}\times ~...\times ~A_{s_{n}}}$これは、${\displaystyle A}$。

整数スタックのシグネチャに関して、ソートを解釈します${\displaystyle int}$セットとして${\displaystyle \mathbb {Z} }$整数のソートを解釈する${\displaystyle stack}$セットとして${\displaystyle Stack}$整数スタックの。さらに、演算記号のファミリーを以下の関数として解釈する。

${\displaystyle {\begin{aligned}{\rm {new}}&:~\to Stack\\{\rm {push}}&:~\mathbb {Z} \times Stack\to Stack\\{\rm {pop}}&:~Stack\to Stack\\{\rm {depth}}&:~Stack\to \mathbb {Z} \\{\rm {top}}&:~Stack\to \mathbb {Z} \\\end{aligned}}}$

代数仕様のセマンティクスは、条件方程式の形式の公理によって定義される。^{[ 1 ]}

整数スタックのシグネチャに関して、以下の公理が成り立つ。

いかなる場合でも${\displaystyle z\in \mathbb {Z} }$そして${\displaystyle s\in Stack}$、

${\displaystyle {\begin{aligned}&A1:~~{\rm {pop}}({\rm {push}}(z,s))=s\\&A2:~~{\rm {depth}}({\rm {push}}(z,s))={\rm {depth}}(s)+1\\&A3:~~{\rm {top}}({\rm {push}}(z,s))=z\\&A4:~~{\rm {pop}}({\rm {new}})={\rm {new}}\\&A5:~~{\rm {depth}}({\rm {new}})=0\\&A6:~~{\rm {top}}(s)=-404~{\rm {if~depth}}(s)=0\\\end{aligned}}}$

どこ "${\displaystyle -404}$「」は「見つかりません」を示します。

仕様の数学的意味論（指示的意味論とも呼ばれる）^{[ 5 ]は、その数学的意味を指します。}

代数仕様の数学的意味論は、その仕様を満たすすべての代数のクラスである。特に、Goguen らによる古典的なアプローチ^{[ 1 ] [ 2 ]}では、初期代数(同型を除いて一意) を代数仕様の「最も代表的な」モデルとして採用している。

仕様の操作的意味論[ ^{6 ]と}は、それを計算手順のシーケンスとしてどのように解釈するかを意味する。

基底項とは、変数を含まない代数式と定義する。代数仕様の操作的意味論とは、与えられた等式公理を左から右への書き換え規則として使用し、基底項が正規形（それ以上書き換えが不可能な状態）に達するまで、どのように変換できるかを示すものである。

整数スタックの公理を考えてみましょう。${\displaystyle \Rrightarrow }$「 」は「 への書き換え」を表します。

${\displaystyle {\begin{aligned}&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {pop}}({\rm {new}})))))))&\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {pop}}({\rm {push}}(1,~{\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))))&({\rm {by~Axiom~}}A4)\\\Rrightarrow ~&{\rm {top}}({\rm {pop}}({\rm {push}}(2,~{\rm {push}}(3,~{\rm {new}}))))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&{\rm {top}}({\rm {push}}(3,~{\rm {new}}))&({\rm {by~Axiom~}}A1)\\\Rrightarrow ~&3&({\rm {by~Axiom~}}A3)\\\end{aligned}}}$

代数仕様は、任意の基底項を書き換えても常に同じ正規形になる場合、合流性（チャーチ・ロッサーとも呼ばれる）であると言われます。任意の基底項を書き換えても有限ステップで正規形になる場合、それは停止性であると言われます。代数仕様は、合流性と停止性の両方を満たす場合、正準性（収束性とも呼ばれる）であると言われます。言い換えれば、任意の基底項を書き換えても有限ステップで一意の正規形になる場合、それは正準性であると言えます。

任意の標準的な代数仕様が与えられれば、数学的意味論は操作的意味論と一致する。^{[ 7 ]}

その結果、プログラムの正当性に関する問題に対処するために、正規代数仕様が広く適用されてきた。例えば、多くの研究者が、オブジェクト指向プログラミングにおけるオブジェクトの観測的等価性のテストにこのような仕様を適用している。 1981年から2013年までの主要な研究の歴史的概観を提供する二次資料として、ChenとTse ^{[ 8 ]を参照されたい。}