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
|
% 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, door gebruik te maken
van inductie naar de lengte van de input. We doen dit aan de hand van een
programma dat een string omdraait~\cite{esolang:prog}:
\begin{smurf}
\footnotesize
"+"i+ ""p ""gtg ""gt "i"p\\
"\textbackslash{}"\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gh\textbackslash{}"o\textbackslash{}"g+\textbackslash{}"o\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gt\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"tg\textbackslash{}"+\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\\
\textbackslash{}"i\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"o\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"\textbackslash{}"gq+\textbackslash{}"\textbackslash{}"g+\textbackslash{}"\textbackslash{}"p\textbackslash{}"o\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+\textbackslash{}"+\textbackslash{}"pgx"\\
""p "\textbackslash{}"+\textbackslash{}"\textbackslash{}"\textbackslash{}"p" "i"gq+ "tg"+ "i"gq+\\
"\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}""+ ""gq+ ""g+ ""p "" "+" "i"g+ pgx
\end{smurf}
Omgezet naar onze leesbare (hier een relatief begrip) syntax ziet de code er zo
uit:
%todo leesbaarheid betekent ook witregels waar logisch
\begin{smurf}
\footnotesize
\StmPush~"+"~:
\StmInput~:
\StmCat~:
\StmPush~$\lambda$~:
\StmPut~:
\StmPush~$\lambda$~:
\StmGet~:
\StmTail~:\\
\StmGet~:
\StmPush~$\lambda$~:
\StmGet~:
\StmTail~:
\StmPush~"i"~:
\StmPut~:\\
\StmPush~"\textbackslash{}"\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gh\textbackslash{}"o\textbackslash{}"g+\textbackslash{}"o\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gt\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"tg\textbackslash{}"+\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\\
\textbackslash{}"i\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"o\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"\textbackslash{}"gq+\textbackslash{}"\textbackslash{}"g+\textbackslash{}"\textbackslash{}"p\textbackslash{}"o\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+\textbackslash{}"+\textbackslash{}"pgx"~:\\
\StmPush~$\lambda$~:
\StmPut~:
\StmPush~"\textbackslash{}"+\textbackslash{}"\textbackslash{}"\textbackslash{}"p"~:\\
\StmPush~"i"~:
\StmGet~:
\StmQuotify~:
\StmCat~:
\StmPush~"tg"~:
\StmCat~:
\StmPush~"i"~:
\StmGet~:
\StmQuotify~:
\StmCat~:
\StmPush~"\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}""~:
\StmCat~:
\StmPush~$\lambda$~:
\StmGet~:
\StmQuotify~:
\StmCat~:
\StmPush~$\lambda$~:
\StmGet~:
\StmCat~:
\StmPush~$\lambda$~:
\StmPut~:
\StmPush~$\lambda$~:
\StmPush~"+"~:
\StmPush~"i"~:
\StmGet~:
\StmCat~:
\StmPut~:
\StmGet~:
\StmExec~:
$\lambda$
\end{smurf}
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$$
\begin{proof}[Bewijs]
Met inductie naar de lengte van $s$.
Basisgeval: $s=\lambda$.
$$%Todo fix dit
\begin{prooftree}
\[
\[
\[
\[
\vdots %todo afmaken
\justifies
\trans
{\StmPut : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
{\Nil}{\lambda}{\st}
\using{\rputns}
\]
\justifies
\trans
{\StmPush~\lambda : \StmPut : ...~}{\Nil}{(["+":\Nil], \emptystore)}
{\Nil}{\lambda}{\st}
\using{\rpushns}
\]
\justifies
\trans
{\StmCat : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
{\Nil}{\lambda}{\st}
\using{\rcatns}
\]
\justifies
\trans
{\StmInput : \StmCat : ...~}{[\lambda:\Nil]}{(["+":\Nil], \emptystore)}
{\Nil}{\lambda}{\st}
\using{\rinputns}
\]
\justifies
\trans
{\StmPush~"+" : \StmInput : ...~}{[\lambda:\Nil]}{(\Nil,\emptystore)}
{\Nil}{\lambda}{\st}
\using{\rpushns}
\end{prooftree}
$$
%FIXME
NB: dit bewijs is overduidelijk niet af. We gaan de afleidingsboom
automatisch genereren, dit is nog maar een begin. Het programma, dat van de
Esolang wiki afkomstig is~\cite{esolang:prog}, werkt helaas niet voor strings
met minder dan twee karakters. In het geval van de lege string wordt geen
output gegeven; in het geval van een string van één karakter crasht het
programma. We zullen ofwel dit programma aanpassen, zodat het wel werkt,
ofwel een ander programma bekijken. In het laatste geval zullen we nog steeds
een programma nemen waar we iets inductief over kunnen bewijzen, zoals het
laatste voorbeeld uit \autoref{sec:intro:exmp}.
%todo afmaken
\end{proof}
|
