diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | report.tex | 10 |
2 files changed, 6 insertions, 10 deletions
@@ -7,16 +7,12 @@ all: $(TARGET) include $(TARGET:.pdf=.dep) -genesis.pdf : genesis.tex - xelatex $< - xelatex $< - %.pdf : %.tex pdflatex $< pdflatex $< clean: - latexmk -c + latexmk -C rm -f *.dep .PHONY: clean @@ -86,7 +86,7 @@ \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. +Het eerste onderdeel dat 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} @@ -120,7 +120,7 @@ Dit geeft schema $\Sigma=\langle\mathcal I,\mathcal R\rangle$ in \autoref{fig:se \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. +Om de expressiviteit en hanteerbaarheid van de wiskundige definities te evalueren, zullen we een aantal vragen \emph{over} het model proberen te beantwoorden. 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: @@ -128,7 +128,7 @@ We kunnen bewijzen dat dit schema globaal objectpopuleerbaar is. Dit doen we doo \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{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\}\}$. @@ -157,7 +157,7 @@ Gezien het schema behoeft het eigenlijk geen argumentatie dat deze populatie de =&\; \{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\}\}\}\\ + &\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)\\ @@ -166,7 +166,7 @@ Gezien het schema behoeft het eigenlijk geen argumentatie dat deze populatie de \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)$. + In dit geval dienen we feittype $@$ te 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)$. |