path: root/report.tex

\documentclass[a4paper]{article}

\usepackage[dutch]{babel}
\usepackage[hidelinks]{hyperref}
\usepackage[margin=30mm,bottom=36mm]{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{syntax}
\newcommand\nonterm[1]{\langle\mathit{#1}\rangle}
\newcommand\term[1]{\text{`\texttt{#1}'}}
\newcommand\termsf[1]{\text{`\textsf{#1}'}}

\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{Een evaluatie van informatiesystementheorie}
\author{Camil Staps}

\begin{document}

\maketitle
\thispagestyle{fancy}

\begin{abstract}
    Dit werkstuk is een evaluatie van de theorie beschreven in Advanced information models \cite{aim}. De evaluatie is gedaan aan de hand van de IMDb \cite{imdb}. De omvang van de theorie en van de IMDb is zo groot dat deze evaluatie helaas onvolledig is. In plaats van een compleet beeld te geven, zullen we twee aspecten van de theorie uitlichten met een voorbeeld uit de IMDb, en aan de hand daarvan de theorie evalueren.
\end{abstract}

\section{Sequentietypen, objectificatie en constraints}
Het eerste onderdeel wat we zullen bekijken is dat van `gewone' typen. Hierin bekijken we objecttypen, feittypen, objectificaties, sequentietypen (en dus eigenlijk ook powertypen) en labeltypen.

\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. 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 \emph{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)$.

        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) objecttypen gepopuleerd \emph{kunnen} worden, willen we nu kijken of we bepaalde objecttypen \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).

\clearpage
\section{Contextvrije grammatica's}
Het omschrijven van een contextvrije grammatica naar een informatiesysteem is een onderwerp wat nog volop in ontwikkeling is. Hoewel de relatie met de IMDb wellicht wat vergezocht is, wil ik het toch even aanstippen.

\subsection{Een voorbeeldschema}
Laten we de contextvrije grammatica $G$ in \autoref{fig:cfg-gram} bekijken. Het gaat hier om de definitie van een cast als een niet leeg lijstje van acteurs.

\begin{figure}[h]
    \centering
    \begin{minipage}{21.6em}
        \setlength{\grammarparsep}{0pt}
        \setlength{\grammarindent}{8.5em}
        \begin{grammar}
            <Cast> ::= <Acteur> `, ' <Cast> | <Acteur>
        
            <Acteur> ::= <Voornaam> ` ' <Achternaam>
        
            <Voornaam> ::= <string>
        
            <Achternaam> ::= <string>
        \end{grammar}
    \end{minipage}
    \caption{Een contextvrije grammatica}
    \label{fig:cfg-gram}
\end{figure}

Het bijbehorende schema $\Delta(G)$ is te zien in \autoref{fig:cfg-schema}. Hierbij zijn die nonterminals die alleen zijn om te schrijven tot $\nonterm{string}$ gerepresenteerd met labels. De standaardrepresentatie zou bijvoorbeeld vereisen dat $\nonterm{Voornaam}$ een generalisatie is van een geobjectificeerd unair feittype met als basis $\nonterm{string}$, maar dit heeft weinig toegevoegde waarde.

\begin{figure}[b!]
    \centering
    \includegraphics[width=\maxwidth{.5\linewidth}]{cfg-schema}
    \caption{De informatiestructuur als gegenereerd vanuit onze grammatica. Indien het onleesbaar is: de predicaten zijn $r_{1,c},r_{1,k},r_{1,a},r_{2,v},r_{2,s}$ en $r_{2,a}$. De naam komt telkens overeen met het bijbehorende feittype en de basis.}
    \label{fig:cfg-schema}
\end{figure}

\subsection{Een voorbeeldpopulatie}
Onze grammatica genereert de string $\termsf{Piet Römer, Victor Reinier}$ als volgt:
\begin{align*}
    \nonterm{Cast} &\to \nonterm{Acteur} \;\term{, }\; \nonterm{Cast}\\
                   &\to \nonterm{Voornaam} \;\term{ }\; \nonterm{Achternaam} \;\term{, }\; \nonterm{Cast}\\
                   &\to \nonterm{string} \;\term{ }\; \nonterm{string} \;\term{, }\; \nonterm{Cast}\\
                   &\to \termsf{Piet} \;\term{ }\; \termsf{Römer} \;\term{, }\; \nonterm{Cast}\\
                   &\to \termsf{Piet} \;\term{ }\; \termsf{Römer} \;\term{, }\; \nonterm{Acteur}\\
                   &\to \termsf{Piet} \;\term{ }\; \termsf{Römer} \;\term{, }\; \nonterm{Voornaam} \;\term{ }\; \nonterm{Achternaam}\\
                   &\to \termsf{Piet} \;\term{ }\; \termsf{Römer} \;\term{, }\; \nonterm{string} \;\term{ }\; \nonterm{string}\\
                   &\to \termsf{Piet} \;\term{ }\; \termsf{Römer} \;\term{, }\; \termsf{Victor} \;\term{ }\; \termsf{Reinier}\\
\end{align*}

Met de elementen van deze string kunnen we dus ook ons schema populeren:

\begin{itemize}
    \item $a_1 \isdef \{r_{2,v}:\termsf{Piet}, r_{1,s}:\term{ }, r_{1,a}:\termsf{Römer}\}$ en $a_2 \isdef \{r_{2,v}:\termsf{Victor}, r_{1,s}:\term{ }, r_{1,a}:\termsf{Reinier}\}$.
    \item $c_1 \isdef \{r_{1,c}:c_2, r_{1,k}:\term{, }, r_{1,a}:a_1\}$ en $c_2\isdef a_2$.
    \item $\Pop(\mathsf{Cast}) = \{c_1,c_2\}$.
    \item $\Pop(\mathsf{Acteur}) = \{a_1,a_2\}$.
    \item $\Pop(\mathsf{Voornaam}) = \{\termsf{Piet},\termsf{Victor}\}$.
    \item $\Pop(\mathsf{Achternaam}) = \{\termsf{Römer},\termsf{Reinier}\}$.
    \item $\Pop(\mathsf{Komma}) = \{\term{, }\}$.
    \item $\Pop(\mathsf{Spatie}) = \{\term{ }\}$.
    \item $\Pop(r_1) = \{c_1\}$.
    \item $\Pop(r_2) = \{a_1, a_2\}$.
\end{itemize}

\subsection{Evaluatie}
Een aantal dingen valt direct op:

\begin{itemize}
    \item Feittypen zijn niet geordend. Hierdoor kan de originele grammatica niet van het informatiesysteem worden gereconstrueerd. Het schema in \autoref{fig:cfg-schema} had evengoed een representatie van de regel $\nonterm{Acteur} ::= \nonterm{Achternaam} \;\term{ }\; \nonterm{Voornaam}$ kunnen bevatten.

        Daar komt nog bij dat als we niet tussen voor- en achternamen zouden differentiëren (we zouden bijvoorbeeld een regel $\nonterm{Acteur} ::= \nonterm{Naam}\;\term{ }\;\nonterm{Naam}$ kunnen hebben), de voorbeeldpopulatie zowel $\termsf{Piet Römer}$ als $\termsf{Römer Piet}$ als acteur had kunnen bevatten, zonder dat het duidelijk was welke van de twee werd bedoeld. Schema's worden op die manier al snel ambigu.

    \item De populatie bevat redundantie. Zo slaan we de populatie van het labeltype $\mathsf{Komma}$ op, terwijl vanaf het begin duidelijk is dat deze populatie altijd precies $\{\term{, }\}$ zal zijn. Dit komt terug in feittype $r_1$, en iets soortgelijks gebeurt voor $\mathsf{Spatie}$ en $r_2$. Het liefst zouden we deze terminals niet opslaan maar in het informatiesysteem inbouwen.
\end{itemize}

\subsection{Suggesties voor uitbreiding van de theorie}
\subsubsection{Geordende feittypen}
Om het eerstgenoemde probleem hierboven op te lossen zouden we de volgende aanpassing kunnen doorvoeren. Waar een feittype $f$ nu een verzameling predicaten $\{p_1,p_2,\dots,p_n\}$ is, maken we hier nu een rijtje $\mathbb N^+\nrightarrow\mathcal P$ van. De grafische weergave van $\{(1,p_1),(2,p_2),(3,p_3)\}$ is dan als in \autoref{fig:ordered-fact-type}. Verder moet de volgende eigenschap gelden om af te dwingen dat elk predicaat precies één keer wordt gebruikt in één of ander feittype:

$$\forall_{p\in\mathcal P}\exists!_{f\in\mathcal F}\exists!_{k\in\mathbb N^+}[f(k)=p].$$

\begin{figure}
    \centering
    \includegraphics[width=\maxwidth{.35\linewidth}]{ordered-fact-type}
    \caption{De representatie van een geordend feittype $\{(1,p_1),(2,p_2),(3,p_3)\}$. De volgorde van de predicaten in de grafische weergave is irrelevant.}
    \label{fig:ordered-fact-type}
\end{figure}

\subsubsection{Een bijectieve transformatie}
De aanpassing hierboven maakt het bijna helemaal mogelijk van een informatiesysteem een contextvrije grammatica te maken. Het enige wat nog nodig is, is om in het informatiesysteem het startsymbool aan te geven. Dit doen we simpelweg door een extra element $S$ aan $\mathcal I$ toe te voegen. Dit zal hieronder duidelijk worden.

Deze aanpassing zorgt ervoor dat we van een informatiesysteem op precies één manier een contextvrije grammatica kunnen maken, waardoor de transformatie een bijectie wordt: gegeven $\mathcal I=\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, S\rangle$ (merk op dat het symbool $S$ hier als startsymbool is toegevoegd) genereren we een contextvrije grammatica $G=\langle N,\Sigma,\Pi,S\rangle$ met:

\begin{itemize}
    \item De verzameling nonterminals $N=\mathcal E$.
    \item De verzameling terminals $\Sigma=\mathcal L$.
    \item De verzameling productieregels $\Pi$, een relatie van $N$ naar $(N\cup\Sigma)^*$:
        $$\Pi = \left\{(e, (p_1,p_2,\dots,p_n)) \mid \exists_{f\in\mathcal F}\left[e \Gen f \land \forall_{1\le k\le|f|}\left[f(k)=p_k\right]\right]\right\}.$$
        In woorden: $e$ produceert $p_1p_2\dots p_n$ precies dan als $e$ een generalisatie is van een feittype $f=\{(1,p_1),(2,p_2),\dots,(n,p_n)\}$.
\end{itemize}

\subsubsection{Geen overbodige informatie opslaan}
Zoals al eerder gezegd slaan we onnodig veel informatie op wanneer we een informatiesysteem, wat gegenereerd is van een contextvrije grammatica, gaan populeren. Dit komt doordat er labeltypen zijn die altijd door precies één objectinstantie kan worden gepopuleerd. In het voorbeeld hierboven zijn dat de typen $\mathsf{Komma}$ en $\mathsf{Spatie}$.

Een manier om dit tegen te gaan is door de informatie in deze labeltypen in de bijbehorende feittypen te zetten. Het idee is om elk feittype $f$ een functie $\hat f : \Pop(f) \to (N\cup\Sigma)^*$ mee te geven, de representatiefunctie. Deze functie geeft aan hoe een instantie in de populatie gerepresenteerd kan worden ($\nonterm{Voornaam}\;\term{ }\;\nonterm{Achternaam}$), terwijl de essentie van de instantie wordt bepaald door niet-triviale objecttypen ($\nonterm{Voornaam}$ en $\nonterm{Achternaam}$). In het voorbeeld van $r_2$ hierboven met de instantie $a_1$ zou $\hat f$ er dus zo uit zien:

$$\hat f(\{r_{2,v}:\termsf{Piet},r_{2,a}:\termsf{Römer}\}) = \termsf{Piet Römer}.$$

In het algemeen ($\mid\mid$ is de concatenatieoperator): $$\hat f(\mathsf{pop}) = \mathsf{pop}(r_{2,v}) \mid\mid \term{ } \mid\mid \mathsf{pop}(r_{2,a}).$$

Merk op dat het predicaat $r_{2,s}$ niet meer bestaat, omdat we het bijbehorende labeltype hebben verwijderd uit de informatiestructuur. 

Belangrijk is verder dat één feittype meerdere representaties kan hebben. Dit was bijvoorbeeld het geval geweest als de grammatica ook een regel $\nonterm{Acteur} ::= \nonterm{Voornaam}\;\term{:}\;\nonterm{Achternaam}$ had gehad. De niet-triviale feittypen zijn in dit geval namelijk hetzelfde als voor de regel die een spatie tussen de voor- en achternaam zet.

Hoe we de representatiefunctie opslaan is niet van groot belang. Eén mogelijkheid is om de verzameling $\mathcal F$ te herdefiniëren als een verzameling tupels $(f,\hat f)$. Het is niet handig om een functie $\hat{\mathcal F}$ te definiëren die voor ieder feittype $f$ alle mogelijke representatiefuncties $\hat f$ geeft. Zouden we dat doen, dan weten we -- nadat we het schema hebben gepopuleerd -- niet meer welke representatie bij welke feittypeinstantie hoort. In ons voorbeeld zouden we dan in een populatie niet kunnen differentiëren tussen $\termsf{Piet Römer}$ en $\termsf{Piet:Römer}$. In andere woorden: de representatiefunctie is een essentieel onderdeel van het bijbehorende feittype.

Indien we deze wijziging doorvoeren, is het niet meer nodig feittypen als rijtjes op te slaan, maar voldoet de originele definitie als een verzameling van predicaten. De informatie die werd opgeslagen in de volgorde van het rijtje wordt nu verwerkt in de representatiefunctie. Het idee om feittypen als rijtjes predicaten te zien staat hierboven nog, omdat het een kleinere wijziging is die makkelijker is in te bouwen in de theorie. Mocht de wijziging in deze paragraaf onvoorziene problemen opleveren, dan raad ik aan om in ieder geval die wijziging door te voeren.

Dit betekent ook dat de bijectieve transformatie hierboven beschreven moet worden aangepast. In plaats van de volgorde van de predicaten in een feittype moet deze nu de representatiefunctie meenemen.

\section{Conclusie}
De theorie gepresenteerd in \cite{aim} zit gedegen in elkaar. De formele definities zijn precies genoeg om geautomatiseerd over informatiesystemen te kunnen redeneren. Dit is bijvoorbeeld van belang bij het ontwikkelen van modelleertoepassingen. Alhoewel het raamwerk van definities goed in elkaar zit, mist er wel wat in de hoek van de algoritmiek. Zo bekeken we naar aanleiding van de metavragen over het model van series en afleveringen wat goede keuzes zijn wanneer we een bewijs voor een bepaalde eigenschap van een model geautomatiseerd willen opstellen. We hebben een suggestie gedaan wat betreft de volgorde waarin men kan zoeken naar een populatie die aan eigenschappen als globale objectpopuleerbaarheid voldoet.

Alhoewel het zeer nuttig is om contextvrije grammatica's naar informatiemodellen te kunnen transformeren (zodat we uiteindelijk bijvoorbeeld natuurlijke tekst in een relationele database kunnen opslaan en geavanceerde zoekqueries kunnen gebruiken op die database), is hier nog wel wat werk aan de winkel. Zo zijn de afgeleide modellen soms ambigu, en is het hierdoor niet mogelijk van een informatiemodel terug te gaan naar een grammatica. Bovendien zijn de populaties van de afgeleide schema's relatief groot doordat zij onnodig veel informatie bevatten. We hebben enkele suggesties gedaan om ambiguïteit te verwijderen en populaties te minimaliseren.

\begin{thebibliography}{9}
    \bibitem{aim} Advanced information models. Arthur ten Hofstede en Patrick van Bommel. Radboud Universiteit Nijmegen, november 2015.
    \bibitem{imdb} International Movie Database, \url{http://imdb.com}.
\end{thebibliography}

\end{document}