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
|
% vim: spelllang=nl:
\subsection{Bewijs}
\label{sec:analyse:proof}
We zullen het buitenste programma als beschreven op~\pageref{pgm:reverse} met
$P_1$ aanduiden, en het recursieve binnenste programma met $P_2$.
Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait,
oftewel: er is een afleidingsboom voor
$$
\trans
{P_1}{[s:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[s^R:\Nil]}{\emptystore}
$$
voor alle $s\in\String$, met
\begin{align*}
\lambda^R &= \lambda, \\
(c~s)^R &= s^R c.
\end{align*}
Het bewijs gaat in twee stappen. Eerst bewijzen we dat $P_2$ de eerste string
op de stack achter de omgedraaide versie van de tweede string op de stack
plaatst, en dat output. Dit wordt bewezen in \autoref{thm:p2}. Hiermee kunnen
we van $P_1$ bewijzen dat het de eerste string op de stack omgedraaid output.
Dit doen we in \autoref{thm:p1}.
\begin{thm}
{
Voor alle $s,t\in\String$ met $t\ne\lambda$ hebben we een afleidingsboom
voor
\normalfont
\belowdisplayskip=-1em
$$
\trans
{P_2}{[s:t:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[t^R~s:\Nil]}{\emptystore}.
$$
}
\label{thm:p2}
\begin{proof}[Bewijs]
Met inductie naar de lengte van $t$.
Inductiebasis: stel $t=c$, met $c$ een willekeurig karakter. In dit geval
krijgen we de boom in \autoref{fig:tree:bootstrap-base}. Hier is $c$ geen
variabele maar het werkelijke karakter \lit{c}. We kunnen \emph{CleanSmurf}
namelijk helaas nog niet vertellen dat een bepaalde variabele lengte $1$
heeft. Uit de afleidingsboom blijkt dat $c$ niet gebruikt wordt als naam in
de variable store, waardoor we ons geen zorgen hoeven te maken over
situaties waar $c$ gelijk is aan \'e\'en van de variabelenamen die we
gebruiken. Uit de boom in \autoref{fig:tree:bootstrap-base} volgt dus dat
bovenstaande stelling geldt voor $t$ van lengte $1$.
\medskip
Inductiestap: we nemen aan dat we een afleidingsboom hebben voor
\begin{equation}\tag{IH}\label{eq:p2:ih}
\trans
{P_2}{[s:t:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[t^R:s:\Nil]}{\emptystore}
\end{equation}
Vervolgens laten we zien dat we voor elke $c\in\Char$ ook een
afleidingsboom hebben voor
$$
\trans
{P_2}{[s:c~t:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[t^R~c~s:\Nil]}{\emptystore}.
$$
Ook hiervoor kunnen we \emph{CleanSmurf} gebruiken. Geven
we~\eqref{eq:p2:ih} mee als aanname, dan krijgen we de boom
in~\autoref{fig:tree:bootstrap-step}. Net zoals bij de inductiebasis moeten
we $c$ als letterlijk \lit{c} meegeven. Eenzelfde inspectie van de
boom wijst uit dat dit geen problemen oplevert met andere waarden voor $c$.
\medskip
Uit het principe van inductie naar de structuur van de string $t$ volgt nu
voor alle $s,t\in\String$ met $t\ne\lambda$ dat we een afleidingsboom
hebben voor
$$
\trans
{P_2}{[s:t:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[t^R~s:\Nil]}{\emptystore}.
$$
\end{proof}
\end{thm}
\begin{thm}
{
Voor alle $s\in\String$ hebben we een afleidingsboom voor
\normalfont
\belowdisplayskip=-1em
$$
\trans
{P_1}{[s:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[s^R:\Nil]}{\emptystore}.
$$
}
\label{thm:p1}
\begin{proof}[Bewijs]
We maken een gevalsonderscheiding over de structuur van $s$.
\begin{enumerate}[label={Geval \arabic*.},itemindent=1.5\parindent]
\item Stel $s=\lambda$. In dit geval hebben we geen enkele variabele. We
kunnen dus simpelweg een boom maken. Dit geeft de boom in
\autoref{fig:tree:lambda}, waaruit blijkt dat de stelling inderdaad
geldt voor $s=\lambda$:
$$
\trans
{P_1}{[\lambda:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[\lambda:\Nil]}{\emptystore}.
$$
\item Stel $s=c~t$. In dit geval gaat $P_1$ het recursieve binnenste
programma gebruiken. We maken dus een boom die het resultaat van
\autoref{thm:p2} als aanname mag gebruiken. Dit geeft de afleidingsboom
in \autoref{fig:tree:bootstrap}, waaruit blijkt dat de bovenstaande
stelling geldt voor alle $s\ne\lambda$.
\end{enumerate}
\end{proof}
\end{thm}
|
