Denotationale Semantik

Die denotationale Semantik interpretiert Programme als mathematische Objekte, typischerweise als Funktionen über strukturierten Domänen, und liefert eine kompositionelle und maschinenunabhängige Beschreibung der Bedeutung.

Definition

Die denotationale Semantik weist jedem Programm ein mathematisches Objekt (seine Denotation) zu, das kompositionell aus den Denotationen seiner Teile definiert wird, wobei die Rekursion über kleinste Fixpunkte in Domänen interpretiert wird.

Scope

Dieses Thema behandelt den Scott-Strachey-Ansatz, bei dem jede Programmphrase ein Element einer mathematischen Domäne bezeichnet. Es umfasst die Domänentheorie, vollständige partielle Ordnungen, stetige Funktionen und Least-Fixed-Point-Interpretationen der Rekursion sowie die vollständige Abstraktion, die sich damit befasst, wie genau die denotationale Bedeutung mit dem beobachtbaren Verhalten übereinstimmt.

Core questions

• Welche mathematischen Strukturen können beliebige Rekursion und Nicht-Terminierung modellieren?
• Wie wird Bedeutung kompositionell aus den Bedeutungen von Unterprogrammen aufgebaut?
• Was ist vollständige Abstraktion und warum ist sie schwer zu erreichen?
• Wie verhält sich die denotationale Bedeutung zum operationalen Verhalten?

Key theories

Domänentheorie und Fixpunktsemantik

Scotts Domänentheorie liefert geordnete Strukturen und stetige Funktionen, in denen rekursive Definitionen als kleinste Fixpunkte interpretiert werden, wodurch das Problem der Bedeutungsgebung für selbstreferenzielle Programme gelöst wird.

Vollständige Abstraktion

Plotkins Studie über LCF formulierte das Problem der vollständigen Abstraktion, ob die denotationale Gleichheit genau mit der Beobachtungsäquivalenz übereinstimmt, und deckte eine Lücke auf, die jahrzehntelange weitere Forschung motivierte.

Clinical relevance

Denotationale Modelle bieten eine präzise, kompositionelle Referenz für die Sprachbedeutung, unterstützen das Argumentieren über Programmäquivalenz und -optimierung und informieren das Design von Merkmalen wie Rekursion und Funktionen höherer Ordnung. Die Domänentheorie verbindet Programmiersprachen auch mit der breiteren Mathematik und Logik.

History

Stracheys Arbeit an mathematischen Beschreibungen von Sprachen und Scotts Konstruktion von Domänenmodellen im Jahr 1969 begründeten die denotationale Semantik, die in ihrem Papier von 1971 formalisiert wurde. Scotts Domänentheorie reifte in den 1970er Jahren, und Plotkins Analyse von LCF kristallisierte das Problem der vollständigen Abstraktion heraus, das spätere Entwicklungen wie die Spielsemantik vorantrieb.

Debates

Das Problem der vollständigen Abstraktion

Eine zentrale Frage ist, ob ein denotationales Modell das beobachtbare Verhalten einer Sprache genau erfassen kann, nicht mehr und nicht weniger; klassische Domänenmodelle versagen hierbei für sequentielle Sprachen höherer Ordnung, was alternative Modelle erforderlich macht.

Key figures

• Dana Scott
• Christopher Strachey
• Gordon Plotkin
• Glynn Winskel

Seminal works

• scott1971
• scott1976
• plotkin1977
• winskel1993

Frequently asked questions

Was ist eine Domäne in der denotationalen Semantik?

Eine Domäne ist eine mathematische Struktur, typischerweise eine partiell geordnete Menge mit Limiten von aufsteigenden Ketten, die einen Rahmen bietet, in dem rekursive und partielle Berechnungen als kleinste Fixpunkte stetiger Funktionen modelliert werden können.

Was ist vollständige Abstraktion?

Eine Semantik ist vollständig abstrakt, wenn zwei Programme genau dann dieselbe Denotation haben, wenn sie beobachtungsäquivalent sind, was bedeutet, dass das Modell weder verhaltensidentische Programme unterscheidet noch unterscheidbare Programme verwechselt.