完全抽象化

ウィキペディア小見出し辞書

完全抽象化

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/30 16:28 UTC 版)

「表示的意味論」の記事における「完全抽象化」の解説

プログラムの表示的意味論と操作的意味論が合致するかどうかを論じる際に、完全抽象化の概念が関わってくる。完全抽象化の特徴は次の通りである。 抽象性 表示的意味論は数学的構造によって形式化され、それはプログラミング言語の操作的意味論や表現とは独立している。 正当性 観測される動作が異なるプログラムは表示も異なる。 完全性 表示が異なるプログラムは観測される動作も異ならなければならない。 その他に表示的意味論と操作的意味論について保持するのが望ましい特徴は以下の通りである。 構築可能性 意味モデルは、直観的に構成可能な要素のみから構築可能であるべきである。形式的に表現すれば、全要素は有限要素の有向集合の上限でなければならない。 進歩性 各システム S について、その意味論には progressionS 関数が存在する。システム S の表示（意味）は、∨i∈ωprogressionSi(⊥S) であり、⊥S は s の初期構成である。 完全抽象性 意味モデルのあらゆる射はプログラムの表示であるべきである。 表示的意味論での長年の懸案は、再帰データ型のある場合の完全抽象化であった。特に再帰に利用可能な自然数型である。この問題は従来、PCF（プログラミング言語）（英語版）の意味論の構築の問題として捉えられてきた。1990年代、ゲーム意味論によって PCF の完全抽象モデルが構築され、表示的意味論の手法に根本的な変化をもたらした。