\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,amsfonts,amssymb,amsthm}

\newtheorem{theorem}{Claim}
\newcommand{\mfr}[1]{\mathcal{#1}}

\DeclareMathOperator{\pess}{pessimistic}
\DeclareMathOperator{\ambi}{ambivalent}
\DeclareMathOperator{\opti}{optimistic}
\DeclareMathOperator{\dleft}{left}
\DeclareMathOperator{\dstay}{stay}
\DeclareMathOperator{\dright}{right}
\DeclareMathOperator{\persona}{\mbox{Waldo}}

\begin{document}

\par\noindent{\bf CS81 HW\#4 Spring 2012} {\em Out: 02/08/2012. Due: 02/15/2012 (before class)} 
\paragraph{\bf Policy on homeworks}
\begin{enumerate}
\item {\em Collaboration}:
        You may discuss a question with any other student currently taking CS81 provided:
        (i) both of you contribute equally;
        (ii) you come away from any discussion with an understanding in your mind (and no archived solution of any form is retained);
        (iii) your submission is your own work prepared by yourself on a separate occassion.

\item {\em Reference materials}:
        You should only refer to materials from this semester of CS81
        (class notes, handouts, textbooks, grutors, instructor, etc).

\item {\em Submission}:
        Your submission should be legible or is prepared using TeX.
\end{enumerate}

\paragraph{Logical Problems}
\begin{enumerate}

\item Let $L_{S}$ be a first-order language with one constant $e$ and one binary function $f$.
	So $S = \{e^{(0)},f^{(2)}\}$. Consider the following first-order sentences over $L_{S}$.
	\begin{eqnarray*}
	\phi_{1} & = & (\forall x)(\forall y)(\forall z)[f(x,f(y,z)) = f(f(x,y),z)] \\
	\phi_{2} & = & (\forall x)[f(x,e) = x] \\
	\phi_{3} & = & (\forall x)(\exists y)[f(x,y) = e] \\
	\phi_{4} & = & (\forall x)(\exists y)[f(y,x) = e] \\
	\phi_{5} & = & (\forall x)[(\forall y)(f(y,x) = y) \to (x = e)] \\
	\phi_{6} & = & (\forall x)(\forall y)(\forall z)[(f(x,z) = e) \to (f(f(x,y),z) = y)] \\
	\phi_{7} & = & (\forall x)(\forall y)(\forall z)[((f(x,y) = e) \wedge (f(x,z) = e)) \to (y = z)]
	\end{eqnarray*}
	Let $\Phi = \{\phi_{1},\phi_{2},\phi_{3}\}$.
	Prove or disprove the following semantic entailments:
	\begin{enumerate}
	\item $\Phi \models \phi_{4}$.
	\item $\Phi \models \phi_{5}$.
	\item $\Phi \models \phi_{6}$.
	\item $\Phi \models \phi_{7}$.
	\end{enumerate}
	You may need to invoke some rules on equality.

\item Imagine $\persona$ playing a game on a Boolean circular array of size $N$. 
	\begin{enumerate}
	\item Each cell of the array contains either $\bot$ or $\top$.
	\item $\persona$'s state of mind can either be $\pess$, $\ambi$, or $\opti$.
	\item $\persona$'s initial position on the array is at location $0$, but he is allowed to move 
		after each step to his left or right. If he moves left from $0$ then he will arrive at 
		location $N-1$. Similarly, moving right off $N-1$ will get him to $0$.
	\item At each step of the game, $\persona$ decides based on his current state of mind (say $q$)
		and the contents of the array cell at his current location (say $a$), 
		what his state of mind will be on the next step (say $q'$), 
		what symbol to write to the current location of the array (say $b$),
		and whether to move left or right within the circular array (say $d$).
		All this can be encoded as a table of mood transitions of the form
		$(q,a) \mapsto (q',b,d)$:
		\begin{eqnarray*}
		(\pess,\bot) & \mapsto & (\pess,\bot,\dleft) \\
		(\ambi,\bot) & \mapsto & (\pess,\top,\dleft) \\
		(\opti,\bot) & \mapsto & (\ambi,\bot,\dright) \\
		(\pess,\top) & \mapsto & (\ambi,\bot,\dleft) \\
		(\ambi,\top) & \mapsto & (\opti,\bot,\dright) \\
		(\opti,\top) & \mapsto & (\opti,\top,\dright)
		\end{eqnarray*}
	\item $\persona$'s initial state of mind is $\pess$.
	\item $\persona$ plays $T$ steps of this game. 
	\end{enumerate}
	For example, after $N=5$ steps on input $[\top,\top,\top]$, $\persona$ ends up at $0$
	feeling $\ambi$ and leaving the array as $[\bot,\bot,\bot]$.
	Consider the following propositional atoms:
	\begin{itemize}
	\item $S(t,q) = \top$ if and only if at step $t$ $\persona$'s state of mind is $q$.
	\item $L(t,j) = \top$ if and only if at step $t$ $\persona$'s location is $j$.
	\item $M(t,j,b) = \top$ if and only if at step $t$ the contents of array cell $j$ is $b$.
	\end{itemize}
	Here $0 \le t \le T$, $q \in \{\pess,\ambi,\opti\}$, $0 \le j < N$, and $b \in \{\bot,\top\}$.

	Express each of the following conditions as propositional formulas:
	\begin{enumerate}
	\item[C1] At each step $t$, $\persona$ is in exactly one state of mind.
	\item[C2] At each step $t$, $\persona$ is located at exactly one array location.
	\item[C3] At each step $t$, each cell of the array contains exactly one Boolean value.
	\item[C4] The initial condition at step $0$ is that $\persona$ is pessimistic and is at location $0$,
		and the contents of the array is specified by a set of variables $x_{0},\ldots,x_{N-1}$.
	\item[C5] The states of the game between steps $t$ and $t+1$ obeys the transition table given above.
	\item[C6] The final condition at step $T$ is that $\persona$ is $\opti$ and is back at location $0$.
	\end{enumerate}
	As an example, for C4 we should have the formula:
	\[
		\phi_{4} = S(0,\pess) \wedge L(0,0) \wedge \bigwedge_{j=0}^{N-1} M(0,j,x_{j})
	\]
	State your formulas in {\em clausal} form (a conjunctive collection of disjunctions).

\end{enumerate}

\end{document}

