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
|
% vim: set spelllang=nl:
\section{Analyse}
\label{sec:analyse}
Omdat de transities van onze natuurlijke semantiek input meenemen, kunnen we
alleen een afleidingsboom maken voor een programma \emph{met} een bepaalde
input. Het is dus niet triviaal mogelijk een afleidingsboom te maken voor
willekeurige input. In deze sectie willen we laten zien hoe het toch mogelijk
is een bewijs te leveren over een programma met een willekeurige input string,
door gebruik te maken van inductie naar de lengte van de input string. We
hadden hiervoor initieel een programma op de Esolang wiki gevonden dat een
string zou omdraaien~\cite{esolang:prog}. Dit programma werkte echter niet naar
behoren: het werkte niet voor strings met lengte $1$. Daarom hebben we zelf een
programma geschreven voor het omdraaien van een string. Dit programma ziet er
als volgt uit:
\begin{smurf}
\footnotesize
i "input" p
"input" g
"input" g q
"\textbackslash{}"\textbackslash{}"\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gh\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"g+\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gt
\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"g\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"v\textbackslash{}\textbackslash{}\textbackslash{}"gq\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"gq++\textbackslash{}\textbackslash{}\textbackslash{}"u\textbackslash{}\textbackslash{}\textbackslash{}"g+
\textbackslash{}\textbackslash{}\textbackslash{}"w\textbackslash{}\textbackslash{}\textbackslash{}"gp\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"pgx\textbackslash{}"\textbackslash{}"u\textbackslash{}"p\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gh\textbackslash{}"v\textbackslash{}"g+\textbackslash{}"v\textbackslash{}"p\textbackslash{}"w\textbackslash{}"gt\textbackslash{}"w\textbackslash{}"p\textbackslash{}"w\textbackslash{}"g\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+
\textbackslash{}"w\textbackslash{}"gq\textbackslash{}"v\textbackslash{}"gq\textbackslash{}"u\textbackslash{}"gq++\textbackslash{}"u\textbackslash{}"g+\textbackslash{}"w\textbackslash{}"gp\textbackslash{}"\textbackslash{}"pgx"
\\
+
"input" g p
"\textbackslash{}"\textbackslash{}"o" "" p
g x
\end{smurf}
Het bovenstaande programma is correcte Smurfsyntax en hierdoor niet erg
leesbaar. We hebben daarom getracht het programma iets leesbaarder te maken:
\input{reverse2}
\input{explanation}
\subsection{bewijs}
Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait,
oftewel: er is een afleidingsboom voor
$$
\trans
{Programma}{[s:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[s^R:\Nil]}{\st}
$$
voor alle s, waar
$$(c~s)^R=s^R c$$
$$\lambda^R=\lambda$$
Dit bewijs gaat in twee stappen.
$$
\trans
{Programma}{[c:s:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[s^R:c:\Nil]}{\st}
$$
Eerst bewijzen we aan de hand van inductie dat voor het recursieve binnenste programma geldt dat voor de stack met waarde $(s:t:\Nil)$ de output $(t^R: s^R: \Nil)$ zal zijn.
\bigskip
Ook wel
$$
\trans
{Programma}{[cs:g:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[g^R:cs:\Nil]}{\st}
$$
\begin{proof}[Bewijs]
\medskip
Met inductie naar de lengte van $g$.
Basisgeval: $g=\lambda$.
We moeten laten zien dat
$$
\trans
{Programma}{[s:c:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[cs:\Nil]}{\st}
$$
Dit volgt uit bewijsboom *referentie*
\bigskip
inductiestap: $g = t $ (t is een variabele)
We moeten laten zien dat
$$
\trans
{Programma}{[s:ct:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[t^R:cs:\Nil]}{\st}
$$
Met als inductiehypothese
$$
\trans
{Programma}{[cs:t:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[t^R:cs:\Nil]}{\st}
$$
Dit volgt uit bewijsboom * referentie*
\end{proof}
Vervolgens zullen we laten zien dat voor het buitenste programma geldt dat
$$
\trans
{Programma}{[s:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[s^R:\Nil]}{\st}
$$
Hierbij zullen we laten zien dat dit geldt voor zowel een lege input als een niet-lege input.
Hierbij mogen we natuurlijk gebruik maken van wat we hierboven bewezen hebben.
\medskip
Eerst zullen we laten zien dat het geldt voor een lege input
We zullen dus moeten laten zien dat:
$$
\trans
{Programma}{[\Nil:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[\Nil:\Nil]}{\st}
$$
Dit volgt direct uit bewijsboom *referentie*
Ten tweede zullen we laten zien dat het geldt voor een niet-lege input
We zullen dus moeten laten zien dat:
$$
\trans
{Programma}{[s:\Nil]}{(\Nil,\emptystore)}
{\Nil}{[s^t:\Nil]}{\st}
$$
Dit volgt uit de bewijsbomen *referentie* (3*)
|
