\documentclass[10pt]{article} \usepackage{latexsym,amssymb,amsmath,theorem,proof,calc,alltt} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % VERSION July 1999 % % % % modified for Hugs98 % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \setlength{\textheight}{22cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\parindent}{0 ex} \setlength{\parskip}{1.5 ex} \newcommand{\commentout}[1]{} \newcommand{\unknown}{\mbox{$\bullet$}} \newcommand{\funknown}{\mbox{$\bullet'$}} \newcommand{\fullbot}{\diamondsuit} \newcommand{\error}{\mbox{\it error}} \newcommand{\fail}{\mbox{\it fail}} \newcommand{\dom}{{\it dom}} \newcommand{\arrow}[1]{{\stackrel{#1}{\longrightarrow}}} \newcommand{\df}{{\it df}} \newcommand{\da}{{\it da}} \newcommand{\os}{{\it os}} \newcommand{\var}{{\it var}} \newcommand{\boA}{{\textbf A}} \newcommand{\bB}{{\textbf B}} \newcommand{\ab}{{\textbf a}} \newcommand{\bb}{{\textbf b}} \newcommand{\bc}{{\textbf c}} \newcommand{\ri}{N} \newcommand{\rn}{{\rm n}} \newcommand{\sass}{\blacktriangleleft} \newcommand{\rsass}{\blacktriangleright} \newcommand{\pre}{\triangleright} \newcommand{\post}{\triangleleft} \newcommand{\Nat}{\mathbb{N}} \newcommand{\Int}{\mathbb{Z}} \newcommand{\NI}{\noindent} \newcommand{\lda}{\lbrack\!\{} \newcommand{\rda}{\}\!\rbrack} \newcommand{\ldb}{\lbrack\!\lbrack} \newcommand{\rdb}{\rbrack\!\rbrack} \newcommand{\ltb}{\lbrack\!\lbrack\!\lbrack} \newcommand{\rtb}{\rbrack\!\rbrack\!\rbrack} \newcommand{\ldc}{\lbrack\!(} \newcommand{\rdc}{)\!\rbrack} \newcommand{\ltc}{\lbrack\!(\!(} \newcommand{\rtc}{)\!)\!\rbrack} \newcommand{\M}{{\cal M}} \newcommand{\m}{{M_?}} \newcommand{\X}{{\cal X}} \newcommand{\bA}{\mathbb{A}} \newcommand{\A}{{\cal A}} \newcommand{\impl}{\rightarrow} \newcommand{\conc}{\hat{\ }} \newcommand{\mi}[1]{\mbox{\it #1}} \newcommand{\negmod}{\mbox{$\:=\!\!\!|\,$}} \newcommand{\LA}{\langle} \newcommand{\RA}{\rangle} \newcommand{\pow}{{\cal P}} \newcommand{\sref}[1]{(\ref{#1})} \newcommand{\bcform}{\cup^{v}_{M..N} \phi} \newcommand{\BCform}{\bigcup^{v}_{M..N} \phi} \newtheorem{theorem}{Theorem} \newtheorem{definition}[theorem]{Definition} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{fact}[theorem]{Fact} \newtheorem{lemma}[theorem]{Lemma} \newenvironment{proof}{\noindent \bf Proof. \ \rm}{\hfill $\Box$} \newsavebox{\fminibox} \newlength{\fminilength} \newenvironment{fminipage}[1][\linewidth] {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}% \bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip} {\smallskip\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}\bigskip} \newenvironment{code}{\begin{fminipage}\begin{alltt}}% {\end{alltt}\end{fminipage}} \newenvironment{Ccode}{\begin{fminipage}\begin{alltt} COMMENTED OUT}% {\end{alltt}\end{fminipage}} \newcommand{\putline}{\rule{\linewidth}{0.1ex}} \newcommand{\rw}[1]{\mbox{\tt #1}} \newcommand{\dyn}{{\em dynamo}\/} \title{Dynamo --- A Language for Dynamic Logic Programming} \author{Jan van Eijck} \date{} \begin{document} \maketitle \begin{abstract} \noindent We describe a Haskell \cite{HudFasPet:agith,Haskell:rep} prototype implementation of {\em dynamo}, a simple language for dynamic logic programming. In the execution mechanism that we implement tests are always executed at once. If a test cannot be performed because values for some of its variables are missing, a transition to the `don't know' state is made. This is the version of {\em dynamo}\/ that is described in \cite{Eijck:pwdpl}. An improvement on this rather crude execution behaviour is proposed in \cite{EijHeg:dwch}. \end{abstract} \section{Dynamic Logic Programming} Dynamic logic programming was introduced in Van Eijck \cite{Eijck:pwdpl}. This paper describes a first implementation of \dyn, a language for pure dynamic logic programming. The \dyn\ language implements the executable process interpretation of Dynamic Predicate Logic or DPL \cite{GroSto:dpl}, augmented with constructs for bounded iteration and bounded choice, as described in \cite{Eijck:pwdpl}. The two main sources of inspiration for \dyn\ are DPL and {\em Alma-0}, a hybrid language for imperative programming mixed with logic programming developed by Apt c.s. \cite{AptCS:aail}. The \dyn\ language demonstrates that dynamic interpretation of FOL can be used as guideline for dynamic logic programming. \dyn\ programs have a purely declarative dynamic semantics. There are no side effects, and no control features: \dyn\ is pure dynamic logic. Because of this logical purity, weakest precondition reasoning for \dyn\ is completely straightforward. \section{Executable Interpretation of FOL} Let a domain $M$ and a set of variables $V$ be given. Let $\A := \bigcup_{X \subseteq V} M^X$, let $\epsilon$ be the empty partial valuation (the only member of $M^\emptyset$), and let $\unknown$ be an object not in $\A$. If $a \in M^X$, for $X\subseteq V$, then a term $t$ is $a$-closed if all variables in $t$ are in $X$, an atom $P t_1 \cdots t_n$ is $a$-closed if all $t_i$ are $a$-closed, and an identity $t_1 \doteq t_2$ is $a$-closed if both of $t_1, t_2$ are. If $a \in M^X$ we call $X$ the domain of $a$. Use $\uparrow$ for `undefined' and $\downarrow$ for `defined'. Term interpretation in a (First Order) model $\M = (M,I)$ wrt valuation $a$: \[ \begin{array}{lll} v^a & := & \left\{ \begin{array}{ll} a(v) & \mbox{ if } v \mbox{ is } a\mbox{-closed} \\ \uparrow & \mbox{ otherwise } \end{array} \right. \\ (f t_1 \cdots t_n)^a & := & \left\{ \begin{array}{ll} I(f) t_1^a \cdots t_n^a & \mbox{ if } t_1, \ldots, t_n \ a\mbox{-closed} \\ \uparrow & \mbox{ otherwise } \end{array} \right. \end{array} \] An identity $t_1 \doteq t_2$ is an $a$-assignment if either $t_1 \equiv v$, $t_1^a = \uparrow$, $t_2^a = \downarrow$, or $t_2 \equiv v$, $t_1^a = \downarrow$, $t_2^a = \uparrow$. \paragraph{Executable Interpretation of Negation} Treatment of negation should be phrased in terms of the so-called forward property: \begin{itemize} \item If $a \arrow{\phi} b$ and $a \subseteq a'$, then there is a $b' \supseteq b$ with $a' \arrow{\phi} b'$. \end{itemize} {\bf Solution}\/: Keep track of variables relevant to a particular path taken by the computation. Two distinguished registers: \begin{itemize} \item $g$ for the set of {\em global}\/ variables that get assigned along a computation path (global variables are dynamically free variables), \item $l$ for the set of {\em local}\/ variables that get declared and possibly assigned along a computation path (local variables are dynamically active variables). \end{itemize} A proper state is a triple consisting of a valuation $a \in \A$, a global store $g^a \subseteq V$, and a local store $l^a \subseteq V$. The improper state is the item $\unknown$. We say that a transition $(a,g^a,l^a) \ \arrow{\phi} \ (b, g^b, l^b)$ has the forward property if $l^a \cup g^b \subseteq \dom(a)$, or equivalently, if $l^a \subseteq \dom(a)$ and $g^a = g^b$. We say that $\bb$ is safe for $(a,g^a,l^a)$ if $\bb = (b, g^b, l^b)$ (i.e., $\bb \neq \unknown$), $l^a \subseteq \dom(a)$ and $g^a = g^b$. We say that $\bB \subseteq (\pow \A \times \pow V \times \pow V) \cup \{ \unknown \}$ is risky for $(a,g^a,l^a)$ if $\bB \neq \emptyset$, but no member of $\bB$ is safe for $(a,g^a,l^a)$. The transition rules for negation are the following: \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{\neg \phi} \ (a,g^a,l^a)} {\mbox{not }(a,g^a,l^a) \ \arrow{\phi}\ \unknown, \mbox{ and there are no } b,g^b,l^b \mbox{ with } \ (a,g^a,l^a)\ \arrow{\phi} \ (b,g^b,l^b)} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{\neg \phi} \ \unknown } {\mbox{there are } \arrow{\phi} \mbox{ transitions for }(a,g^a,l^a), \mbox{ but none of them safe for } (a,g^a,l^a)} \end{center} \paragraph{Propagation of $\unknown$} \begin{center} \mbox{} \infer{\unknown \ \arrow{\phi}\ \unknown}{\mbox{}} \end{center} \paragraph{Executable Interpretation of Atomic Tests} \begin{center} \mbox{} \mbox{ no } $\arrow{\bot}$ \mbox{ transitions from } $(a,g^a,l^a)$ \end{center} \begin{center} \mbox{} \infer{(a,g^a,l^a) \ \arrow{Pt_1\cdots t_n} \ (a,g^a,l^a)} {Pt_1\cdots t_n \ a\mbox{-closed and } (t^a_1, \ldots, t^a_n) \in I(P)} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{Pt_1\cdots t_n} \ \unknown} {Pt_1\cdots t_n \ \mbox{ not }a\mbox{-closed}} \end{center} \paragraph{Executable Interpretation of Identities} \begin{center}\mbox{} \infer{(a,g^a ,l^a) \ \arrow{t_1\doteq t_a} \ (a,g^a,l^a)} {t_1\doteq t_2 \ a\mbox{-closed and } t^a_1 = t^a_2} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{t_1\doteq t_a} \ (a \cup \{ v/t^a_2 \}, g^a, l^a)} {t_1 \doteq t_2 \mbox{ an $a$-assignment with } t_1 \equiv v, v^a = \uparrow, t_2^a = \downarrow, v \in l^a} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{t_1\doteq t_a} \ (a \cup \{ v/t^a_2 \}, g^a \cup \{ v \}, l^a)} {t_1 \doteq t_2 \mbox{ an $a$-assignment with } t_1 \equiv v, v^a = \uparrow, t_2^a = \downarrow, v \notin l^a} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{t_1\doteq t_a} \ (a \cup \{ v/t^a_1 \}, g^a, l^a)} {t_1 \doteq t_2 \mbox{ an $a$-assignment with } t_2 \equiv v, v^a = \uparrow, t_1^a = \downarrow, v \in l^a} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{t_1\doteq t_a} \ (a \cup \{ v/t^a_1 \}, g^a \cup \{ v \}, l^a)} {t_1 \doteq t_2 \mbox{ an $a$-assignment with } t_2 \equiv v, v^a = \uparrow, t_1^a = \downarrow, v \notin l^a} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{t_1\doteq t_a} \ \unknown } {t_1 \doteq t_2 \mbox{ not an $a$-assignment and not $a$-closed}} \end{center} \paragraph{Executable Interpretation of Quantification} \begin{center}\mbox{} \infer{(a,g^a,l^a) \ \arrow{\exists v} \ (a, g^a, l^a \cup \{ v \})} {v \notin \dom(a)} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a)\ \arrow{\exists v} \ (a - \{ v/v^a \}, g^a, l^a \cup \{ v \})} {v \in \dom(a) } \end{center} \paragraph{Executable Interpretation of Composition} \begin{center} \mbox{} \infer{(a,g^a,l^a)\ \arrow{\phi_1; \phi_2} \ \unknown} {(a,g^a,l^a) \ \arrow{\phi_1} \ \unknown} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a)\ \arrow{\phi_1; \phi_2} \ \unknown} {(a,g^a,l^a) \ \arrow{\phi_1} \ (b,g^b,l^b) \ \ \ \ \ \ (b,g^b,l^b) \ \arrow{\phi_2}\ \unknown} \end{center} \begin{center}\mbox{} \infer{(a,g^a,l^a)\ \arrow{\phi_1; \phi_2} \ (c,g^c,l^c)} {(a,g^a,l^a) \ \arrow{\phi_1} \ (b,g^b,l^b)\ \ \ \ \ \ (b,g^b,l^b)b \ \arrow{\phi_2}\ (c,g^c,l^c)} \end{center} \paragraph{Exec Interpretation of Union} \begin{center}\mbox{} \infer[i \in \{ 1,2\}]{(a,g^a,l^a) \ \arrow{\phi_1 \cup \phi_2} \ \unknown} {(a,g^a,l^a)a \ \arrow{\phi_i} \ \unknown} \end{center} \begin{center}\mbox{} \infer[i \in \{ 1,2\}]{(a,g^a,l^a) \ \arrow{\phi_1 \cup \phi_2} \ (b,g^b,l^b)} {(a,g^a,l^a) \ \arrow{\phi_i} \ (b,g^b,l^b)} \end{center} \paragraph*{Executable Interpretation of Bounded Iteration} We want to be able to execute a formula $\phi$ $N$ times, where the value of $N$ possibly depends on previous computation. In other words: we want to be able to perform bounded iteration, with the bound not fixed at compile time, but only at run time. Assuming we have a type for nonnegative integer expressions, and $N$ is an expression of that type, we can write this as $\phi^N$. Assuming that $n$ is a natural number, we write $\phi^n$ for: execute $\phi$ $n$ times. Note the difference between $\phi^n$ and $\phi^N$ caused by the fact that $n$ is a number and $N$ a numerical expression. The executable interpretation of $\phi^n$ and $\phi^N$ is given by the following transition rules: \begin{center}\mbox{} \infer{\ab \ \arrow{\phi^0} \ \ab}{\mbox{}} \hspace{3em} \infer{\ab\ \arrow{\phi^{n+1}} \ \unknown} {\ab \ \arrow{\phi} \ \unknown} \hspace{3em} \infer{\ab\ \arrow{\phi^{n+1}} \ \unknown} {\ab \ \arrow{\phi} \ \bb \ \ \ \ \ \bb \ \arrow{\phi^n}\ \unknown} \end{center} \begin{center}\mbox{} \infer{\ab \ \arrow{\phi^{n+1}} \ \bc} {\ab \ \arrow{\phi} \ \bb\ \ \ \ \ \ \bb \ \arrow{\phi^n}\ \bc} \end{center} \begin{center}\mbox{} \infer[\ri^a = \uparrow]{\ab\ \arrow{\phi^{\ri}} \ \unknown}{\mbox{}} \hspace{3em} \infer[\ri^a = \downarrow, \max(0,\ri^a) = n] {\ab\ \arrow{\phi^{\ri}} \ \unknown} {\ab\ \arrow{\phi^{n}} \ \unknown} \end{center} \begin{center}\mbox{} \hspace{1em} \infer[\ri^a = \downarrow, \max(0,\ri^a) = n] {\ab\ \arrow{\phi^{\ri}} \ \bb} {\ab\ \arrow{\phi^{n}} \ \bb} \end{center} \paragraph*{Executable Interpretation of Bounded Choice} Suppose we want to check whether program $\phi$ succeeds for any $i$ in a bounded range of possibilities, say $M..N$. Again, we don't want to fix the values of $M$ and $N$ in advance, but let them be computed. For this, we add a new construct to the language, by introducing formulas of the form $\bcform$, with the following transition rules: \begin{center}\mbox{} \infer[M^a = \uparrow]{\ab\ \arrow{\bcform} \ \unknown}{\mbox{}} \hspace{3em} \infer[N^a = \uparrow]{\ab\ \arrow{\bcform} \ \unknown}{\mbox{}} \end{center} \begin{center}\mbox{} \infer[M^a = m, N^a = n, m \leq j \leq n] {\ab \ \arrow{\bcform} \ \unknown} {\ab \ \arrow{v_i = j; \phi} \ \unknown} \end{center} \begin{center}\mbox{} \infer[M^a = m, N^a = n, m \leq j \leq n] {\ab \ \arrow{\bcform} \ \bb} {\ab \ \arrow{v_i = j; \phi} \ \bb} \end{center} \section{Checks on the Executable Process Definition} The following facts about the executable interpretation of FOL are proved in \cite{Eijck:pwdpl}: \begin{itemize} \item Comp is associative: $ \ab \ \arrow{\phi_1;(\phi_2;\phi_3)} \ \bb \mbox{ iff } \ab \ \arrow{(\phi_1;\phi_2);\phi_3} \ \bb$. \item $l^a \subseteq \dom(a)$ and $g^a = g^b$ together guarantee the forward property for $(a,g^a,l^a) \ \arrow{\phi} \ (b,g^b,l^b)$. \item Executable interpretation is faithful to DPL in the following sense: \begin{itemize} \item If $(a,g^a,l^a) \ \arrow{\phi} \ (b,g^b,l^b)$ then there are full extensions $a',b'$ with $b' \in \ldc \phi \rdc(a')$. \item If there are no $\phi$-transitions from $(a,g^a,l^a)$, then for every full extension $a'$ of $a$ it holds that $\ldc \phi \rdc(a') = \emptyset$. \end{itemize} \end{itemize} \section{Assignment Without Sting} In dynamic logic programming, destructive assignment is replaced by safe assignment. Write $\exists j; j = i; \exists i; i = t$ as: \[ i \sass_j t. \] Destructive assignment statement $x := x+1$ can be replaced by safe assignment statement $x \sass_{x'} x'+1$. General procedure for removing the sting from assignment: \[ \begin{array}{lll} (x := t)^\heartsuit & := & \left\{ \begin{array}{ll} \exists x; x = t & \mbox{ if } x \mbox{ does not occur in } t, \\ x \sass_{x'} t[x'/x] & \mbox{ otherwise.} \end{array} \right. \end{array} \] In \dyn, $x \sass_y t$ is written as \verb^x >> y = t^. \section{Extended DPL Syntax Versus Dynamo Syntax} \newcommand{\ddonot}{\mbox{\tt donot\ }} \newcommand{\ddo}{\mbox{\tt do\ }} \newcommand{\dbegin}{\mbox{\tt begin\ }} \newcommand{\dend}{\mbox{\tt\ end}} \newcommand{\dfind}{\mbox{\tt find\ }} \newcommand{\din}{\mbox{\tt\ in\ }} \newcommand{\dwith}{\mbox{\tt\ with\ }} \newcommand{\dtimes}{\mbox{\tt\ times\ }} \newcommand{\deither}{\mbox{\tt either\ }} \newcommand{\dorelse}{\mbox{\tt\ orelse\ }} \newcommand{\dskip}{\mbox{\tt skip}} \newcommand{\dfail}{\mbox{\tt fail}} \newcommand{\dif}{\mbox{\tt if\ }} \newcommand{\dthen}{\mbox{\tt \ then\ }} \newcommand{\delse}{\mbox{\tt \ else\ }} \newcommand{\dtest}{\mbox{\tt test\ }} \newcommand{\dsome}{\mbox{\tt some\ }} \newcommand{\dand}{\mbox{\tt \ and\ }} \newcommand{\dnot}{\mbox{\tt not\ }} \newcommand{\dor}{\mbox{\tt \ or\ }} A final extension of DPL that we need is indexed variables. If a set $\mbox{Var}$ of variables is given, we can form new variables by means of appending indices. Assuming for a moment that we are computing on the natural numbers, we get the following language of extended DPL. \[ \begin{array}{llll} v & ::= & \mbox{var} \mid v[N] \\ \ri & ::= & 0 \mid 1 \mid \cdots \mid v \mid (\ri_1 + \ri_2) \mid (\ri_1 \dot{-} \ri_2) \mid (\ri_1 * \ri_2) \mid f N_1 \cdots N_n \\ \phi & ::= & \bot \mid P N_1 \cdots N_n \mid N_1 \doteq N_2 \mid \exists v \mid \neg \phi \mid (\phi_1 ; \phi_2) \mid (\phi_1 \cup \phi_2) \mid \phi^\ri \mid \BCform \end{array} \] Figure \sref{DynTrans} introduces the \dyn\ syntax by means of a translation to the extended DPL language. The translation fixes the intended meaning of every \dyn\ construct. \begin{figure}[htbp] \caption{Translation from \dyn\ to Extended DPL. \label{DynTrans}} \begin{center} \begin{tabular}{|lcl|} \hline $(\dbegin S_1 ; \ldots ; S_n \dend)^\circ$ \rule{0ex}{4ex} & := & $S_1^\circ ; \ldots ; S_n^\circ$ \\[2ex] $(\dskip)^\circ$ & := & $\neg \bot$ \\[2ex] $ (\dfail)^\circ$ & := & $\bot$ \\[2ex] $(t_1 = t_2)^\circ$ & := & $t_1 = t_2$ \\[2ex] $(\dsome v)^\circ$ & := & $\exists v$ \\[2ex] $(\dsome v_1, \ldots , v_n)^\circ$ & := & $\exists v_1 ; \ldots ; \exists v_n$ \\[2ex] $(v_1 \ \verb^>>^ \ v_2 = t)^\circ$ & := & $\exists v_2; v_1 = v_2; \exists v_1; v_1 = t$ \\[2ex] $(\dfind v \din [N .. M] \dwith S)^\circ$ & := & $\cup^{v}_{M..N} S^\circ$ \\[2ex] $(\ddo N \dtimes S)^\circ$ & := & $(S^\circ)^N$ \\[2ex] $(\dif B \dthen S_1 \delse S_2)^\circ$ & := & $(\neg \neg B^\odot; S_1^\circ) \cup (\neg B^\odot; S_2^\circ)$ \\[2ex] $(\deither S_1 \dorelse S_2)^\circ$ & := & $S_1^\circ \cup S_2^\circ$ \\[2ex] $(\dtest B)^\circ$ & := & $\neg \neg B^\odot$ \\[2ex] $(\ddonot S)^\circ$ & := & $\neg S^\circ$ \\[2ex] \hline $(t_1 = t_2)^\odot$ \rule{0ex}{4ex} & := & $t_1 = t_2$ \\[2ex] $(P t_1 \cdots t_n)^\odot$ & := & $P t_1 \cdots t_n$ \\[2ex] $(\dnot B)^\odot$ & := & $\neg B^\odot$ \\[2ex] $(B_1 \dand B_2)^\odot$ & := & $B_1^\odot ; B_2^\odot$ \\[2ex] $(B_1 \dor B_2)^\odot$ & := & $B_1^\odot \cup B_2^\odot$ \\[2ex]\hline \end{tabular} \end{center} \end{figure} \section{The Dynamo Statements One by One} \paragraph{Some Statement} Example: \begin{verbatim} some x, y, z \end{verbatim} \paragraph{Skip Statement} \begin{verbatim} skip \end{verbatim} \paragraph{Fail Statement} \begin{verbatim} fail \end{verbatim} \paragraph{Identity Statement} Example: \begin{verbatim} x = 2 \end{verbatim} \paragraph{Composite Statement} Example: \begin{verbatim} begin x = 0; y = 1; z = 3 end \end{verbatim} \paragraph{Put Statement} Example: \begin{verbatim} x >> x0 = x0 + 1 \end{verbatim} This example statement increments the value of \verb^x^ while using \verb^x0^ as an auxiliary variable. The example statement is equivalent to the following composite statement: \begin{verbatim} begin some x0; x0 = x; some x; x = x0 + 1 end \end{verbatim} \paragraph{Test Statement} Example: \begin{verbatim} test x = 2 \end{verbatim} This behaves different from the identity statement \verb^x=2^ for input states that have no value for \verb^x^. For such inputs, the identity statement \verb^x=2^ will assign $2$ to \verb^x^, but the test statement \verb^test x = 2^ will raise an exception, because the test cannot be evaluated for the current input. \paragraph{If Statement} Example: \begin{verbatim} if x = 2 then skip else fail \end{verbatim} Here the condition \verb^x = 2^ is read as a test. In case there is no input value for \verb^x^, the example statement will raise an exception. \paragraph{Either Statement} Example: \begin{verbatim} either x = 2 orelse x = 3 \end{verbatim} Note that any if statement can be paraphrased in terms of an either statement and a test statement. The if statement example above is equivalent to: \begin{verbatim} either test x = 2 orelse fail \end{verbatim} \paragraph{Do Statement} Example: \begin{verbatim} do 100 times begin x >> x0 = x0 + 1; y[x] = 0 end \end{verbatim} If \verb^x^ does have a value $n$ for the current input, this initializes an array $y[n+1],\ldots, y[n+100]$. If \verb^x^ does not have a value for the current input, the example raises an exception. \paragraph{Find Statement} Example: \begin{verbatim} find i in [1..100] with i = j \end{verbatim} \paragraph{Not Statement} Example: \begin{verbatim} donot find i in [1..100] with i = j \end{verbatim} \section{Some Simple Dynamo Programs and Their Outputs} Here is a dynamo program that computes values for $x$ and $y$: \begin{verbatim} begin some x; x = 0; x = y; some x; x = 1 end \end{verbatim} In its output, a distinction is made between the {\em global}\/ variable $y$ and the {\em local}\/ variable $x$. Also note that the output indicates that the solution set is complete. \begin{verbatim} "y":0 e.g. "x":1 There are no further solutions \end{verbatim} Next, consider the following program: \begin{verbatim} begin either x = 2 orelse x = 3; either y = x + 1 orelse 2 = y; 2 * x = 3 * y end \end{verbatim} Its output: \begin{verbatim} "x":3 "y":2 There are no further solutions \end{verbatim} When we change the order of the first and the second statement the execution mechanism encounters the statement \verb^y = x + 1^ in a situation where neither $x$ nor $y$ is known. This raises an exception which is propagated. \begin{verbatim} begin either y = x + 1 orelse 2 = y; either x = 2 orelse x = 3; 2 * x = 3 * y end \end{verbatim} The output indicates that the value `unknown' was encountered: \begin{verbatim} "y":2 "x":3 There may be further solutions \end{verbatim} \section{Example: Stable Marriages} For a slightly more involved example, here is a \dyn\ program for marrying off $4$ women to $4$ men in a random fashion. The program has a name, followed by a list containing the schemes of the display variables. A display list \verb^(a,b,c)^ indicates that the single variables {\tt a}, {\tt b} and {\tt c} are to be displayed. A display list \verb^(a,b[],c[][])^ indicates that the single variable {\tt a}, the indexed array {\tt b} and the doubly indexed array {\tt c} are to be displayed. In the following example, \verb^(WifeOf [])^ indicates that the computed values of the array {\tt WifeOf}\/ should be displayed. \begin{verbatim} program marriage (WifeOf []); begin n = 4; m = 0; some w; w = 0; do n times { marry off the women one by one } begin w >> w0 = w0 + 1; find m in [1 .. n] with begin b[m] = 1; { m is still a bachelor } w = WifeOf[m]; { propose woman w to man m } some b[m]; b[m] = 0; { m is no bachelor anymore } end end end \end{verbatim} \begin{figure}[htbp] \caption{\dyn\ output for the marriage program. \label{marriage}} \begin{fminipage} \begin{tt} "WifeOf[4]":1 "WifeOf[1]":2 "WifeOf[3]":3 "WifeOf[2]":4 \\ "WifeOf[4]":1 "WifeOf[1]":2 "WifeOf[2]":3 "WifeOf[3]":4 \\ "WifeOf[4]":1 "WifeOf[2]":2 "WifeOf[3]":3 "WifeOf[1]":4 \\ "WifeOf[4]":1 "WifeOf[2]":2 "WifeOf[1]":3 "WifeOf[3]":4 \\ "WifeOf[4]":1 "WifeOf[3]":2 "WifeOf[2]":3 "WifeOf[1]":4 \\ "WifeOf[4]":1 "WifeOf[3]":2 "WifeOf[1]":3 "WifeOf[2]":4 \\ "WifeOf[3]":1 "WifeOf[1]":2 "WifeOf[4]":3 "WifeOf[2]":4 \\ "WifeOf[3]":1 "WifeOf[1]":2 "WifeOf[2]":3 "WifeOf[4]":4 \\ "WifeOf[3]":1 "WifeOf[2]":2 "WifeOf[4]":3 "WifeOf[1]":4 \\ "WifeOf[3]":1 "WifeOf[2]":2 "WifeOf[1]":3 "WifeOf[4]":4 \\ "WifeOf[3]":1 "WifeOf[4]":2 "WifeOf[2]":3 "WifeOf[1]":4 \\ "WifeOf[3]":1 "WifeOf[4]":2 "WifeOf[1]":3 "WifeOf[2]":4 \\ "WifeOf[2]":1 "WifeOf[1]":2 "WifeOf[4]":3 "WifeOf[3]":4 \\ "WifeOf[2]":1 "WifeOf[1]":2 "WifeOf[3]":3 "WifeOf[4]":4 \\ "WifeOf[2]":1 "WifeOf[3]":2 "WifeOf[4]":3 "WifeOf[1]":4 \\ "WifeOf[2]":1 "WifeOf[3]":2 "WifeOf[1]":3 "WifeOf[4]":4 \\ "WifeOf[2]":1 "WifeOf[4]":2 "WifeOf[3]":3 "WifeOf[1]":4 \\ "WifeOf[2]":1 "WifeOf[4]":2 "WifeOf[1]":3 "WifeOf[3]":4 \\ "WifeOf[1]":1 "WifeOf[2]":2 "WifeOf[4]":3 "WifeOf[3]":4 \\ "WifeOf[1]":1 "WifeOf[2]":2 "WifeOf[3]":3 "WifeOf[4]":4 \\ "WifeOf[1]":1 "WifeOf[3]":2 "WifeOf[4]":3 "WifeOf[2]":4 \\ "WifeOf[1]":1 "WifeOf[3]":2 "WifeOf[2]":3 "WifeOf[4]":4 \\ "WifeOf[1]":1 "WifeOf[4]":2 "WifeOf[3]":3 "WifeOf[2]":4 \\ "WifeOf[1]":1 "WifeOf[4]":2 "WifeOf[2]":3 "WifeOf[3]":4 \\ There are no further solutions \end{tt} \end{fminipage} \end{figure} The output of this program is given in Figure \sref{marriage}. If we have full information about the preferences of the men and women we can compute the matches that are stable. When is your marriage stable? An equivalent but possibly more disturbing version of this question runs: when is your marriage in danger? If your marriage is in danger it can be (basically) for two reasons\cite{Wirth:apdsip}: \begin{itemize} \item Either you yourself prefer someone else to your partner, and that other person either is single or prefers you to his/her own partner, or ... \item your partner prefers someone else to you, and that other person either is single or prefers your partner to his/her own partner. \end{itemize} A relational situation is stable if the above two dangers are avoided for everyone. How do we recognize or create stable situations? By means of a \dyn\ program. The program has to represent the preferences of the men and women involved. We can do that by means of two arrays $m$ and $f$. \verb^f[4][2] = 1^ signifies that woman $4$ puts man $2$ top of her list.\footnote{Anne Kaldeway informs me that there is some world knowledge involved in devising an efficient stable marriage algorithm. One should always take the women's preferences as one's point of departure. Why? Because it is a fact of life --- always according to Kaldeway --- that men tend to have their preferences shaped by superficial sentiments, with virtually identical wish lists as a result.} \begin{verbatim} program StableMatching (WifeOf[]); begin { first we list the women's ranking of the men } f[1][1] = 4; f[1][2] = 2; f[1][3] = 3; f[1][4] = 1; f[2][1] = 1; f[2][2] = 3; f[2][3] = 4; f[2][4] = 2; f[3][1] = 1; f[3][2] = 2; f[3][3] = 3; f[3][4] = 4; f[4][1] = 2; f[4][2] = 1; f[4][3] = 4; f[4][4] = 3; { second we list the men's ranking of the women } m[1][1] = 2; m[1][2] = 1; m[1][3] = 4; m[1][4] = 3; m[2][1] = 2; m[2][2] = 1; m[2][3] = 3; m[2][4] = 4; m[3][1] = 2; m[3][2] = 1; m[3][3] = 3; m[3][4] = 4; m[4][1] = 3; m[4][2] = 1; m[4][3] = 2; m[4][4] = 4; n = 4; m = 0; do n times { record that all men are bachelors } begin m >> m0 = m0 + 1; b[m] = 1 end; some w; w = 0; do n times { try to marry off the women one by one } begin w >> w0 = w0 + 1; find m in [1 .. n] with begin some i; f[w][m] = i; { m is w's i-th preference } b[m] = 1; { m is still a bachelor } w = WifeOf[m]; { propose woman w to man m } some b[m]; b[m] = 0; { m is no bachelor anymore } donot find rival in [1 .. n] with begin test f[w][rival] < i;{ w prevers rival to m } either b[rival] = 1 { rival is still unmarried } orelse begin b[rival] = 0; { or .. rival is married } test m[rival][w] < m[rival][WifeOf[rival]]; { rival prefers w to his own Wife } end end end end end \end{verbatim} The output of program {\tt StableMatching} is in Figure \sref{stable}. \begin{figure}[htbp] \caption{\dyn\ output for the stable marriage program \label{stable}} \begin{fminipage} \begin{tt} "WifeOf[4]":1 "WifeOf[1]":2 "WifeOf[2]":3 "WifeOf[3]":4 \\ There are no further solutions \end{tt} \end{fminipage} \end{figure} \section{Example: N Queens} The challenge: position $N$ queens on a chess-board of size $N \times N$ in such manner that none of them is under attack from any of the others\cite{Wirth:apdsip}. Represent a placement of the queens on the board as a function $f$ from columns to rows. Then $f(4) = 5$ expresses that the queen of column $4$ is in row $5$. If $f(k) = r$, then: \begin{enumerate} \item No queen from $i \in \{ 1, \ldots, k-1 \}$, should be on row $r$. \item No queen from $i \in \{ 1, \ldots, k-1 \}$ should be on the $\nearrow$ diagonal through $r$ (i.e., on position $r + (k - i)$). \item No queen from $i \in \{ 1, \ldots, k-1 \}$ should be on the $\searrow$ diagonal through $r$ (i.e., on position $r - (k -i)$). \end{enumerate} Here is a \dyn\ program for the eight queens problem. \begin{figure}[htbp] \caption{\dyn\ output for the Eight Queens problem. \label{8queens}} \begin{fminipage}\tiny \begin{alltt} "f[1]":8 "f[2]":2 "f[3]":5 "f[4]":3 "f[5]":1 "f[6]":7 "f[7]":4 "f[8]":6 "f[1]":4 "f[2]":1 "f[3]":5 "f[4]":8 "f[5]":6 "f[6]":3 "f[7]":7 "f[8]":2 "f[1]":8 "f[2]":2 "f[3]":4 "f[4]":1 "f[5]":7 "f[6]":5 "f[7]":3 "f[8]":6 "f[1]":4 "f[2]":1 "f[3]":5 "f[4]":8 "f[5]":2 "f[6]":7 "f[7]":3 "f[8]":6 "f[1]":8 "f[2]":3 "f[3]":1 "f[4]":6 "f[5]":2 "f[6]":5 "f[7]":7 "f[8]":4 "f[1]":4 "f[2]":2 "f[3]":8 "f[4]":5 "f[5]":7 "f[6]":1 "f[7]":3 "f[8]":6 "f[1]":8 "f[2]":4 "f[3]":1 "f[4]":3 "f[5]":6 "f[6]":2 "f[7]":7 "f[8]":5 "f[1]":4 "f[2]":2 "f[3]":8 "f[4]":6 "f[5]":1 "f[6]":3 "f[7]":5 "f[8]":7 "f[1]":7 "f[2]":1 "f[3]":3 "f[4]":8 "f[5]":6 "f[6]":4 "f[7]":2 "f[8]":5 "f[1]":4 "f[2]":2 "f[3]":7 "f[4]":3 "f[5]":6 "f[6]":8 "f[7]":5 "f[8]":1 "f[1]":7 "f[2]":2 "f[3]":6 "f[4]":3 "f[5]":1 "f[6]":4 "f[7]":8 "f[8]":5 "f[1]":4 "f[2]":2 "f[3]":7 "f[4]":3 "f[5]":6 "f[6]":8 "f[7]":1 "f[8]":5 "f[1]":7 "f[2]":2 "f[3]":4 "f[4]":1 "f[5]":8 "f[6]":5 "f[7]":3 "f[8]":6 "f[1]":4 "f[2]":2 "f[3]":7 "f[4]":5 "f[5]":1 "f[6]":8 "f[7]":6 "f[8]":3 "f[1]":7 "f[2]":3 "f[3]":8 "f[4]":2 "f[5]":5 "f[6]":1 "f[7]":6 "f[8]":4 "f[1]":4 "f[2]":2 "f[3]":5 "f[4]":8 "f[5]":6 "f[6]":1 "f[7]":3 "f[8]":7 "f[1]":7 "f[2]":3 "f[3]":1 "f[4]":6 "f[5]":8 "f[6]":5 "f[7]":2 "f[8]":4 "f[1]":4 "f[2]":6 "f[3]":8 "f[4]":2 "f[5]":7 "f[6]":1 "f[7]":3 "f[8]":5 "f[1]":7 "f[2]":4 "f[3]":2 "f[4]":5 "f[5]":8 "f[6]":1 "f[7]":3 "f[8]":6 "f[1]":4 "f[2]":6 "f[3]":8 "f[4]":3 "f[5]":1 "f[6]":7 "f[7]":5 "f[8]":2 "f[1]":7 "f[2]":4 "f[3]":2 "f[4]":8 "f[5]":6 "f[6]":1 "f[7]":3 "f[8]":5 "f[1]":4 "f[2]":6 "f[3]":1 "f[4]":5 "f[5]":2 "f[6]":8 "f[7]":3 "f[8]":7 "f[1]":7 "f[2]":5 "f[3]":3 "f[4]":1 "f[5]":6 "f[6]":8 "f[7]":2 "f[8]":4 "f[1]":4 "f[2]":7 "f[3]":5 "f[4]":2 "f[5]":6 "f[6]":1 "f[7]":3 "f[8]":8 "f[1]":6 "f[2]":1 "f[3]":5 "f[4]":2 "f[5]":8 "f[6]":3 "f[7]":7 "f[8]":4 "f[1]":4 "f[2]":7 "f[3]":5 "f[4]":3 "f[5]":1 "f[6]":6 "f[7]":8 "f[8]":2 "f[1]":6 "f[2]":2 "f[3]":7 "f[4]":1 "f[5]":4 "f[6]":8 "f[7]":5 "f[8]":3 "f[1]":4 "f[2]":7 "f[3]":3 "f[4]":8 "f[5]":2 "f[6]":5 "f[7]":1 "f[8]":6 "f[1]":6 "f[2]":2 "f[3]":7 "f[4]":1 "f[5]":3 "f[6]":5 "f[7]":8 "f[8]":4 "f[1]":4 "f[2]":7 "f[3]":1 "f[4]":8 "f[5]":5 "f[6]":2 "f[7]":6 "f[8]":3 "f[1]":6 "f[2]":3 "f[3]":7 "f[4]":2 "f[5]":8 "f[6]":5 "f[7]":1 "f[8]":4 "f[1]":4 "f[2]":8 "f[3]":5 "f[4]":3 "f[5]":1 "f[6]":7 "f[7]":2 "f[8]":6 "f[1]":6 "f[2]":3 "f[3]":7 "f[4]":2 "f[5]":4 "f[6]":8 "f[7]":1 "f[8]":5 "f[1]":4 "f[2]":8 "f[3]":1 "f[4]":3 "f[5]":6 "f[6]":2 "f[7]":7 "f[8]":5 "f[1]":6 "f[2]":3 "f[3]":7 "f[4]":4 "f[5]":1 "f[6]":8 "f[7]":2 "f[8]":5 "f[1]":4 "f[2]":8 "f[3]":1 "f[4]":5 "f[5]":7 "f[6]":2 "f[7]":6 "f[8]":3 "f[1]":6 "f[2]":3 "f[3]":5 "f[4]":7 "f[5]":1 "f[6]":4 "f[7]":2 "f[8]":8 "f[1]":3 "f[2]":1 "f[3]":7 "f[4]":5 "f[5]":8 "f[6]":2 "f[7]":4 "f[8]":6 "f[1]":6 "f[2]":3 "f[3]":5 "f[4]":8 "f[5]":1 "f[6]":4 "f[7]":2 "f[8]":7 "f[1]":3 "f[2]":5 "f[3]":8 "f[4]":4 "f[5]":1 "f[6]":7 "f[7]":2 "f[8]":6 "f[1]":6 "f[2]":3 "f[3]":1 "f[4]":7 "f[5]":5 "f[6]":8 "f[7]":2 "f[8]":4 "f[1]":3 "f[2]":5 "f[3]":7 "f[4]":1 "f[5]":4 "f[6]":2 "f[7]":8 "f[8]":6 "f[1]":6 "f[2]":3 "f[3]":1 "f[4]":8 "f[5]":5 "f[6]":2 "f[7]":4 "f[8]":7 "f[1]":3 "f[2]":5 "f[3]":2 "f[4]":8 "f[5]":6 "f[6]":4 "f[7]":7 "f[8]":1 "f[1]":6 "f[2]":3 "f[3]":1 "f[4]":8 "f[5]":4 "f[6]":2 "f[7]":7 "f[8]":5 "f[1]":3 "f[2]":5 "f[3]":2 "f[4]":8 "f[5]":1 "f[6]":7 "f[7]":4 "f[8]":6 "f[1]":6 "f[2]":4 "f[3]":7 "f[4]":1 "f[5]":8 "f[6]":2 "f[7]":5 "f[8]":3 "f[1]":3 "f[2]":6 "f[3]":8 "f[4]":1 "f[5]":5 "f[6]":7 "f[7]":2 "f[8]":4 "f[1]":6 "f[2]":4 "f[3]":7 "f[4]":1 "f[5]":3 "f[6]":5 "f[7]":2 "f[8]":8 "f[1]":3 "f[2]":6 "f[3]":8 "f[4]":1 "f[5]":4 "f[6]":7 "f[7]":5 "f[8]":2 "f[1]":6 "f[2]":4 "f[3]":2 "f[4]":8 "f[5]":5 "f[6]":7 "f[7]":1 "f[8]":3 "f[1]":3 "f[2]":6 "f[3]":8 "f[4]":2 "f[5]":4 "f[6]":1 "f[7]":7 "f[8]":5 "f[1]":6 "f[2]":4 "f[3]":1 "f[4]":5 "f[5]":8 "f[6]":2 "f[7]":7 "f[8]":3 "f[1]":3 "f[2]":6 "f[3]":4 "f[4]":1 "f[5]":8 "f[6]":5 "f[7]":7 "f[8]":2 "f[1]":6 "f[2]":8 "f[3]":2 "f[4]":4 "f[5]":1 "f[6]":7 "f[7]":5 "f[8]":3 "f[1]":3 "f[2]":6 "f[3]":4 "f[4]":2 "f[5]":8 "f[6]":5 "f[7]":7 "f[8]":1 "f[1]":5 "f[2]":1 "f[3]":8 "f[4]":4 "f[5]":2 "f[6]":7 "f[7]":3 "f[8]":6 "f[1]":3 "f[2]":6 "f[3]":2 "f[4]":5 "f[5]":8 "f[6]":1 "f[7]":7 "f[8]":4 "f[1]":5 "f[2]":1 "f[3]":8 "f[4]":6 "f[5]":3 "f[6]":7 "f[7]":2 "f[8]":4 "f[1]":3 "f[2]":6 "f[3]":2 "f[4]":7 "f[5]":5 "f[6]":1 "f[7]":8 "f[8]":4 "f[1]":5 "f[2]":1 "f[3]":4 "f[4]":6 "f[5]":8 "f[6]":2 "f[7]":7 "f[8]":3 "f[1]":3 "f[2]":6 "f[3]":2 "f[4]":7 "f[5]":1 "f[6]":4 "f[7]":8 "f[8]":5 "f[1]":5 "f[2]":2 "f[3]":8 "f[4]":1 "f[5]":4 "f[6]":7 "f[7]":3 "f[8]":6 "f[1]":3 "f[2]":7 "f[3]":2 "f[4]":8 "f[5]":6 "f[6]":4 "f[7]":1 "f[8]":5 "f[1]":5 "f[2]":2 "f[3]":6 "f[4]":1 "f[5]":7 "f[6]":4 "f[7]":8 "f[8]":3 "f[1]":3 "f[2]":7 "f[3]":2 "f[4]":8 "f[5]":5 "f[6]":1 "f[7]":4 "f[8]":6 "f[1]":5 "f[2]":2 "f[3]":4 "f[4]":6 "f[5]":8 "f[6]":3 "f[7]":1 "f[8]":7 "f[1]":3 "f[2]":8 "f[3]":4 "f[4]":7 "f[5]":1 "f[6]":6 "f[7]":2 "f[8]":5 "f[1]":5 "f[2]":2 "f[3]":4 "f[4]":7 "f[5]":3 "f[6]":8 "f[7]":6 "f[8]":1 "f[1]":2 "f[2]":4 "f[3]":6 "f[4]":8 "f[5]":3 "f[6]":1 "f[7]":7 "f[8]":5 "f[1]":5 "f[2]":3 "f[3]":8 "f[4]":4 "f[5]":7 "f[6]":1 "f[7]":6 "f[8]":2 "f[1]":2 "f[2]":5 "f[3]":7 "f[4]":1 "f[5]":3 "f[6]":8 "f[7]":6 "f[8]":4 "f[1]":5 "f[2]":3 "f[3]":1 "f[4]":6 "f[5]":8 "f[6]":2 "f[7]":4 "f[8]":7 "f[1]":2 "f[2]":5 "f[3]":7 "f[4]":4 "f[5]":1 "f[6]":8 "f[7]":6 "f[8]":3 "f[1]":5 "f[2]":3 "f[3]":1 "f[4]":7 "f[5]":2 "f[6]":8 "f[7]":6 "f[8]":4 "f[1]":2 "f[2]":6 "f[3]":8 "f[4]":3 "f[5]":1 "f[6]":4 "f[7]":7 "f[8]":5 "f[1]":5 "f[2]":7 "f[3]":4 "f[4]":1 "f[5]":3 "f[6]":8 "f[7]":6 "f[8]":2 "f[1]":2 "f[2]":6 "f[3]":1 "f[4]":7 "f[5]":4 "f[6]":8 "f[7]":3 "f[8]":5 "f[1]":5 "f[2]":7 "f[3]":2 "f[4]":4 "f[5]":8 "f[6]":1 "f[7]":3 "f[8]":6 "f[1]":2 "f[2]":7 "f[3]":5 "f[4]":8 "f[5]":1 "f[6]":4 "f[7]":6 "f[8]":3 "f[1]":5 "f[2]":7 "f[3]":2 "f[4]":6 "f[5]":3 "f[6]":1 "f[7]":8 "f[8]":4 "f[1]":2 "f[2]":7 "f[3]":3 "f[4]":6 "f[5]":8 "f[6]":5 "f[7]":1 "f[8]":4 "f[1]":5 "f[2]":7 "f[3]":2 "f[4]":6 "f[5]":3 "f[6]":1 "f[7]":4 "f[8]":8 "f[1]":2 "f[2]":8 "f[3]":6 "f[4]":1 "f[5]":3 "f[6]":5 "f[7]":7 "f[8]":4 "f[1]":5 "f[2]":7 "f[3]":1 "f[4]":3 "f[5]":8 "f[6]":6 "f[7]":4 "f[8]":2 "f[1]":1 "f[2]":5 "f[3]":8 "f[4]":6 "f[5]":3 "f[6]":7 "f[7]":2 "f[8]":4 "f[1]":5 "f[2]":7 "f[3]":1 "f[4]":4 "f[5]":2 "f[6]":8 "f[7]":6 "f[8]":3 "f[1]":1 "f[2]":6 "f[3]":8 "f[4]":3 "f[5]":7 "f[6]":4 "f[7]":2 "f[8]":5 "f[1]":5 "f[2]":8 "f[3]":4 "f[4]":1 "f[5]":7 "f[6]":2 "f[7]":6 "f[8]":3 "f[1]":1 "f[2]":7 "f[3]":5 "f[4]":8 "f[5]":2 "f[6]":4 "f[7]":6 "f[8]":3 "f[1]":5 "f[2]":8 "f[3]":4 "f[4]":1 "f[5]":3 "f[6]":6 "f[7]":2 "f[8]":7 "f[1]":1 "f[2]":7 "f[3]":4 "f[4]":6 "f[5]":8 "f[6]":2 "f[7]":5 "f[8]":3 There are no further solutions \end{alltt} \end{fminipage} \end{figure} \begin{verbatim} program Nqueens (f[]); begin n = 8; some k; k = 0; do n times begin k >> k0 = k0 + 1; find r in [1 .. n] with begin r = f[k]; donot find i in [1 .. k-1] with either f[i] = r orelse either f[i] = r + (k - i) orelse f[i] = r - (k - i) end end end \end{verbatim} The program generates the 92 solutions and displays them (see Figure \ref{8queens}). \section{The Implementation} We now turn to the description of the Haskell implementation of \dyn. The following gives the (almost) complete code. In fact, the paper you are now reading is the \LaTeX\ output of the literate code for \dyn. The only exception is the parsing code, which is generated by a Haskell parser generator (see below). The Haskell implementation of \dyn\ consists of three modules: the main module {\em dynamo}, and the modules {\em L}\/ (for lexical scanning) and {\em D}\/ (for parsing). Everything below that appears in a frame and is typeset in {\tt typescript} font is part of the actual Haskell code. \section{Import Scanning and Parsing Modules} The module {\em Dynamo}\/ uses the modules {\em L}\/ and {\em D}. \begin{code} module Dynamo where import L import D \end{code} The modules {\em L}\/ and {\em D}\/ contain the lexicalizer and the parser for \dyn\ programs. \input{L.lhs} \section{Parsing} The BNF definition of \dyn\ program statements is given by the following piece of code. We give part of the input for the parser module, which is generated from the code below (typeset in {\tt typescript}, between horizontal lines) by the Haskell {\em Happy}\/ parser generator \cite{Marlow:hug}. A program is either a single statement, or it starts with the reserved word {\tt program}, followed by a program name, a list of display variable schemes, and a statement. The display variable schemes indicate whether a display variable is a single variable {\tt a}, a variable with a single index {\tt a[]}, or a variable with a double index {\tt a[][]}. Indicating display variables by schemes is necessary because in \dyn\ nothing prevents the use of the same name {\tt a} for these three purposes. \putline \begin{verbatim} Pgm : Stmt { (False,[],$1) } | program Name ';' Stmt { (False,[],$4) } | program Name Vdecl ';' Stmt { (True,$3,$5) } Name : name { } Vdecl : '(' Vschemes ')' { $2 } Vschemes : Vschemes ',' Vscheme { $3 : $1 } | Vscheme { [$1] } | {- empty -} { [] } Vscheme : name { ($1,0) } | name '[' ']' { ($1,1) } | name '[' ']' '[' ']' { ($1,2) } \end{verbatim}\putline The form of a \dyn\ statement is given by the following: \putline\begin{verbatim} Stmt : some Var { Some $2 } | some Vars { Comp [ (Some x) | x <- (reverse $2) ] } | skip { Skip } | fail { Fail } | Exp '=' Exp { Iseq $1 $3 } | Var '>' '>' Var '=' Exp { Put $1 $4 $6 } | test Bexp { Test $2 } | if Bexp then Stmt else Stmt { If $2 $4 $6 } | either Stmt orelse Stmt { Either $2 $4 } | do Exp times Stmt { Do $2 $4 } | find Var in Rng with Stmt { Find $2 $4 $6 } | donot Stmt { Not $2 } | begin Stmts end { Comp (reverse $2)} | {- empty -} { Skip } \end{verbatim}\putline The statements in a list are generated by the parser in the form of a parse stack, so the list has to be reversed to get its meaning right. The same holds for the variables is a variable list. \putline\begin{verbatim} Stmts : Stmts ';' Stmt { $3 : $1 } | Stmt { [$1] } Vars : Vars ',' Var { $3 : $1 } | Var ',' Var { [$3,$1] } \end{verbatim}\putline Variables can be strings, strings with single indices, or strings with double indices. Note the difference between variables and the variable schemes above. \putline\begin{verbatim} Var : name { Svar $1 } | name '[' Exp ']' { Ivar $1 $3 } | name '[' Exp ']' '[' Exp ']' { Divar $1 $3 $6 } \end{verbatim}\putline Ranges for bounded search are also indicated by square brackets: \putline\begin{verbatim} Rng : '[' Exp '.' '.' Exp ']' { ($2,$5) } \end{verbatim}\putline The capitalized keywords on the righthand side are the datatypes that are used for the construction of the parse trees. For example, the \dyn\ program \begin{verbatim} begin either x = 3 orelse y = 4; x = 4 + y end \end{verbatim} gives rise to the following parse tree: \begin{verbatim} Comp [Either (Iseq (Term (Factor (Var (Svar "x")))) (Term (Factor (Int 3)))) (Iseq (Term (Factor (Var (Svar "y")))) (Term (Factor (Int 4)))), Iseq (Term (Factor (Var (Svar "x")))) (Plus (Term (Factor (Int 4))) (Factor (Var (Svar "y"))))] \end{verbatim} The main parse procedure is called {\tt parse}. \section{Datatype Declarations for Semantics} The following type declarations are needed for the semantics. All variables are represented as strings. If a variable has an index, it is incorporated in the string. The advantage of this is that it will usually not be necessary to allocate space for arrays. Instead, we just represent those values of the array that get actually computed by the program. A valuation is a list of pairs consisting of variables with their values. A store is a list of variables. \begin{code} type Variable = String type Valuation = [(Variable,Int)] type Store = [Variable] \end{code} {\tt Vscheme} is the type of a variable scheme: the integer indicates the number of indexes. {\tt Pgm}\/ is the type of a program: the boolean in the first component indicates whether a display constraint was stated, the list of variable schemes in the second component specifies the display constraint, and the statement in the third component gives the actual program. The indication of a display constraint allows us to distinguish between \verb^program Test; n = 1^ and \verb^program Test (); n = 1^. The first program will display the value of \verb^n^, the second will merely state that that the test evaluates to true. \begin{code} type Vscheme = (Variable,Integer) type Pgm = (Bool,[Vscheme],Stmt) \end{code} A proper state is a triple consisting of a valuation, a global store and a local store. Two proper states are equal when they are equal componentwise. A state is either just a proper state, or improper. \begin{code} data ProperState = Ps Valuation Store Store instance Eq ProperState where Ps a g l == Ps b g' l' = a == b && g == g' && l == l' type State = Maybe ProperState \end{code} The {\tt Maybe}\/ datatype is a convenient Haskell provision for handling exceptions. A datatype {\tt Maybe a}\/ for type {\tt a}, has as possible values {\tt Nothing}\/ and {\tt Just a}. The value {\tt Nothing}\/ signifies that an exception has arisen, the value {\tt Just a}\/ indicates that a proper answer has been computed. We will use {\tt Nothing}\/ for the improper state $\bullet$. \section{Values for Arithmetic and Boolean Expressions} Exception handling also plays a role in the computation process of answers for operators that may get inproper inputs. The following functions lift operators of types \verb^a -> b^ and \verb^a -> a -> b^ to a type that can handle inproper input by raising an exception. \begin{code} maybe_op1 :: (a -> b) -> Maybe a -> Maybe b maybe_op1 op Nothing = Nothing maybe_op1 op (Just x) = Just (op x) maybe_op2 :: (a -> a -> b) -> Maybe a -> Maybe a -> Maybe b maybe_op2 op Nothing arg = Nothing maybe_op2 op arg Nothing = Nothing maybe_op2 op (Just x) (Just y) = Just (op x y) \end{code} Computing the values of arithmetic expressions, with exception handling: \begin{code} a_val_exp :: Exp -> Valuation -> Maybe Int a_val_exp(Plus a_1 a_2) s = maybe_op2 (+) (a_val_exp a_1 s) (a_val_term a_2 s) a_val_exp(Minus a_1 a_2) s = maybe_op2 (-) (a_val_exp a_1 s) (a_val_term a_2 s) a_val_exp(Term a) s = a_val_term a s a_val_term :: Term -> Valuation -> Maybe Int a_val_term(Times a_1 a_2) s = maybe_op2 (*) (a_val_term a_1 s) (a_val_factor a_2 s) a_val_term(Div a_1 a_2) s = maybe_op2 div (a_val_term a_1 s) (a_val_factor a_2 s) a_val_term(Factor a) s = a_val_factor a s \end{code} In order to handle indexed variables, we convert the index to a string, by means of the following: \begin{code} intStr :: Int -> String intStr i = intStrStr i [] intStrStr :: Int -> String -> String intStrStr i s | i == last = (intToDigit last):s | otherwise = intStrStr (quot i 10) (intToDigit(last):s) where last = rem i 10 \end{code} This allows us to use the index as an appendix to the variable name, and do the variable lookup: \begin{code} a_val_factor :: Factor -> Valuation -> Maybe Int a_val_factor(Int n) s = Just n a_val_factor(Var (Svar x)) s = lookup x s a_val_factor(Var (Ivar x expr)) s = lookup (x ++ ('[':(intStr i)) ++ "]") s where Just i = a_val_exp expr s a_val_factor(Var (Divar x expr1 expr2)) s = lookup (x ++ '[':(intStr i) ++ ']':'[':(intStr j) ++ "]") s where Just i = a_val_exp expr1 s Just j = a_val_exp expr2 s a_val_factor(Brack expr) s = a_val_exp expr s \end{code} Computing the values of Boolean expressions, with exception handling: \begin{code} b_val_exp :: Bexp -> Valuation -> Maybe Bool b_val_exp(Bool t) s = Just t b_val_exp(Eq e_1 e_2) s = maybe_op2 (==) (a_val_exp e_1 s) (a_val_exp e_2 s) b_val_exp(Gr e_1 e_2) s = maybe_op2 (>) (a_val_exp e_1 s) (a_val_exp e_2 s) b_val_exp(Geq e_1 e_2) s = maybe_op2 (>=) (a_val_exp e_1 s) (a_val_exp e_2 s) b_val_exp(Less e_1 e_2) s = maybe_op2 (<) (a_val_exp e_1 s) (a_val_exp e_2 s) b_val_exp(Leq e_1 e_2) s = maybe_op2 (<=) (a_val_exp e_1 s) (a_val_exp e_2 s) b_val_exp(Neq e_1 e_2) s = maybe_op2 (/=) (a_val_exp e_1 s) (a_val_exp e_2 s) b_val_exp(Neg e) s = maybe_op1 not (b_val_exp e s) b_val_exp(Conj e_1 e_2) s = maybe_op2 (&&) (b_val_exp e_1 s) (b_val_exp e_2 s) b_val_exp(Disj e_1 e_2) s = maybe_op2 (||) (b_val_exp e_1 s) (b_val_exp e_2 s) \end{code} \section{Handling Valuations and Stores} Resetting a variable in a valuation: \begin{code} reset :: Variable -> Valuation -> Valuation reset v [] = [] reset v ((x,d):xds) | v == x = reset v xds | otherwise = ((x,d):reset v xds) \end{code} Taking the {\tt union}\/ of two lists. Needed further on to add elements to valuations, to stores, and to state lists. Note that no duplicates are introduced. \begin{code} union :: Eq a => [a] -> [a] -> [a] union s [] = s union s (e:ee) | elem e s = union s ee | otherwise = e:(union s ee) \end{code} Check if {\tt Exp}\/ consists of a single variable, an indexed variable or a doubly indexed variable, with the index or indices defined for the current valuation, and if so, return it: \begin{code} getvar :: Exp -> Valuation -> [Variable] getvar (Term (Factor (Var (Svar v)))) s = [v] getvar (Term (Factor (Var (Ivar v exp)))) s = make_ivar v s (a_val_exp exp s) getvar (Term (Factor (Var (Divar v exp1 exp2)))) s = make_divar v s (a_val_exp exp1 s) (a_val_exp exp2 s) getvar _ _ = [] getvarstring :: Var -> Valuation -> [Variable] getvarstring (Svar x) s = [x] getvarstring (Ivar x exp) s = make_ivar x s (a_val_exp exp s) getvarstring (Divar x exp1 exp2) s = make_divar x s (a_val_exp exp1 s) (a_val_exp exp2 s) getvarstring _ _ = [] make_ivar :: Variable -> Valuation -> Maybe Int -> [Variable] make_ivar v val i = maybe [] f i where f j = [v ++ ('[':(intStr j)) ++ "]"] make_divar :: Variable -> Valuation -> Maybe Int -> Maybe Int -> [Variable] make_divar v val i = maybe (\j -> []) f i where f i j = maybe [] g j where g j = [v ++ '[':(intStr i) ++ ']':'[':(intStr j) ++ "]"] \end{code} {\tt processId}\/ processes the two expressions constituting an identity, in the context of a valuation, in order to see whether the identity is an assignment or a test. \begin{code} processId :: Exp -> Exp -> Valuation -> ([Variable],Maybe Int,[Variable],Maybe Int) processId exp1 exp2 s = (getvar exp1 s, a_val_exp exp1 s, getvar exp2 s, a_val_exp exp2 s) \end{code} Check whether a set of outputs is safe for a given input triple $(a,g^a,l^a)$. A set of outputs is safe if it contains at least one triple $(b,g^b,l^b)$ that guarantees the forward property for $(a,g^a,l^a) \to (b,g^b,l^b)$. The condition for this is: $l^a \cup g^b \subseteq \dom(a)$. Since the two stacks can only grow, and the global store grows only when a value gets assigned to a variable not in the local input store and not in the domain of the input valuation, we can replace this by two simpler conditions: $g^b = g^a$ and $l^a \subseteq \dom(a)$. Needed for a proper treatment of negation. \begin{code} isSafe :: ProperState -> [State] -> Bool isSafe _ [] = False isSafe agl states | not (localSafe agl) = False | otherwise = globalSafe agl states localSafe :: ProperState -> Bool localSafe (Ps a g l) = containedIn l [ x | (x,d) <- a ] globalSafe :: ProperState -> [State] -> Bool globalSafe pstate [] = False globalSafe pstate (Nothing:ss) = globalSafe pstate ss globalSafe (Ps a g l) (Just (Ps b g' l'):ss) = g == g' || (isSafe (Ps a g l) ss) containedIn :: Eq a => [a] -> [a] -> Bool containedIn [] bs = True containedIn (a:as) bs = (elem a bs) && (containedIn as bs) \end{code} \section{Evaluating Statements} {\tt run}\/ runs a statement on a state, and outputs a list of states. Note that the input state may be improper. The procedure {\tt run}\/ checks whether the input is proper. If not, the output list only contains the improper state, otherwise the procedure {\tt dorun}\/ is invoked: \begin{code} run :: Stmt -> State -> [State] run stmt = maybe [Nothing] (dorun stmt) \end{code} {\tt runs}\/ runs a sequence of statements for a list of input states, running the sequence for every member of the list of inputs and taking the union of the results. \begin{code} runs :: [Stmt] -> [State] -> [State] runs [] sts = sts runs (stmt:stmts) [] = [] runs (stmt:stmts) (st:sts) = runs stmts (union (run stmt st) (runs [stmt] sts)) \end{code} {\tt doruncomp}\/ runs a list of statements for a proper input state, and outputs a list of states. \begin{code} doruncomp :: [Stmt] -> ProperState -> [State] doruncomp [] pstate = [Just pstate] doruncomp [stmt] pstate = dorun stmt pstate doruncomp (stmt:stmts) pstate = runs stmts (dorun stmt pstate) \end{code} {\tt doSome}\/ is used in the evaluation of {\tt Some}\/ statements and in the evaluation of {\tt Find1}\/ statements. \begin{code} doSome :: Var -> ProperState -> ProperState doSome v (Ps a g l) = (Ps (reset x a) g (union l [x])) where [x] = getvarstring v a \end{code} {\tt dorun}\/ is the main procedure for executing single statements in the context of a proper input valuation. It takes a statement and a proper state, and returns a state list. \begin{code} dorun :: Stmt -> ProperState -> [State] \end{code} A {\tt Some v}\/ statement resets the variable {\tt v}. We isolate the procedure {\tt doSome}, as we need it later on in the definition of the evaluation of {\tt Find1}\/ statements. \begin{code} dorun (Some v) pstate = [Just (doSome v pstate)] \end{code} The {\tt Skip}\/ statement returns the input. The {\tt Fail}\/ statement returns an empty state set. \begin{code} dorun Skip pstate = [Just pstate] dorun Fail pstate = [] \end{code} The evaluation of the {\tt Iseq}\/ statement relies on the function {\tt processId}. \begin{code} dorun (Iseq e1 e2) (Ps val g l) = case (processId e1 e2 val) of ([v],Nothing,_,Just m) | elem v l -> [Just (Ps ((v,m):val) g l)] | otherwise -> [Just (Ps ((v,m):val) (union g [v]) l)] (_,Just m,[v],Nothing) | elem v l -> [Just (Ps ((v,m):val) g l)] | otherwise -> [Just (Ps ((v,m):val) (union g [v]) l)] (_,Just m,_,Just n ) | m == n -> [Just (Ps val g l)] | otherwise -> [] (_,_,_,_) -> [Nothing] \end{code} The {\tt Put v x exp}\/ statement merely abbreviates the sequential composition of {\tt Some x}, an identity statement, {\tt Some v}, and a second identity statement: \begin{code} dorun (Put v x exp) pstate = doruncomp [Some x,id1,Some v,id2] pstate where id1 = (Iseq (Term (Factor (Var v))) (Term (Factor (Var x)))) id2 = (Iseq (Term (Factor (Var v))) exp) \end{code} The {\tt Test}\/ statement checks the value of a Boolean expression. If the expression cannot be evaluated for the current input an exception is raised. Note the difference between the program statements \verb^test x = 3^ and \verb^x = 3^. The first raises an exception if \verb^x^ is not in the domain of the input, the second assigns $3$ to \verb^x^ in that case. \begin{code} dorun (Test b) (Ps val g l) | b_val_exp b val == Nothing = [Nothing] | b_val_exp b val == Just True = [Just (Ps val g l)] | b_val_exp b val == Just False = [] \end{code} The {\tt If}\/ statement raises an exception when its Boolean expression cannot be evaluated. Otherwise it picks the branch indicated by the evaluation of the Boolean. \begin{code} dorun (If b s1 s2) (Ps val g l) | b_val_exp b val == Nothing = [Nothing] | b_val_exp b val == Just True = dorun s1 (Ps val g l) | b_val_exp b val == Just False = dorun s2 (Ps val g l) \end{code} Evaluating the {\tt Either}\/ statement is taking the union of the results of the component statements. \begin{code} dorun (Either s1 s2) (Ps val g l) = union (dorun s1 (Ps val g l)) (dorun s2 (Ps val g l)) \end{code} The {\tt Do}\/ statement for bounded iteration evaluates the arithmetical expression for the number of iterations. If this fails, an exception is raised. If it succeeds, the embedded statement is executed the appropriate number of times, or skipped if the control number is not positive. \begin{code} dorun (Do exp s) (Ps val g l) | a_val_exp exp val == Nothing = [Nothing] | otherwise = (doruncomp (iter n s) (Ps val g l)) where Just n = (a_val_exp exp val) iter m s | m <= 0 = [] | otherwise = s:(iter (m-1) s) \end{code} The {\tt Find}\/ statement tries to evaluate the range expressions, and evaluates a {\tt Find1} statement when it finds proper values, and raises an exception otherwise. \begin{code} dorun (Find var (exp1,exp2) s) (Ps val g l) | a_val_exp exp1 val == Nothing = [Nothing] | a_val_exp exp2 val == Nothing = [Nothing] | otherwise = dorun (Find1 var m n s) (Ps val g l) where Just m = (a_val_exp exp1 val) Just n = (a_val_exp exp2 val) \end{code} The {\tt Find1}\/ statement executes a bounded search. \begin{code} dorun (Find1 var m n s) pstate | n < m = [] | m == n = try | otherwise = union try next where try = (doruncomp [id,s] new) new = (doSome var pstate) id = (Iseq (Term (Factor (Var var))) (Term (Factor (Int m)))) next = dorun (Find1 var (m+1) n s) pstate \end{code} The {\tt Not}\/ statement evaluates the embedded statement, and checks the result for safety. \begin{code} dorun (Not stmt) pstate = case (dorun stmt pstate) of [] -> [Just pstate] x | isSafe pstate x -> [] | otherwise -> [Nothing] \end{code} Finally, a {\tt Comp}\/ statement is evaluated by invoking {\tt doruncomp}. \begin{code} dorun (Comp stmts) pstate = doruncomp stmts pstate \end{code} \section{Starting the Dynamo Computation Process} A computation with a \dyn\ program gets as input from the parser a pair \verb^(displayC,vschemes,stmt)^, where \verb^displayC^ indicates whether a display constraint was specified or not, \verb^vschemes^ gives the display constraint, and \verb^stmt^ gives the program statement in the abstract syntactic form produced by the parser. The actual \dyn\ computation is called by {\tt process}, and starts with an empty valuation and empty stores. \begin{code} compute :: Pgm -> (Bool,[Vscheme],[State]) compute (displayC,vschemes,stmt) = (displayC,vschemes, (process stmt)) process :: Stmt -> [State] process stmt = dorun stmt (Ps [] [] []) \end{code} \section{Displaying the Results} The goal is to display all instantiations of the dynamically free variables of a \dyn\ program, and for each of those a {\em sample}\/ instantiation of the dynamically active variables of the program. The dynamically active variables are the variables that are introduced by means of a wide scope {\tt some}\/ statement. Thus, for any given output valuation, the global variables have universal force, the local variables existential force, and we have to clearly indicate the distinction when we display the results. The procedure {\tt splitValues}\/ splits the variable-value pairs in the valuation of a proper state into existentally quantified ones and the universally quantified ones, according to whether or not the variable occurs in the local variable store. Note that {\tt splitValues}\/ effectively reverses a valuation before display. This comes in handy, for the valuation is computed as a stack, with the most recently computed value on top. The net effect of first building a stack and then reversing it is that the valuations are displayed in the order in which they were computed. \begin{code} splitValues :: ProperState -> (Valuation,Valuation) splitValues pstate = splitValues1 pstate [] [] splitValues1 :: ProperState -> Valuation -> Valuation -> (Valuation,Valuation) splitValues1 (Ps [] _ _) uVal eVal = (uVal,eVal) splitValues1 (Ps ((v,d):rest) g l) uVal eVal | elem v l = splitValues1 (Ps rest g l) uVal ((v,d):eVal) | otherwise = splitValues1 (Ps rest g l) ((v,d):uVal) eVal \end{code} In case there are no solutions, we say so. In case the solution has an empty set of global variables, the program was just a check, so we can return `True' as outcome. The output should distinguish between the values that are computed solutions (the universal values) and the values that are mere sample values (the existential values). The list of sample values is preceded by ``e.g.''. \begin{code} showsV :: ProperState -> String -> String showsV pstate string = case (uVals,eVals) of ([],[]) -> "True" otherwise -> showsuVal uVals (showseVal eVals string) where (uVals,eVals) = splitValues pstate showsuVal :: Valuation -> String -> String showsuVal [] string = "True" ++ string showsuVal a string = showsValues a string showseVal :: Valuation -> String -> String showseVal [] string = string showseVal a string = " e.g. " ++ (showsValues a string) showsValues :: Valuation -> String -> String showsValues [] string = ' ':string showsValues ((v,d):rest) string = shows v (':':(shows d (' ':(showsValues rest string)))) \end{code} It is important to inform the user about possible incompleteness of the computed solution set. This is done by means of `There may be solutions, but none were found' if there are only improper outcomes, or `There may be further solutions' if both proper and improper outcomes are generated. {\tt showStates} displays the solution set, and gives informative feedback on possible incompleteness of the computed answer. Note that \verb^(chr 10)^ is a representation for the ``newline'' character. It is possible to refer to ``newline'' in Haskell directly, by means of \verb^'\n'^, but we refrain from doing so as this confuses the \LaTeX\ processor. \begin{code} showStates :: [State] -> String showStates [] = "False" showStates [Nothing] = "There may be solutions, but none were found" showStates (Nothing:states) = showMaybeStates states showStates (Just pstate:states) = showsV pstate (showMoreStates states) showMaybeStates :: [State] -> String showMaybeStates [] = "There may be solutions, but none were found" showMaybeStates [Nothing] = "There may be solutions, but none were found" showMaybeStates (Nothing:states) = showMaybeStates states showMaybeStates (Just pstate:states) = showsV pstate (showMaybeMoreStates states) showMoreStates :: [State] -> String showMoreStates [] = (chr 10):"There are no further solutions" showMoreStates [Nothing] = (chr 10):"There may be further solutions" showMoreStates (Nothing:states) = showMaybeMoreStates states showMoreStates (Just pstate:states) = (chr 10):(showsV pstate (showMoreStates states)) showMaybeMoreStates :: [State] -> String showMaybeMoreStates [] = (chr 10):"There may be further solutions" showMaybeMoreStates [Nothing] = (chr 10):"There may be further solutions" showMaybeMoreStates (Nothing:states) = showMaybeMoreStates states showMaybeMoreStates (Just pstate:states) = (chr 10):(showsV pstate (showMaybeMoreStates states)) \end{code} \section{Pruning the State Space} If a display list of variable schemes is given at the beginning of the program, we select those variables from the valuation that satisfy a scheme from the list. For this, we first need to decompose a variable into its variable scheme: its identifier prefix, plus a number indicating the count of indices. \begin{code} decompVar :: Variable -> Vscheme decompVar varstring = case break (== '[') varstring of (x,[]) -> (x,0) (x,(y:ys)) | '[' `elem` ys -> (x,2) | otherwise -> (x,1) \end{code} {\tt varForm} checks whether a variable satisfies a display list of schemes. \begin{code} varForm :: Variable -> [Vscheme] -> Bool varForm variable [] = False varForm variable ((s,i):rest) = ((s,i) == (decompVar variable)) || varForm variable rest \end{code} In any case, we don't want to see all the values of the local variables. If a local variable is required for display, one example instantiation is enough. If a display constraint was specified, we prune away all variables from the valuations that are not specified by the display requirements. \begin{code} pruneStates :: (Bool,[Vscheme],[State]) -> [State] pruneStates (displayC,schemes,states) | displayC == False = pruneStates1 states [] [] | otherwise = pruneStates2 schemes states [] [] pruneStates1 :: [State] -> [Valuation] -> [State] -> [State] pruneStates1 [] vals states = states pruneStates1 (Nothing:states) vals newstates = (Nothing:(pruneStates1 states vals newstates)) pruneStates1 (Just (Ps a g l):states) vals newstates | val `elem` vals = (pruneStates1 states vals newstates) | otherwise = (pruneStates1 states (val:vals) (Just (Ps val g l):newstates)) where val = [ (x,d) | (x,d) <- a, x `elem` g] pruneStates2 :: [Vscheme] -> [State] -> [Valuation] -> [State] -> [State] pruneStates2 schemes [] vals states = states pruneStates2 schemes (Nothing:states) vals newstates = (Nothing:(pruneStates2 schemes states vals newstates)) pruneStates2 schemes (Just (Ps a g l):states) vals newstates | val `elem` vals = (pruneStates2 schemes states vals newstates) | otherwise = (pruneStates2 schemes states (val:vals) (Just (Ps val g l):newstates)) where val = [ (x,d) | (x,d) <- a, x `elem` g, varForm x schemes] \end{code} \section{Wrapping it all up} Ask for a program, lexicalize and parse its contents, compute the output valuations, and prune and display the results: \begin{code} main = do putStr "Input program: " ifile <- getLine readFile ifile >>= (putStr . showStates . pruneStates . compute . parse . lexer) mainw = do putStr "Input program: " ifile <- getLine s <- readFile ifile writeFile "dynamo.output" ((showStates . pruneStates . compute . parse . lexer) s) putStr "result written to file" \end{code} \bibliographystyle{plain} \bibliography{/ufs/jve/texmacros/fracasV1-7,/ufs/jve/papers/pwdpl/pwdpl,dynamo} %\bibliography{/home/jve/texmacros/fracasV1-7,/home/jve/papers/pwdpl/pwdpl,dynamo} \end{document}