diff options
| m--------- | CleanSmurfProver | 0 | ||||
| -rw-r--r-- | cleansmurf-proofs.tex | 59 | ||||
| -rw-r--r-- | cleansmurf-rules.tex | 30 | ||||
| -rw-r--r-- | cleansmurf-trees.tex | 40 | ||||
| -rw-r--r-- | cleansmurf-types.tex | 43 | ||||
| -rw-r--r-- | cleansmurf.tex | 120 |
6 files changed, 178 insertions, 114 deletions
diff --git a/CleanSmurfProver b/CleanSmurfProver -Subproject 97325a5ef30b63c68adaffb69a0bcfa7f1135d6 +Subproject b7916c0e11abd630a59ccb67700e8814f903c68 diff --git a/cleansmurf-proofs.tex b/cleansmurf-proofs.tex new file mode 100644 index 0000000..47e5945 --- /dev/null +++ b/cleansmurf-proofs.tex @@ -0,0 +1,59 @@ +% vim: spelllang=nl: +\subsection{Hulp bij bewijzen} +\label{sec:cleansmurf:proofs} + +Omdat aan de linkerkant van Smurftransities niet alleen het programma en de +toestand, maar ook de input staat, heeft een Smurfprogramma voor iedere input +een andere afleidingsboom. Deze afleidingsbomen zijn vervolgens met +\emph{CleanSmurf} te genereren. Vaak zullen we echter uitspraken willen doen +die abstraheren van de input, zoals ``Voor iedere input $s_1:s_2:\Nil$ zal de +output $s_2:\Nil$ zijn.'' Hier kan \emph{CleanSmurf} niet mee overweg, wat het +een weinig behulpzame toepassing voor bewijshulp maakt. + +Een uitbreiding op \emph{CleanSmurf} implementeert een simplistische bewijshulp +die in sommige gevallen met variabelen overweg kan. Op dit moment is het een +\emph{proof of concept}. Sommige delen zijn nog niet geïmplementeerd. Wel is +het al bruikbaar in bepaalde gevallen, zoals we in \autoref{sec:analyse} zullen +zien. + +De oplossing hiervoor is complex. Waar hierboven de stack werd gemodelleerd met +een lijst van Strings, zal dit nu niet meer voldoende zijn: we moeten +onderscheid maken tussen \emph{literals} en \emph{bewijsvariabelen}. Voor de +duidelijkheid maken we vanaf nu onderscheid tussen variabelen (elementen op de +stack of in de variable store) en bewijsvariabelen (variabelen waar de +bewijshulp mee werkt). + +Combinaties van literals en bewijsvariabelen moeten ook voor kunnen komen (bv. +literal \lit{s} geconcateneerd met variabele $t$). Bovendien kunnen +bewijsvariabelen ook in een Smurfprogramma terechtkomen, omdat Smurf geen +duidelijk onderscheid kent tussen variabelen en Smurfprogramma's (middels +$\StmExec$ kan een variabele uitgevoerd worden). Dit laatste moet de bewijshulp +ten minste deels ondersteunen: variabelen komen al snel in programma's terecht +op het moment dat iteratie gewenst is. + +Om variabelen te modelleren definiëren we een nieuw type, \CI{Expr}: + +\lstinputlisting[firstline=15,lastline=20]{CleanSmurfProver/Smurf.dcl} + +Vervolgens vervangen we \CI{String} door \CI{Expr} in de definities van +\CI{Stm}, \CI{Stack} en \CI{Store}. + +Dit heeft gevolgen voor de \CI{step}-functie en zijn hulpfuncties. Waar we +eerst \CI{head} op een \CI{String} toepasten, doen we dat nu op een \CI{Expr}. +Deze functie moeten we dus herschrijven naar: + +\lstinputlisting[firstline=272,lastline=275]{CleanSmurfProver/Smurf.icl} + +Op deze manier kunnen we de head van een variabele nemen. Er wordt in dit geval +niet gecontroleerd of die variabele niet leeg is. Het is aan de gebruiker van +de bewijshulp dit na te gaan. Soortgelijke aanpassingen moeten we maken voor +andere functies. + +Helaas werkt de oude functie om een boom te maken, \CI{tree}, niet meer na deze +veranderingen: op een gegeven moment zal \CI{step} moeten weten wat de inhoud +van een bewijsvariabele is. + +Om dit op te lossen introduceren we \emph{bewijshints}. Dit zijn transities +waarvan we de bewijshulp vertellen dat hij mag aannemen dat die bestaan. De +\CI{prover}, de bewijshulp-variant van \CI{tree}, zal bomen slechts maken tot +het punt dat zo'n bewijshint gevonden wordt. diff --git a/cleansmurf-rules.tex b/cleansmurf-rules.tex new file mode 100644 index 0000000..2e71c12 --- /dev/null +++ b/cleansmurf-rules.tex @@ -0,0 +1,30 @@ +% vim: set spelllang=nl: +\subsection{Semantiekregels} +\label{sec:cleansmurf:regels} +Iedere semantiekregel vertaalt min of meer direct naar een functiealternatief +voor \CI{step}. Echter, omdat we geen \CI{run}- maar een \CI{step}-functie +schrijven, moeten we compositie expliciet maken. + +Als voorbeeld zullen we de implementatie van $\StmHead$ bekijken. Aangezien +\CI{pop} en \CI{head} allebei een \CI{Maybe} opleveren, kunnen we de resultaten +gemakkelijk binden. Vervolgens wordt de stack geüpdate en wordt de rest van het +programma (\CI{p}) teruggegeven. De IO-toestand wordt zonder gebruik +doorgegeven. Het vierde argument hebben we niet nodig en kan dus worden +genegeerd. + +\lstinputlisting[firstline=213,lastline=215]{CleanSmurf/Smurf.icl} + +Andere regels, voor $\StmPush$, $\StmTail$, $\StmCat$, $\StmQuotify$ en ook +$\StmPut$ en $\StmGet$ gaan op soortgelijke wijze. Ook $\StmInput$ en +$\StmOutput$ kunnen op dezelfde manier worden geschreven, afgezien van het feit +dat de IO-toestand en -functies gebruikt moeten worden. + +In het geval van $\StmExec$ kunnen we handig gebruik maken van het feit dat +\CI{step} een nieuw programma oplevert: + +\lstinputlisting[firstline=228,lastline=230]{CleanSmurf/Smurf.icl} + +Zoals te zien wordt een nieuwe toestand gemaakt (\CI{zero}) waarin dit nieuwe +programma (\CI{p}) wordt uitgevoerd. De compositie \CI{parse o fromString} +parseert een String van de stack en levert een \CI{Maybe Program} op. Dus ook +deze wat afwijkende regel levert geen problemen op. diff --git a/cleansmurf-trees.tex b/cleansmurf-trees.tex new file mode 100644 index 0000000..6264697 --- /dev/null +++ b/cleansmurf-trees.tex @@ -0,0 +1,40 @@ +% vim: set spelllang=nl: +\subsection{Afleidingsbomen} +Door herhaaldelijk gebruik te maken van \CI{step} kunnen we gemakkelijk een +afleidingsboom genereren. We maken hierbij gebruik van een aantal handige +eigenschappen van afleidingsbomen voor Smurf: + +\begin{itemize} + \item Alle semantiekregels hebben ten hoogste één premisse, waardoor we een + boom als lijst van transities kunnen representeren. + \item Ieder commando heeft precies één regel. Hierdoor is aan het eerste + statement van een programma te herkennen welke regel wordt toegepast. Dit + hoeven we dus niet in de types \CI{Transition} en \CI{DerivationTree} op te + slaan. + \item Doordat condities van de semantiekregels enkel afhangen van de + linkerkant van de conclusie (het programma, de input en de toestand), en + deze informatie beschikbaar is op het moment dat de boom gemaakt wordt, + hoeven we geen backtracking toe te passen. Wanneer het niet lukt de regel + die bij het eerste commando van het programma hoort toe te passen, weten we + zeker dat er geen afleidingsboom bestaat. +\end{itemize} + +De functie \CI{tree} is als volgt geïmplementeerd: + +\lstinputlisting[firstline=274]{CleanSmurf/Smurf.icl} + +Bij het genereren van bomen leggen we de input van te voren vast in een lijst. +We slaan de output op in een andere lijst. Dit is wat het type \CI{ListIO} +inhoudt --- de implementatie hiervan is irrelevant hier. + +Het eerste dat \CI{tree} doet is het berekenen van de volgende stap. Lukt dat +niet (\CI{isNothing mbPgmSt}), dan kunnen we ook geen boom maken. + +Omdat \CI{step} voor een leeg programma een nieuw leeg programma oplevert, +moeten we in deze functie controleren of het nieuwe programma leeg is. Is dit +het geval, dan zetten we de $\lambda$-regel zelf in de boom als \CI{([], +io.input, st) --> (io.input, [], st)}. + +Is dit niet het geval, dan maken we recursief een boom voor de premisse +(\CI{tree pgm st io iof}). Lukt dit niet, dan kunnen we geen boom maken. +Anders, dan voegen we de boom en de transitie gevonden met \CI{step} samen. diff --git a/cleansmurf-types.tex b/cleansmurf-types.tex new file mode 100644 index 0000000..bed29e2 --- /dev/null +++ b/cleansmurf-types.tex @@ -0,0 +1,43 @@ +% vim: set spelllang=nl: +\subsection{Types} +\label{sec:cleansmurf:types} +Het programma houdt de expressieve syntax uit \autoref{sec:def:syn} aan. Het +type \CI{Stm} is dus: + +\lstinputlisting[firstline=15,lastline=20]{CleanSmurf/Smurf.dcl} + +We gebruiken lijsten als stacks en implementeren de store met behulp van een +tabel van naam-waarde paren: + +\lstinputlisting[firstline=22,lastline=27]{CleanSmurf/Smurf.dcl} + +Ten slotte definiëren we transities. Aangezien alle semantiekregels hooguit één +premisse hebben, kunnen we een afleidingsboom als lijstje transities zien: + +\lstinputlisting[firstline=35,lastline=36]{CleanSmurf/Smurf.dcl} + +Met deze definities kunnen we een \CI{step :: Program State -> Maybe (Program, +State)} definiëren. Dit komt bijna overeen met de structuur van transities. We +moeten een \CI{Program} teruggeven, omdat we slechts één stap zetten. Wat dit +betreft lijken de regels van \emph{CleanSmurf} meer op regels in structurele +operationele semantiek. We hebben al laten zien dat deze regels erg veel lijken +op die in natuurlijke semantiek. + +Het type van \CI{step} neemt nog geen Input/Output mee. We maken er een +overloaded functie van, zodat hij voor meerdere inputmethodes kan worden +gebruikt. Het uiteindelijke type is: + +\lstinputlisting[firstline=56,lastline=56]{CleanSmurf/Smurf.dcl} + +Hoe dit precies werkt is niet belangrijk voor de beschrijving hier. Het derde +argument, van type \CI{io}, is de `IO-toestand'. Het vierde argument, van type +\CI{IO io}, omvat een input-functie die strings oplevert (gegeven de +IO-toestand) en een output-functie die strings opneemt (in de IO-toestand). + +\medskip +Verder definiëren we een aantal hulpfuncties: + +\lstinputlisting[firstline=232,lastline=245]{CleanSmurf/Smurf.icl} + +De partiële functies zijn hier gesimuleerd met het \CI{Maybe}-type. Dit laat +ons monadische operatoren gebruiken in het uitwerken van de interpreter. diff --git a/cleansmurf.tex b/cleansmurf.tex index 24011bf..2958399 100644 --- a/cleansmurf.tex +++ b/cleansmurf.tex @@ -2,122 +2,14 @@ \section{CleanSmurf} \label{sec:cleansmurf} -Semantiekregels vertalen zich uiterst gemakkelijk naar een implementatie van -een interpreter in een functionele taal. \emph{CleanSmurf}~\cite{cleansmurf} is +Semantiekregels laten zich uiterst gemakkelijk vertalen naar een implementatie +van de taal in een functionele stijl. \emph{CleanSmurf}~\cite{cleansmurf} is een interpreter voor Smurf, geschreven in Clean, dat onze semantiekregels volgt. Omdat het de semantiekregels volgt, was het niet lastig dit uit te breiden naar een programma dat een afleidingsboom genereert. In dit hoofdstuk beschrijven we de globale opzet van dit programma. -\subsection{Types} -\label{sec:cleansmurf:types} -Het programma houdt de expressieve syntax uit \autoref{sec:def:syn} aan. Het -type \CI{Stm} is dus: - -\lstinputlisting[firstline=15,lastline=20]{CleanSmurf/Smurf.dcl} - -We gebruiken lijsten als stacks en implementeren de store met behulp van een -tabel van naam-waarde paren: - -\lstinputlisting[firstline=22,lastline=27]{CleanSmurf/Smurf.dcl} - -Ten slotte definiëren we transities. Aangezien alle semantiekregels hooguit één -premisse hebben, kunnen we een afleidingsboom als lijstje transities zien: - -\lstinputlisting[firstline=35,lastline=36]{CleanSmurf/Smurf.dcl} - -Met deze definities kunnen we een \CI{step :: Program State -> Maybe (Program, -State)} definiëren. Dit komt bijna overeen met de structuur van transities. We -moeten een \CI{Program} teruggeven, omdat we slechts één stap zetten. Wat dit -betreft lijken de regels van \emph{CleanSmurf} meer op regels in structurele -operationele semantiek. We hebben al laten zien dat deze regels erg veel lijken -op die in natuurlijke semantiek. - -Het type van \CI{step} neemt nog geen Input/Output mee. We maken er een -overloaded functie van, zodat hij voor meerdere inputmethodes kan worden -gebruikt. Het uiteindelijke type is: - -\lstinputlisting[firstline=56,lastline=56]{CleanSmurf/Smurf.dcl} - -Hoe dit precies werkt is niet belangrijk voor de beschrijving hier. Het derde -argument, van type \CI{io}, is de `IO-toestand'. Het vierde argument, van type -\CI{IO io}, omvat een input-functie die strings oplevert (gegeven de -IO-toestand) en een output-functie die strings opneemt (in de IO-toestand). - -\medskip -Verder definiëren we een aantal hulpfuncties: - -\lstinputlisting[firstline=232,lastline=245]{CleanSmurf/Smurf.icl} - -De partiële functies zijn hier gesimuleerd met het \CI{Maybe}-type. Dit laat -ons monadische operatoren gebruiken in het uitwerken van de interpreter. - -\subsection{Semantiekregels} -\label{sec:cleansmurf:regels} -Iedere semantiekregel vertaalt min of meer direct naar een functiealternatief -voor \CI{step}. Echter, omdat we geen \CI{run}- maar een \CI{step}-functie -schrijven, moeten we compositie expliciet maken. - -Als voorbeeld zullen we de implementatie van $\StmHead$ bekijken. Aangezien -\CI{pop} en \CI{head} allebei een \CI{Maybe} opleveren, kunnen we de resultaten -gemakkelijk binden. Vervolgens wordt de stack geüpdate en wordt de rest van het -programma (\CI{p}) teruggegeven. De IO-toestand wordt zonder gebruik -doorgegeven. Het vierde argument hebben we niet nodig en kan dus worden -genegeerd. - -\lstinputlisting[firstline=213,lastline=215]{CleanSmurf/Smurf.icl} - -Andere regels, voor $\StmPush$, $\StmTail$, $\StmCat$, $\StmQuotify$ en ook -$\StmPut$ en $\StmGet$ gaan op soortgelijke wijze. Ook $\StmInput$ en -$\StmOutput$ kunnen op dezelfde manier worden geschreven, afgezien van het feit -dat de IO-toestand en -functies gebruikt moeten worden. - -In het geval van $\StmExec$ kunnen we handig gebruik maken van het feit dat -\CI{step} een nieuw programma oplevert: - -\lstinputlisting[firstline=228,lastline=230]{CleanSmurf/Smurf.icl} - -Zoals te zien wordt een nieuwe toestand gemaakt (\CI{zero}) waarin dit nieuwe -programma (\CI{p}) wordt uitgevoerd. De compositie \CI{parse o fromString} -parseert een String van de stack en levert een \CI{Maybe Program} op. Dus ook -deze wat afwijkende regel levert geen problemen op. - -\subsection{Afleidingsbomen} -Door herhaaldelijk gebruik te maken van \CI{step} kunnen we gemakkelijk een -afleidingsboom genereren. We maken hierbij gebruik van een aantal handige -eigenschappen van afleidingsbomen voor Smurf: - -\begin{itemize} - \item Alle semantiekregels hebben ten hoogste één premisse, waardoor we een - boom als lijst van transities kunnen representeren. - \item Ieder commando heeft precies één regel. Hierdoor is aan het eerste - statement van een programma te herkennen welke regel wordt toegepast. Dit - hoeven we dus niet in de types \CI{Transition} en \CI{DerivationTree} op te - slaan. - \item Doordat condities van de semantiekregels enkel afhangen van de - linkerkant van de conclusie (het programma, de input en de toestand), en - deze informatie beschikbaar is op het moment dat de boom gemaakt wordt, - hoeven we geen backtracking toe te passen. Wanneer het niet lukt de regel - die bij het eerste commando van het programma hoort toe te passen, weten we - zeker dat er geen afleidingsboom bestaat. -\end{itemize} - -De functie \CI{tree} is als volgt geïmplementeerd: - -\lstinputlisting[firstline=274]{CleanSmurf/Smurf.icl} - -Bij het genereren van bomen leggen we de input van te voren vast in een lijst. -We slaan de output op in een andere lijst. Dit is wat het type \CI{ListIO} -inhoudt --- de implementatie hiervan is irrelevant hier. - -Het eerste dat \CI{tree} doet is het berekenen van de volgende stap. Lukt dat -niet (\CI{isNothing mbPgmSt}), dan kunnen we ook geen boom maken. - -Omdat \CI{step} voor een leeg programma een nieuw leeg programma oplevert, -moeten we in deze functie controleren of het nieuwe programma leeg is. Is dit -het geval, dan zetten we de $\lambda$-regel zelf in de boom als \CI{([], -io.input, st) --> (io.input, [], st)}. - -Is dit niet het geval, dan maken we recursief een boom voor de premisse -(\CI{tree pgm st io iof}). Lukt dit niet, dan kunnen we geen boom maken. -Anders, dan voegen we de boom en de transitie gevonden met \CI{step} samen. +\input{cleansmurf-types} +\input{cleansmurf-rules} +\input{cleansmurf-trees} +\input{cleansmurf-proofs} |