\documentclass[11pt]{article}
\input{/home/fac2/blair/TeX/macros}
\newcommand{\ggets}{\mbox{:=}}
\begin{document}
\thispagestyle{empty}
\begin{center}
{\Large {\bf Semantics of Programming Languages Comprehensive}}\\
{\Large {\bf January 7, 1998}}
\end{center}
\par
\noindent
{\large\sc Instructions}. Do all questions. You have 4 hours.
\par
\skp{2}
\noindent
{\bf Question 1}:
All of the variables in the following command are integer
variables.
\par
\noindent
Give a formal proof (or natural deduction
style proof-tree) that
the following specification is partially correct:
\[
\mbox{\small
\{N $\geq$ 0 and N is even\}~X~:=~N;~Y~:=~N;~{\bf while}~Y~$>$~0~%
{\bf do}~(X~:=~X~-~1;~Y~:=~Y~-~2)~\{X~=~N~div~2\}
}
\]
\par
\skp{3}
\noindent
{\bf Question 2}:  There are many parts to this question.
Read all of the parts before you try to start answering.  In
most cases the questions have concise answers that can quickly
be written down.  (Part(i) is the exception; that may be a
little longer.)  When you are asked to give an example, be
concise.  
\par
\skp{1}
\noindent
{\bf Definition:}  A {\em domain} is an $\omega$-complete
partial order.  (If you have forgotten the definition of an
$\omega$-complete partial order, you can infer it from
part(a).)
\par
\skp{1}
\noindent
{\bf Part a:} Give an example of a partially ordered set in which every 
subset has an upper bound, but for which there is at least one 
chain which does not have a least upper bound.  (Hence, your
example would be an example of a partially ordered set in
which every subset has an upper bound, but which
is not a domain because it is not $\omega$-complete.)
\par
\skp{1}
\noindent
{\bf Part b:}  Consider the simple imperative language, as in
{\em Tennent}.  What is a state?
\par
\skp{1}
\noindent
{\bf Part c:}  Given a nonempty set $S$, we may consider the 
{\em discrete} partially ordered set $\ddot{S} = (S,
\sqsubseteq)$  whose partial order is defined by 
\[
s_{1} \sqsubseteq s_{2}\ \ \mbox{iff}\ \ s_{1} = s_{2}\,.
\]
Show that $\ddot{S}$ is a domain.
\par
\skp{1}
\noindent
{\bf Part d:} Show that if $D$ is a domain, then so is the {\em
raised} set $D_{\bot}$.  
\par
\skp{1}
\noindent
{\bf Part e:}
Let $D$ be the discrete domain on three elements $a$, $b$, and
$c$.  Describe the ordering on $D_{\bot}$.  (Just draw a
diagram.)
\par
\skp{1}
\noindent
{\bf Part f:}
Let $D$ be a domain and $S$ just an ordinary nonempty set.
Show that the set $S \longrightarrow D$, ordered by 
\[
f \sqsubseteq g\ \ \mbox{iff}\ \ \mbox{for all}\ s \in S: 
f(s) \sqsubseteq_{D} g(s)
\]
is a domain.
\par
\skp{1}
\noindent
{\bf Definition:}  Let $D_{1}$ and $D_{2}$ be domains with
partial orders $\sqsubseteq_{1}$ and $\sqsubseteq_{2}$,
respectively. Let $f\,:\,D_{1} \longrightarrow D_{2}$.  
$f$ is {\em monotone} iff $x \sqsubseteq_{1} y$ implies $f(x) 
\sqsubseteq_{2} f(y)$ for all $x,y$ in $D_{1}$.  Also, $f$ is
$\omega$-{\em compact} iff for every chain $\{x_{i}\mid i \in
\Nat\}$ in $D_{1}$, the least upper bound, 
$\displaystyle{\bigsqcup^{\infty}_{i=0}f(x_{i})}$ is defined
in $D_{2}$ and
$f(\displaystyle{\bigsqcup^{\infty}_{i=0}}x_{i})
\sqsubseteq_{2}
\displaystyle{\bigsqcup^{\infty}_{i=0}f(x_{i})}$. $f$ is
{\em $\omega$-continuous} iff $f$ is monotone and $\omega$-compact.
(This definition agrees with Tennent's definition of continuity
on $\omega$-complete partial orders.
\par
\skp{1}
\noindent
{\bf Part g:} Give an example of an $\omega$-compact function
$f\,:\, D \longrightarrow D$, where $D$ is a domain, 
which is not monotone.
\par
\skp{1}
\noindent
{\bf Part h:}  Let $D$ be a domain with a bottom element $\bot$
and let 
$f\,:\,D \longrightarrow D$ be $\omega$-continuous.  Show that 
$\displaystyle{\bigsqcup^{\infty}_{i=0}f^{i}(\bot)}$
is the least fixed point of $f$.  i.e.
if $a = \displaystyle{\bigsqcup^{\infty}_{i=0}f^{i}(\bot)}$
then $f(a) = a$ and for all $d$ such that $f(d) = d$, $a
\sqsubseteq d$.
\par
\skp{1}
\noindent
{\bf Part i:}  Let $S$ be the set of states of the simple
imperative language.  The set of all partial functions from $S$
to $S$, denoted by $S \rightharpoonup S$, is identifiable with
the set of functions
\[
S \longrightarrow \ddot{S}_{\bot}
\]
Let $\beta$ be a function from $S$ to $\{\mbox{\em
true},\mbox{\em false}\}$.  Let $\kappa$ be a function in
$\ddot{S}_{\bot} \longrightarrow \ddot{S}_{\bot}$
Now, define
\[
\Gamma_{\beta,\kappa}\,:\,(S \longrightarrow \ddot{S}_{\bot})
\longrightarrow (S \longrightarrow \ddot{S}_{\bot})
\]
by 
\[
\Gamma_{\beta,\kappa}(c) = \mathbf{\lambda} s.%
\left\{
\begin{array}{lr}
c(\kappa(s)) & \mbox{if}\ \beta(s) =\ \mbox{\em true}\\
s            & \mbox{if}\ \beta(s) =\ \mbox{\em false}
\end{array}
\right.
\]
Show that $\Gamma_{\beta,\kappa}$ is $\omega$-continuous.
\par
\skp{1}
\noindent
{\bf Part j:}
The preceding development applies elementary techniques about
domains to obtain the semantics of the while-command.  Explain
how.  (Note that by part(h), $\Gamma_{\beta,\kappa}$ has a
least fixed point.  Let $\beta$ be the meaning of a Boolean
expression B, and let $\kappa$ be the meaning of a command C.
Explain how $\Gamma_{\beta,\kappa}$ is related to the semantics of {\bf
while}~B~{\bf do}~C.)
\par
\skp{3}
\noindent
{\bf Question 3}:  Compare and contrast states vs.
environments.  (Think of states with regard to
the semantics of the simple imperative language and think of
environments with regard to the semantics of the simple 
recursive applicative language.)
\end{document}
