「表示的意味論」の版間の差分

関係 <tt>x≤y</tt> は、<tt>x</tt> が <tt>y</tt> に計算的に発展する可能性があることを意味する。表示が完備半順序集合の要素ならば、例えば <tt>f≤g</tt> は <tt>f</tt> が定義されている全ての値について <tt>g</tt> と等しいことを意味する。

 

# ''下限の存在'': 領域には必ず <tt>⊥</tt> で表される要素が含まれ、領域内の任意の要素 <tt>x</tt> について <tt>⊥≤x</tt> が成り立つ。

# ''上限の存在'': 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、<math>\forall i \in \omega</math> <math>x_i \le x_{i+1}</math> としたとき、上限 <math>\vee_{i \in \omega} x_i</math> が存在する。これを <math>\omega</math>-完全と呼ぶ。

ヒューイットと Baker の論文には <tt>'''immediate-descendants'''_f</tt> の定義に小さな誤りがあったが、Will Clinger [1981] によって修正された。

-->

== 完全抽象化 ==

プログラムの表示的意味論と操作的意味論が合致するかどうかを論じる際に、完全抽象化の概念が関わってくる。完全抽象化の特徴は次の通りである。