summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCamil Staps2016-04-23 17:58:53 +0200
committerCamil Staps2016-04-23 17:58:53 +0200
commitb72abb59ffbb485c5c6b7bf3bee0a2237230cc4b (patch)
tree467cfbb9e8713981cbb5591f2f314e16871c1b5b
parentFinish report (diff)
Last changes
-rw-r--r--Makefile6
-rw-r--r--report.tex10
2 files changed, 6 insertions, 10 deletions
diff --git a/Makefile b/Makefile
index 477790f..e545cdf 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/report.tex b/report.tex
index 3c1172c..d229b95 100644
--- a/report.tex
+++ b/report.tex
@@ -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)$.