Benutzer:DerSpezialist/Scott-Informationssystem

Ein Scott-Informationssystem oder kurz Informationssystem ist eine mathematische Struktur aus dem Gebiet der Breichstheorie. Sie werden in der konstruktiven Mathematik statt Scott-Jershow-Bereichen verwendet, um Datentypen zu modellieren. Man ordnet einem algebraischen Datentyp ein Informationssystem als dessen Interpretation zu.^[1]

Ein Informationssystem ist eine Struktur ${\displaystyle (A,\mathrm {Con} ,\vdash )}$ mit einer Menge ${\displaystyle A}$ von Informationsatomen oder Tokens, einer Menge ${\displaystyle \mathrm {Con} }$ von endlichen konsistenten Teilmengen von A und einer Folgerungsrelation ${\displaystyle \vdash }$ auf ${\displaystyle \mathrm {Con} }$ und ${\displaystyle A}$, die den folgenden Axiomen genügt:

• Die leere Menge und Einermengen sind konsistent: Es gilt ${\displaystyle \emptyset \in \mathrm {Con} }$ und ${\displaystyle \{a\}\in \mathrm {Con} }$ für alle ${\displaystyle a\in A}$.
• Konsistenz bleibt unter Teilmengen erhalten: Ist ${\displaystyle U\subset V\in \mathrm {Con} }$, so ist ${\displaystyle V\in \mathrm {Con} }$.
• Elemente können stets gefolgert werden: Ist ${\displaystyle a\in U\in \mathrm {Con} }$, so gilt ${\displaystyle U\vdash a}$.
• Konsistenz bleibt unter Folgerung erhalten: Aus ${\displaystyle U\vdash V}$ folgt ${\displaystyle U\cup V\in \mathrm {Con} }$.
• Folgerung ist transitiv: Aus ${\displaystyle U\vdash V\vdash a}$ folgt ${\displaystyle U\vdash a}$.

Dabei steht ${\displaystyle U\vdash V}$ für ${\displaystyle U\vdash b}$ für alle ${\displaystyle b\in V}$. Gilt ${\displaystyle U\vdash V}$ und ${\displaystyle U\dashv V}$, so sind ${\displaystyle U}$ und ${\displaystyle V}$ (folgerungs-)äquivalent, geschrieben ${\displaystyle U\sim V}$.

Gilt stets ${\displaystyle U\in \mathrm {Con} }$ genau dann, wenn ${\displaystyle \{a,b\}\in \mathrm {Con} }$ für alle ${\displaystyle a,b\in U}$, so heißt das Informationssystem kohärent.

Gilt stets ${\displaystyle U\vdash b}$ genau dann, wenn ${\displaystyle \{a\}\vdash b}$ für ein ${\displaystyle a\in U}$, so heißt das Informationssystem linear.

Betrachte das System der nichtleeren Teilmengen von natürlichen Zahlen. Eine Menge ${\displaystyle {\mathcal {N}}=\{N_{1},\dots ,N_{n}\}}$ gelte als konsistent, falls ${\displaystyle \textstyle \bigcap _{i=1}^{n}N_{i}}$ nichtleer ist und ${\displaystyle {\mathcal {N}}\vdash N}$ gelte, falls ${\displaystyle \textstyle \bigcap _{i=1}^{n}N_{i}\subset N}$. Diese erfüllt die Bedingungen für ein Informationssystem. Damit der Schnitt ${\displaystyle \textstyle \bigcap _{i=1}^{n}N_{i}}$ für ${\displaystyle n=0}$ wohlgeformt ist, setze ${\displaystyle \textstyle \bigcap \emptyset =\mathbb {N} }$.

Das Beispiel ist nicht kohärent, da ${\displaystyle {\mathcal {N}}_{1}=\{1,2\}}$, ${\displaystyle {\mathcal {N}}_{2}=\{2,3\}}$ und ${\displaystyle {\mathcal {N}}_{3}=\{3,4\}}$ paarweise, aber nicht gemeinsam konsistent sind (vgl. stochastische Unabhängigkeit).

Das Beispiel ist auch nicht linear, da ${\displaystyle \{2\mathbb {N} ,\mathbb {P} \}\vdash \{1,2\}}$, jedoch weder ${\displaystyle \{2\cdot \mathbb {N} \}\vdash \{1,2\}}$ noch ${\displaystyle \{\mathbb {P} \}\vdash \{1,2\}}$ gelten, wobei ${\displaystyle 2\cdot \mathbb {N} =\{2\cdot n|n\in \mathbb {N} \}}$ und ${\displaystyle \mathbb {P} =\{p\in \mathbb {N} |p{\text{ prim}}\}}$.

Auf Informationssystemen, die linear und kohärent sind, lassen sich Konsistenz und Folgerung durch binäre Prädikate auf Tokens ausdrücken.^[2] Eine Struktur ${\displaystyle (A,\asymp ,\succsim )}$ heiße eine quasigeorndete Toleranz, falls

• die Relation ${\displaystyle \asymp }$ eine Toleranz ist, also reflexiv und symmetrisch,
• die Relation ${\displaystyle \succsim }$ eine Quasi-Ordnung ist, also reflexiv und transitiv, und
• aus ${\displaystyle a\asymp b\succsim c}$ auch ${\displaystyle a\asymp c}$ folgt.

Die letzte Eigenschaft heißt auch Weitergabe von Konsistenz durch Ableitung. Sie gilt auch in allgemeinen Informationssystemen: Aus ${\displaystyle U\cup V\in \mathrm {Con} }$ und ${\displaystyle V\vdash W}$ folgt ${\displaystyle U\cup W\in \mathrm {Con} }$.

Man rekonstruiert aus einer quasigeordneten Toleranz ein lineares und kohärentes Informationssystem durch:

• Gelte ${\displaystyle U\in \mathrm {Con} }$, falls ${\displaystyle a\asymp b}$ für alle ${\displaystyle a,b\in U}$ gilt.
• Gelte ${\displaystyle U\vdash b}$, falls ${\displaystyle a\succsim b}$ für ein ${\displaystyle a\in U}$ gilt.

Umgekehrt kann jedes lineare und kohärente Informationssystem durch eine quasigeordnete Toleranz beschrieben werden. Allgemein kann man jedoch keine Halbordnung also ein antisymmetrisches ${\displaystyle \succsim }$ erwarten. Man kann Datentypen ohne Verlust auch durch quasigeordneten Toleranzen modellieren. Für diese Anwendung ist sogar möglich, die Relation ${\displaystyle \succsim }$ antisymmetrisch zu bekommen.^[2]

1. ↑ Helmut Schwichtenberg und Stanley S. Wainer: Proofs and Computations. Cambridge University Press, Cambridge 2012, ISBN 978-0-521-51769-0 (englisch). 
2. ↑ ^{a b} Basil A. Karádais: Normal forms, linearity, and prime algebraicity over nonflat domains. Mathematical Logic Quarterly, 2018, doi:10.1002/malq.201600020 (englisch).