Difference between revisions 138950849 and 138956657 on dewiki

Die '''Bereichstheorie''' ist ein ''Zweig der Mathematik'' und dient auf dem Gebiet der [[Theoretische Informatik|theoretischen Informatik]] zum mathematischen Nachweis der korrekten Funktionalität (Wirkungsweise) von Computerprogrammen [[Formale Semantik|(formale Semantik)]] bzw. zum Nachweis von Programmier- und Spezifikationssprachen [[denotationelle Semantik|(denotationelle Semantik)]]. Die Bereichstheorie kann ebenso als ein Teilgebiet der [[Ordnungstheorie]] betrachtet werden.

Konkret kann man mit Hilfe der Bereichstheorie die Wirkungsweise eines Computerprogrammes im Zusammenhang mit einer formalen Programmiersprache berechnen. Die [[formale Sprache]] dient hierbei als mathematisches Modell für eine echte Programmiersprache. Somit kann die Wirkungsweise eines Computerprogramms mit Hilfe der formalen und denotationellen Semantik beschrieben werden. [[Korrektheitsbeweis|(Korrektheitsbeweise).]]

== Motivation und Formulierung ==  
Die primäre Motivation für die Initiierung der Bereichstheorie erfolgte in den späten 1960er Jahren durch den amerikanischen Mathematiker und Informatiker [[Dana Stewart Scott]], im Zuge seiner Suche nach der denotationellen Semantik (Funktionensemantik) des [[Lambda-Kalkül|Lambda-Kalküls]]. [[File:Greek lc lamda thin.svg|mini|120px|Symbol für den [[Lambda]]-Kalkül]]Der Lambda-Kalkül ist ebenso eine formale Sprache zur Untersuchung von Funktionen und beschreibt Funktionsdefinitionen, das dDefinieren formaler Parameter sowie das Auswerten und Einsetzen aktueller Parameter. Strukturell gesehen, kann man bezugnehmend auf dasen Lambda  -Kalkül von [[Einfache Funktion|einfachen Funktionen]] ausgehen. Das bedeutet, es handelt sich um Funktionen, die wiederum andere Funktionen und deren Eingabeargumente übernehmen. Unter Berücksichtigung dieser einfachen Funktionen erhält man formale Parameter, sogenannte Fixpunktkombinatoren (der bekannteste ist der ''Y-Kombinator''). 

Um nun eine entsprechende Funktionensemantik zu formulieren, könnte man zunächst versuchen, ein Modell für den Lambda-Kalkül zu konstruieren, in dem eine tatsächliche Funktion ohne freie Variablen (Lambda-Term) assoziiert ist, zu konstruieren. Man würde dadurch einen sogenanntesn Kombinator-Kalkül erhalten. Jedoch wären die Elemente eines solch erhaltenen Kombinator-Kalküls Funktionen aus Funktionen zu Funktionen. Sie können also nicht tatsächlich, wirkliche Funktionen sein, sondern lediglich Teilfunktionen. Folglich würde man nur „teilweise“ oder „unvollständige“ Informationen erhalten.

Diesesr Kombinator-Kalkül [[Kombinatorische Logik|(Kombinatorische Logik)]] kann aber in weiterer Folge als alternativer Ansatz zum Lambda-Kalkül gesehen werden.

== Berechnung und Modellierung == 
Um nicht nur ''"teilweise"'' oder ''"unvollständige"'' Informationen zu erhalten und zu einem tatsächlichen Ergebnis zu gelangen muss man bei der Berechnung (Modellierung) folgende Variablen berücksichtigen:

(contracted; show full)
* [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.903 ''Domain Theory (1994) by Samson Abramsky''] - 16.Februar 2015 (englisch)
* [http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf ''Domain Theory - Corrected and expanded version''] - 16.Februar 2015 (PDF, 1.06 MB)

[[Kategorie:Mathematischer Grundbegriff]]
[[Kategorie:Ordnungstheorie]]