1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
|
\documentclass[a4paper]{article}
\usepackage[dutch]{babel}
\usepackage[hidelinks]{hyperref}
\usepackage[margin=28mm,bottom=32mm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{graphicx}
\usepackage{fancyhdr}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\fancyhead{}
\fancyfoot[C]{Copyright {\textcopyright} 2015 Camil Staps}
\pagestyle{fancy}
% http://tex.stackexchange.com/a/86355/23992 maxwidth for includegraphics
\makeatletter
\def\maxwidth#1{\ifdim\Gin@nat@width>#1 #1\else\Gin@nat@width\fi}
\makeatother
\addto\extrasdutch{%
\renewcommand{\figureautorefname}{Figuur}%
}
\usepackage{amssymb}
\let\emptyset\varnothing
\usepackage{amsmath}
\usepackage{stmaryrd}
\newcommand\isdef{:=}
\newcommand\Val[1]{\mathsf{Val}\left\llbracket#1\right\rrbracket}
\DeclareMathOperator{\Base}{Base}
\DeclareMathOperator{\Elt}{Elt}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Gen}{Gen}
\DeclareMathOperator{\Dom}{Dom}
\DeclareMathOperator{\Fact}{Fact}
\DeclareMathOperator{\Schema}{Schema}
\DeclareMathOperator{\Pop}{Pop}
\DeclareMathOperator{\POP}{POP}
\DeclareMathOperator{\GlobObjPop}{GlobObjPop}
\DeclareMathOperator{\GlobAtomPop}{GlobAtomPop}
\DeclareMathOperator{\LocObjPop}{LocObjPop}
\DeclareMathOperator{\LocAtomPop}{LocAtomPop}
\DeclareMathOperator{\cstrsub}{subset}
\DeclareMathOperator{\cstreq}{equal}
\DeclareMathOperator{\cstrexcl}{exclusion}
\DeclareMathOperator{\cstruniq}{unique}
\DeclareMathOperator{\cstrtot}{total}
% Sans serif operators; http://tex.stackexchange.com/a/43135/23992
\DeclareSymbolFont{sfoperators}{OT1}{cmss}{m}{n}
\DeclareSymbolFontAlphabet{\mathsf}{sfoperators}
\makeatletter
\def\operator@font{\mathgroup\symsfoperators}
\makeatother
% new line after comma in math mode, see http://tex.stackexchange.com/a/1960/23992
\makeatletter
\def\old@comma{,}
\catcode`\,=13
\def,{%
\ifmmode%
\old@comma\discretionary{}{}{}%
\else%
\old@comma%
\fi%
}
\makeatother
\title{Werkstuk Informatiesystemen} %todo working title
\author{Camil Staps}
\begin{document}
\maketitle
\thispagestyle{fancy}
\begin{abstract}
%todo
\end{abstract}
%\section{Simpele typen}
%Laten we allereerst bekijken hoe makkelijk simpele typen werken.
%
%\begin{exmp}[Labels, simpele entiteiten en feiten]
% Een voorbeeld voor deze simpele typen is overal in de IMDb te vinden. Hier bekijken we nieuwsberichten.
%
% We definiëren de volgende verzamelingen:
%
% \begin{itemize}
% \item $\mathcal E \isdef \{\mathsf{Artikel}, \mathsf{Bron}, \mathsf{Film}\}$.
% \item $\mathcal L \isdef \{\mathsf{URL}, \mathsf{Inhoud}, \mathsf{Datum}\}$.
% \item $\mathcal P \isdef \{\mathsf{heeft-inhoud}, \mathsf{hoort-bij}, \mathsf{komt-van}, \mathsf{om}, \mathsf{schreef}, \mathsf{verwijst-naar}, \mathsf{wordt-genoemd-door}, \mathsf{heeft-url}, \mathsf{linkt-naar}, \mathsf{heeft-permalink}, \mathsf{permalink-van}\}$.
% \item $\mathcal F \isdef \{\mathsf{ai}, \mathsf{abd}, \mathsf{af}, \mathsf{bu}, \mathsf{au}\}$ met $\mathsf{ai}\isdef\{\mathsf{heeft-inhoud}, \mathsf{hoort-bij}\}, \mathsf{abd}\isdef\{\mathsf{komt-van},\mathsf{schreef},\mathsf{om}\}, \mathsf{af}\isdef\{\mathsf{verwijst-naar}, \mathsf{wordt-genoemd-door}\}, \mathsf{bu}\isdef\{\mathsf{heeft-url}, \mathsf{linkt-naar}\}, \mathsf{au}\isdef\{\mathsf{heeft-permalink}, \mathsf{permalink-van}\}$. Verder $\Base(\mathsf{heeft-inhoud}) = \Base(\mathsf{komt-van}) = \Base(\mathsf{verwijst-naar}) = \mathsf{Artikel}, \Base(\mathsf{hoort-bij}) = \mathsf{Inhoud}, \Base(\mathsf{om}) = \mathsf{Datum}, \Base(\mathsf{schreef}) = \Base(\mathsf{heeft-url}) = \mathsf{Bron}, \Base(\mathsf{wordt-genoemd-door}) = \mathsf{Film}, \Base(\mathsf{linkt-naar}) = \mathsf{URL}, \Base(\mathsf{heeft-permalink}) = \mathsf{Artikel}, \Base(\mathsf{permalink-van}) = \mathsf{URL}$.
% \end{itemize}
%\end{exmp}
%
%%todo
\section{Sequentietypen, objectificatie en constraints}
Laten we kijken of onze modelleermethode expressief genoeg is om alleen populaties toe te laten waarin de populatie van een entiteit volledig wordt opgedeeld in paarsgewijs disjuncte sequenties.
\subsection{Een voorbeeldschema}
Een voorbeeld hiervan kunnen we vinden in de structuur van series en afleveringen. Hiervoor bekijken we de volgende verzamelingen:
\begin{itemize}
\item $\mathcal E\isdef \{\mathsf{Aflevering}\}$.
\item $\mathcal S\isdef \{\mathsf{Serie}\}$.
\item $\mathcal L\isdef \{\mathsf{Titel}, \mathsf{I}\}$.
\item $\mathcal G\isdef \mathcal C\isdef \emptyset$.
\item $\mathcal P\isdef \{\in^e, \in^s, @^s, @^i, \mathsf{heet}_s, \mathsf{heet}_a, \mathsf{van}_s, \mathsf{van}_a\}$.
\item $\mathcal F\isdef \{\in, @, \mathsf{st}, \mathsf{at}\}$, met $\in\;\isdef\{\in^e,\in^s\}, @\isdef\{@^s,@^i\}, \mathsf{st}\isdef\{\mathsf{heet}_s,\mathsf{van}_s\}, \mathsf{at}\isdef\{\mathsf{heet}_a,\mathsf{van}_a\}$. Hierbij geldt $\Base(\in^e)=\Base(\mathsf{heet}_a)=\mathsf{Aflevering}, \Base(\in^s)=\Base(\mathsf{heet}_s)=\mathsf{Serie}, \Base(@^s)=\in, \Base(@^i)=\mathsf{I}, \Base(\mathsf{van}_s)=\Base(\mathsf{van}_a)=\mathsf{Titel}$.
\item $\mathcal O\isdef \mathcal E \cup \mathcal S \cup \mathcal L \cup \mathcal F$.
\end{itemize}
We nemen $\mathcal I\isdef \langle\mathcal P,\mathcal O,\mathcal L,\mathcal E,\mathcal F,\mathcal G,\mathcal S,\mathcal C,\Base,\Elt,\prec,\Spec,\Gen,\mathcal D,\Dom\rangle$ met $\prec=\Spec=\Gen=\emptyset$, $\Elt=\{(\mathsf{Serie},\mathsf{Aflevering})\}$ en $\Dom=\{(\mathsf{Titel},\mathcal A^+),(\mathsf{I},\mathbb N^+)\}$ waar $\mathcal A$ uit letters, cijfers en leestekens bestaat. %todo p. 37
Verder definiëren we de verzameling $\mathcal R$ met de volgende constraints:
\begin{itemize}
\item Totale rol: $\tau_s\isdef\{\in^s\}, \tau_a\isdef\{\in^e\}, \tau_e\isdef\{@^s\}, \tau_i\isdef\{@^i\}, \tau_t\isdef\{\mathsf{van}_s,\mathsf{van}_a\}, \tau_{st}\isdef\{\mathsf{heet}_s\}, \tau_{at}\isdef\{\mathsf{heet}_a\}$. Merk op dat dit strikter is dan de standaard constraints bij een sequentietype.
\item Uniciteit: $\upsilon_e\isdef\{\in^e\}, \upsilon_i\isdef\{@^s\}, \upsilon_s\isdef\tau_{st}, \upsilon_a\isdef\tau_{at}, \upsilon_{ts}\isdef\{\mathsf{van}_s\}, \upsilon_{ta}\isdef\{\mathsf{van}_a\}$. Ook dit is strikter dan de standaard constraints bij een sequentietype.
\item Exclusie: $\cstrexcl(\{\mathsf{van}_s\},\{\mathsf{van}_a\})$.
\end{itemize}
Dit geeft schema $\Sigma=\langle\mathcal I,\mathcal R\rangle$ in \autoref{fig:sequence-type}.
\begin{figure}[h]
\centering
\includegraphics[width=\maxwidth{.8\linewidth}]{sequence-type}
\caption{Een sequentietype met extra constraints}
\label{fig:sequence-type}
\end{figure}
\subsection{Metavragen}
Om de expressiviteit van de wiskundige definities te kunnen evalueren, zullen we een aantal vragen over het model proberen te beantwoorden met behulp van de wiskundige definities. Alhoewel het antwoord op de meeste vragen eenvoudig is in te zien, is het doel hier ze met de formele definities te vinden. Als dit ook kan, dan betekent dit dat we het proces in principe ook kunnen automatiseren in bijvoorbeeld een modelleerapplicatie.
\subsubsection{Globale objectpopuleerbaarheid}
We kunnen bewijzen dat dit schema globaal objectpopuleerbaar is. Dit doen we door een geldige populatie $\Pop$ aan te wijzen die instanties aan ieder objecttype toewijst:
\begin{itemize}
\item $\Pop(\textsf{Aflevering}) = \{a_1,a_2,a_3\}$.
\item $\Pop(\textsf{Serie}) = \{s_1,s_2\}$.
\item $\Pop(\textsf{Titel}) = \{\textsf{De Cock en de moord op het bureau}, \textsf{De Cock en de Reclamemoord}, \textsf{Gasbellen}, \textsf{De Fractie}, \textsf{Baantjer}\}$.
\item $\Pop(\textsf{I}) = \{1,2\}$.
\item $\Pop(\in) = \{t_1\isdef\{\in^s:s_1, \in^e:a_3\}, t_2\isdef\{\in^s:s_2, \in^e:a_1\}, t_3\isdef\{\in^s:s_2, \in^e:a_2\}\}$.
\item $\Pop(@) = \{\{@^s:t_1,@^i:1\}, \{@^s:t_2,@^i:1\}, \{@^s:t_3,@^i:2\}\}$.
\item $\begin{aligned}\Pop(\textsf{at}) = \{&\{\textsf{heet}_a:a_1, \textsf{van}_a:\textsf{De Cock en de moord op het bureau}\},\\
&\{\textsf{heet}_a:a_2, \textsf{van}_a:\textsf{De Cock en de Reclamemoord}\},\\
&\{\textsf{heet}_a:a_3, \textsf{van}_a:\textsf{Gasbellen}\}\}.\end{aligned}$
\item $\Pop(\textsf{st}) = \{\{\textsf{heet}_s:s_1, \textsf{van}_s:\textsf{De Fractie}\}, \{\textsf{heet}_s:s_2, \textsf{van}_s:\textsf{Baantjer}\}\}$.
\end{itemize}
Gezien het schema behoeft het eigenlijk geen argumentatie dat deze populatie de constraints niet schendt. Maar laten we toch even kijken of we ook tot die conclusie kunnen komen met de wiskundige definities.
\begin{itemize}
\item We weten dat $\Pop\vDash\cstrtot(\tau_s)$, want \begin{align*}
\bigcup_{q\in\tau_s}\Pop(\Base(q)) &= \Pop(\Base(\in^s)) = \Pop(\mathsf{Serie}) = \{s_1, s_2\}\\
&= \{t(\in^s) \mid t \in \{(\in^s:s_1,\in^e:a_3), (\in^s:s_2,\in^e:a_1), (\in^s:s_2,\in^e:a_2)\}\}\\
&= \{t(\in^s) \mid t \in \Val{\pi_{\in^s}(\in)}(\Pop)\}\\
&= \Val{\theta_{\in^s}(\pi_{\in^s}(\in))}(\Pop)\\
&= \Val{\theta_{\in^s}(\pi_{\in^s}(\Fact(\in^s)))}(\Pop)\\
&= \bigcup_{q\in\tau_s}\Val{\theta_q(\pi_q(\Fact(q)))}(\Pop).
\end{align*}
De andere totale rol-constraints $\cstrtot(\tau_a), \cstrtot(\tau_e), \cstrtot(\tau_i), \cstrtot(\tau_{st})$ en $\cstrtot(\tau_{at})$ gaan op soortgelijke wijze.
\item Het constraint $\cstrtot(\tau_t)$ verdient een aparte behandeling, aangezien $|\tau_t|>1$. Onze populatie voldoet ook aan dit constraint. Er geldt $\Pop\vDash\cstrtot(\tau_t)$, want \begin{align*}
\bigcup_{q\in\tau_t}\Pop(\Base(q)) =&\; \Pop(\Base(\mathsf{van}_s)) \cup \Pop(\Base(\mathsf{van}_a)) = \Pop(\mathsf{Titel})\\
=&\; \{t(\mathsf{van}_s) \mid t \in \{(\mathsf{van}_s:\textsf{De Fractie},\mathsf{heet}_s:s_1),(\mathsf{van}_s:\textsf{Baantjer},\mathsf{heet}_s:s_2)\}\}\\
&\; \cup \{t(\mathsf{van}_a) \mid t \in \{(\mathsf{van}_a:\textsf{De Cock en de moord op het bureau},\mathsf{heet}_a:a_1),\\
&\qquad\qquad (\mathsf{van}_a:\textsf{De Cock en de Reclamemoord},\mathsf{heet}_a:a_2),\\
&\qquad\qquad (\mathsf{van}_a:\textsf{Gasbellen},\mathsf{heet}_a:a_3)\}\}\\
=&\; \{t(\mathsf{van}_s) \mid t\in\Val{\pi_{\mathsf{van}_s}(\mathsf{st})}(\Pop)\} \cup \{t(\mathsf{van}_a) \mid t\in\Val{\pi_{\mathsf{van}_a}(\mathsf{at})}(\Pop)\}\\
=&\; \Val{\theta_{\mathsf{van}_s}(\pi_{\mathsf{van}_s}(\mathsf{st}))}(\Pop) \cup \Val{\theta_{\mathsf{van}_a}(\pi_{\mathsf{van}_a}(\mathsf{at}))}(\Pop)\\
=&\; \Val{\theta_{\mathsf{van}_s}(\pi_{\mathsf{van}_s}(\Fact({\mathsf{van}_s})))}(\Pop) \cup \Val{\theta_{\mathsf{van}_a}(\pi_{\mathsf{van}_a}(\Fact({\mathsf{van}_a})))}(\Pop)\\
=&\; \bigcup_{q\in\tau_t}\Val{\theta_q(\pi_q(\Fact(q)))}(\Pop).
\end{align*}
\item $\Pop$ voldoet op triviale wijze aan de uniciteitsconstraints behorend bij de verzamelingen $\upsilon_e$, $\upsilon_s$, $\upsilon_a$, $\upsilon_{ts}$ en $\upsilon_{ta}$. We bekijken hier daarom alleen $\cstruniq(\upsilon_i)$. %todo
In dit geval dienen we feittype $@$ unnesten. Dit geeft de afgeleide relatie $\xi(\upsilon_i)=\{\in^s, \in^e, @^i\}$ waarbij een uniciteitsconstraint op zowel $\{\in^e\}$ als $\{\in^e,\in^s\}$ ligt. Het eerste constraint correspondeert met $\cstruniq(\upsilon_e)$, het tweede met $\cstruniq(\upsilon_i)$.
Maar omdat we hierboven al hebben gezien dat $\Pop\vDash\cstruniq(\upsilon_e)$ kunnen in de populatie van $\xi(\upsilon_i)$ geen twee verschillende tupels met gelijke $\in^e$ zitten. Hieruit volgt dan ook dat $\Pop\vDash\cstruniq(\upsilon_i)$.
\item Het uitwerken van het laatste constraint, $\cstrexcl(\{\mathsf{van}_s\},\{\mathsf{van}_a\})$, heeft op dit punt geen toegevoegde waarde omdat het op soortgelijke wijze gaat.
\end{itemize}
We hebben gezien dat $\Pop$ aan alle constraints voldoet. Bovendien is $\Pop$ niet leeg. Hiermee hebben we dus bewezen dat bovenstaand schema globaal objectpopuleerbaar is: $\GlobObjPop(\Sigma)$. Hieruit volgt direct ook $\GlobAtomPop(\Sigma)$, $\LocObjPop(\Sigma)$ en $\LocAtomPop(\Sigma)$.
\subsubsection{Zijn er populaties waarbij een bepaald objecttype niet gepopuleerd is?}
Het is voor te stellen dat we in bepaalde gevallen niet willen dat een objecttype niet gepopuleerd wordt. Waar we bij globale objectpopuleerbaarheid kijken of (alle) objecttypes gepopuleerd \emph{kunnen} worden, willen we nu kijken of we bepaalde objecttypes \emph{moeten} populeren. Voor alle duidelijkheid: dit is in feite equivalent met het controleren of het frequentieconstraint $\{1\dots\}$ op dit objecttype overbodig zou zijn. Hierbij laten we de lege populatie buiten beschouwing.
Aangezien we de lege populatie buiten beschouwing laten, moet tenminste één objecttype gepopuleerd zijn.
\begin{itemize}
\item Stel dat $\Pop(\mathsf{Titel})\neq\emptyset$. Aangezien $\bigcup_{q\in\tau_t}\Pop(\Base(q))=\Pop(\mathsf{Titel})\neq\emptyset$, moet volgens $\cstrtot(\tau_t)$ de verzameling $\bigcup_{q\in\tau_t}\Val{\theta_q(\pi_q(\Fact(q)))}(\Pop)$ tenminste één element bevatten. Concreet betekent dit dat $\Pop(\mathsf{st})\neq\emptyset$ of $\Pop(\mathsf{at})\neq\emptyset$. In het eerste geval geldt dan ook $\Pop(\mathsf{Serie})\neq\emptyset$ volgens de conformiteitsregel, in het tweede geval geldt $\Pop(\mathsf{Aflevering})\neq\emptyset$ volgens diezelfde regel. In beide gevallen dient één van de twee totale rolconstraints over $\tau_s$ en $\tau_a$ vervuld te worden (op eenzelfde manier als hierboven), waardoor $\Pop(\in)\neq\emptyset$. Ten slotte blijkt zo ook dat $\Pop(@)\neq\emptyset$ en aangezien $@^i\in@$ en $\Base(@^i)=\mathsf{I}$ geldt dan ook $\Pop(\mathsf{I})\neq\emptyset$. In dit geval is zo ieder objecttype gepopuleerd.
\item Stel dat $\Pop(\mathsf{Titel})=\emptyset$ maar $\Pop(\mathsf{Serie})\neq\emptyset$. Om de populatie te laten voldoen aan $\cstrtot(\tau_{st})$ moet $\mathsf{st}$ gepopuleerd zijn. Maar omdat $\mathsf{van}_s\in\mathsf{st}$ en $\Base(\mathsf{van}_s)=\mathsf{Titel}$, moet dan ook $\mathsf{Titel}$ gepopuleerd zijn, wat in tegenspraak is met onze aanname. Op dezelfde manier is het ook niet mogelijk dat $\Pop(\mathsf{Aflevering})\neq\emptyset$ tenzij $\mathsf{Titel}$ ook gepopuleerd is.
\item Stel dat $\Pop(\mathsf{Titel})=\Pop(\mathsf{Serie})=\Pop(\mathsf{Aflevering})=\emptyset$ maar dat $\in$ wel gepopuleerd kan worden. Dan moet volgens de conformiteitsregel bijvoorbeeld $\Base(\in^s)=\mathsf{Serie}$ gepopuleerd worden, wat in tegenspraak is met onze aanname.
\item Stel ten slotte dat geen enkel objecttype gepopuleerd wordt behalve $\mathsf{I}$. In dit geval moet $\Pop(@)\neq\emptyset$ om $\Pop\vDash\cstrtot(\tau_e)$ te laten gelden. Maar aangezien $@^s\in@$ en $\Base(@^s)=\in$ moet dan ook $\in$ gepopuleerd zijn, wat in strijd is met onze aanname omdat $\in$ een geobjectificeerd feittype is.
\end{itemize}
Het blijkt dus dat er geen mogelijkheid is voor welk objecttype dan ook om ongepopuleerd te zijn, tenzij alle objecttypen dat zijn.
\subsubsection{Heeft het toevoegen van $\cstruniq(\{\mathsf{heet}_s,\mathsf{heet}_a\})$ zin?}
Het is mogelijk dat een modelleur oppert bovenstaand constraint toe te voegen aan het schema, om uit te sluiten dat een $\mathsf{Serie}$ en een $\mathsf{Aflevering}$ dezelfde titel hebben. Op dat moment zouden we graag willen weten of het toevoegen van dit constraint de semantiek van het schema verandert en of het dus iets uitmaakt. Formeel kunnen we stellen dat een constraint $r'$ alleen `iets toevoegt' aan $\Sigma=\langle\mathcal I,\mathcal R\rangle$ als het volgende geldt:
$$\exists_{\Pop\in\POP_{\mathcal I}}\left[\forall_{r\in\mathcal R}\left[\Pop\vDash r\right] \land \Pop\nvDash r'\right].$$
Laten we dan bekijken of dit geldt voor $r'=\cstruniq(\{\mathsf{heet}_s,\mathsf{heet}_a\})$. De afgeleide relatie is $\xi(r')=\sigma_{\mathsf{van}_a=\mathsf{van}_s}(\mathsf{at}\bowtie\mathsf{st})$. Het constraint zegt nu dat $\{\mathsf{heet}_s,\mathsf{heet}_a\}$ een sleutel van $\xi(r')$ moet zijn. Als deze constraint niet overbodig zou zijn, dan is er dus een populatie $\Pop$ die wel aan alle constraints in $\mathcal R$ voldoet, maar waarvoor $\{\mathsf{heet}_s,\mathsf{heet}_a\}$ de afgeleide relatie $\xi(r')$ niet identificeert.
Er zijn dus $s\in\Pop(\mathsf{Serie}), a\in\Pop(\mathsf{Aflevering})$ en $t\in\Pop(\mathsf{Titel})$ zo dat $(s,a,t)$ meerdere keren voorkomt in $\Pop(\xi(r'))$. Dit kan op drie verschillende manieren zo zijn gekomen:
\begin{itemize}
\item $(a,t)$ komt meerdere keren voor in $\Pop(\mathsf{at})$. Dit is echter in strijd met $\cstruniq(\upsilon_{ta})$. Dit constraint heeft de afgeleide relatie $\xi(\upsilon_{ta})=\mathsf{at}$, maar $\upsilon_{ta}=\{\mathsf{van}_a\}$ kan geen sleutel van deze relatie zijn als $(a,t)$ meerdere keren voorkomt in $\Pop(\mathsf{at})=\Pop(\xi(\upsilon_{ta}))$.
\item $(s,t)$ komt meerdere keren voor in $\Pop(\mathsf{st})$. Dit is onmogelijk vanwege een soortgelijk argument.
\item $(a,t)$ komt (één keer) voor in $\Pop(\mathsf{at})$, en $(s,t)$ komt (één keer) voor in $\Pop(\mathsf{st})$. Maar dit is in strijd met $\cstrexcl(\{\mathsf{van}_s\},\{\mathsf{van}_a\})$. Dit constraint stelt namelijk dat $\Pop\vDash\pi_{\{\mathsf{van}_s\}}(\xi(\{\mathsf{van}_s\})) \otimes \pi_{\{\mathsf{van}_a\}}(\xi(\{\mathsf{van}_a\}))$, terwijl dit niet het geval is:
\belowdisplayskip=0pt\begin{align*}
& \Pop\vDash \pi_{\{\mathsf{van}_s\}}(\xi(\{\mathsf{van}_s\})) \otimes \pi_{\{\mathsf{van}_a\}}(\xi(\{\mathsf{van}_a\}))\\
\equiv\;& \Pop\vDash \pi_{\{\mathsf{van}_s\}}(\mathsf{st}) \otimes \pi_{\{\mathsf{van}_a\}}(\mathsf{at})\\
\equiv\;& \Pop\vDash \forall_{u\in\Val{\pi_{\{\mathsf{van}_s\}}}(\Pop)} \lnot\exists_{v\in\Val{\pi_{\{\mathsf{van}_a\}}}(\Pop)} \forall_{p\in\Schema(\{\mathsf{van}_s\})}[u(p)=v(\phi(p))]\\
\equiv\;& \Pop\vDash \forall_{u\in\{(\mathsf{heet}_s:s,\mathsf{van}_s:t)\}} \lnot\exists_{v\in\{(\mathsf{heet}_a:a,\mathsf{van}_a:t)\}} [u(\mathsf{van_s})=v(\mathsf{van_a})],\\
\end{align*}
maar neem maar $u=(s,t), v=(a,t)$. Hierbij zijn we voor het gemak even uitgegaan van een minimale populatie (met slechts $(a,t)$ en $(s,t)$).
\end{itemize}
Aangezien elk van deze drie mogelijkheden tegenspraak oplevert, is er geen populatie die werd toegestaan door de constraints in $\mathcal R$, maar wordt verboden door $\cstruniq(\{\mathsf{heet}_s,\mathsf{heet}_a\})$. Het toevoegen van dit constraint zou de semantiek van $\Sigma$ dus niet veranderen.
\subsection{Evaluatie}
Zowel het bewijs van de globale objectpopuleerbaarheid als het bewijs van het niet bestaan van lege lokale populaties in een willekeurige niet-lege globale populatie als het bewijs dat het toevoegen van $\cstruniq(\{\mathsf{heet}_s,\mathsf{heet}_a\})$ geen zin heeft vergden geen bijzondere stappen. Het is niet moeilijk voor te stellen dat deze bewijzen geautomatiseerd zouden kunnen worden. Op die manier zou een modelleertoepassing deze en andere eigenschappen van het model onder handen zelf autonoom kunnen onderzoeken, en de gebruiker bijvoorbeeld een waarschuwing geven op het moment dat hij een wijziging maakt waardoor het schema bijvoorbeeld niet meer globaal objectpopuleerbaar is. Hierbij is de wiskundige definitie natuurlijk van levensbelang.
Wel hadden we op bepaalde punten handige keuzes nodig om het bewijs rond te krijgen. Bij het bewijs van de globale objectpopuleerbaarheid hebben we niet gekeken hoe we de keuzes voor de populaties van de verschillende objecttypen zouden kunnen formaliseren. Is het handig om veel instanties in de populatie te hebben of weinig? En wat moeten we doen als we een populatie kiezen die niet aan de constraints voldoet? Welke keuzes moeten we maken om zo efficiënt mogelijk een bewijs te kunnen leveren?
En daarnaast: hoe zouden we moeten herkennen dat een schema \emph{niet} globaal objectpopuleerbaar is? Willen we dit bewijs daadwerkelijk automatiseren, dan kunnen we niet zomaar de hoogstwaarschijnlijk oneindig grote zoekruimte $\POP_{\mathcal I}$ doorzoeken om te kijken of er een populatie is die voldoet aan alle constraints. Bij de twee andere bewijzen spelen soortgelijke problemen.
\subsection{Suggesties voor uitbreiding van de theorie}
\subsubsection{Orden de zoekruimte}
Dit is niet zozeer een suggestie voor de uitbreiding van de theorie als wel een suggestie voor de automatisering van een bewijs voor globale objectpopuleerbaarheid waar hierboven al op werd gehint. Dezelfde methode zou natuurlijk ook gebruikt kunnen worden voor lokale objectpopuleerbaarheid en dergelijke.
Zoals hierboven al aangegeven kunnen we niet zomaar de hele zoekruimte $\POP_{\mathcal I}$ doorzoeken, willen we één populatie vinden die globaal objectpopuleerbaar is. De suggestie hier is om de zoekruimte in een gerichte graaf $G=(V,E)$ te ordenen. Laat $V=\POP_{\mathcal I}$, en laat er een kant bestaan van een populatie $\Pop$ naar een populatie $\Pop'$ als $\Pop'$ precies één objectinstantie meer telt dan $\Pop$, terwijl de populaties voor de rest gelijk zijn.
Vervolgens doorlopen we de graaf middels een breadth first search op grootte van de populaties. Op het moment dat een populatie $\Pop$ niet voldoet aan de constraints van het schema omdat het \emph{te veel} elementen bevat (dit kan het geval zijn bij uniciteits-, frequentie- en setconstraints), kan de gehele subgraaf die uit $\Pop$ bereikbaar is worden gesnoeid.
In theorie zou het ook mogelijk zijn om, als we van een populatie $\Pop$ weten dat deze niet voldoet aan de constraints omdat het \emph{te weinig} elementen bevat (bijvoorbeeld bij een totale rolconstraint), die populaties van waaruit $\Pop$ bereikt kan worden te snoeien. Willen we echter beide methoden gebruiken om de zoekruimte in te perken, dan moeten we eerst een manier hebben om een aantal goede populaties te kiezen om mee te beginnen. Deze mogen niet te klein zijn, zodat we de eerste snoeimethode kunnen gebruiken, maar ook niet te groot, zodat we de tweede methode kunnen benutten. Wellicht is het starten vanuit de lege populatie echter efficiënter dan het bepalen van goede populaties om mee te beginnen.
In ieder geval zou het op deze manier mogelijk zijn efficiënter naar mogelijk interessante populaties te zoeken, en bovendien is het op deze manier sneller te bepalen wanneer zo'n populatie niet bestaat (namelijk als er geen onbezochte, niet gesnoeide vertices meer in de graaf zitten).
\section{Contextvrije grammatica's}
Het omschrijven van een contextvrije grammatica naar een informatiesysteem is een onderwerp wat nog volop in ontwikkeling is. %todo
\end{document}
|
