\batchmode
\documentstyle[twoside,11pt,htmllist,html,epsf]{article}
\makeatletter


\title{Lifeworld Analysis}

\author{ Philip Agre pagre@ucsd.edu \\ 
        Department of Communication 0503 \\ 
        University of California, San Diego \\ 
        La Jolla, CA 92093, USA \\ 
        and \\ 
        Ian Horswill ian@ils.nwu.edu \\ 
        Northwestern University Computer Science Department \\ 
        1890 Maple Avenue \\ 
	Evanston, IL 60201, USA}





\makeatletter


{\catcode`\ =\active\gdef\vobeyspaces{\catcode`\ =\active\let =\@xobeysp}}


{\catcode`\^^I=\active\gdef\vobeytabs{\catcode`\^^I=\active\let^^I=\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp}}




{\catcode`\^^M=\active\gdef\vobeylines{\catcode`\^^M=\active\let^^M=\par\penalty10000{}}}




{\catcode`\^^M=\active\gdef\obeycrsp{\catcode`\^^M=\active\let^^M=\@xobeysp}}


\begingroup
\catcode``=13
\gdef\@noligs{\let`=\@lquote}
\endgroup




















\makeatother












































































\newcounter{myenumerator}






\def\xvobeytabs{\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp\@xobeysp}

\def\xvobeylines{\par\penalty10000{}}

\def\setupcode{\small\tt\frenchspacing\catcode``=13\@noligs\def  \\ {\char`\\ }\@makeother\_\@makeother\#\@makeother\&\@makeother\^\@makeother\$\@makeother\`\@makeother\'\@makeother\~\@makeother\@\@makeother\"\@makeother\%\vobeytabs\vobeyspaces}

\newenvironment {bigcode}{\list{}{\parsep=0pt}\item[]\setupcode\obeylines}{\endlist}

\newenvironment {code}{\list{}{\parsep=0pt}\item[]\setupcode\vobeylines}{\endlist}

\newcommand {\codeskip}{\vspace{2ex}}

\newcommand {\cd}{\begingroup\setupcode\obeycrsp\startcode}

\newcommand {\startcode}[1]{#1\endgroup}

\newcommand {\sexp}[1]{{\tt #1}}

\newcommand {\ignore}[1]{}

\newcommand {\w}{\vec{\omega}}

\newcommand {\implies}{\Rightarrow}

\newtheorem {definition}{Definition}

\newtheorem {proposition}{Proposition}

\newtheorem {theorem}{Theorem}

\newtheorem {lemma}{Lemma}

\newtheorem {claim}{Claim}

\newtheorem {corollary}{Corollary}

\newtheorem {observation}{Observation}

\newcommand {\proof}{\noindent {\it Proof: }}

\newcommand {\denseitems}{
   \setlength{\itemsep}{0in}
   \setlength{\parskip}{0in}}

\newcommand {\onetoone}{$1\colon\!1$ }

\newcommand {\fdef}[3]{#1\colon\!#2\!\!\rightarrow\!\!#3}

\newcommand {\qed}{$\; \Box$ \par \bigskip}

\newcommand {\nbox}[1]{\framebox{\ $#1\rule[-.1in]{0in}{.25in}$\ }}

\newcommand {\psystem}{\Rightarrow\!\!}

\newcommand {\feeds}{\!\!\rightarrow\!\!}

\newcommand {\reals}{{\cal R}}

\newcommand {\nextbox}[1]{\nbox{#1}\feeds}

\newcommand {\firstbox}[1]{\psystem\nextbox{#1}}

\newcommand {\rfirstbox}[1]{\firstbox{$\makebox{#1}$}}

\newcommand {\rnextbox}[1]{\nextbox{$\makebox{#1}$}}

\newcommand {\ceq}[1]{\stackrel{{\small #1}}{=}}

\newcommand {\cequiv}[1]{\stackrel{{\small #1}}{\equiv}}

\newcommand {\capprox}[1]{\stackrel{{\small #1}}{\approx}}

\newcommand {\world}{{\cal W}}

\newcommand {\images}[1]{{\cal I}(#1)}

\newcommand {\x}{{\bf x}}

\newcommand {\X}{{\bf X}}

\newcommand {\y}{{\bf y}}

\newcommand {\Y}{{\bf Y}}

\newcommand {\T}{{\bf T}}

\newcommand {\R}{{\bf R}}

\newcommand {\f}{{\bf f}}

\newcommand {\h}{{\bf h}}

\newcommand {\z}{{\bf z}}

\newcommand {\Z}{{\bf Z}}

\newcommand {\p}{{\bf p}}

\newcommand {\bP}{{\bf P}}

\newcommand {\psfigure}[1]{\epsfbox{/home1/ian/words/figures/#1}}

\newcommand {\centerfig}[1]{\centerline{\epsfxsize=\textwidth \psfigure{#1}}}

\newcommand {\sizedfig}[2]{{\epsfxsize=#1 \psfigure{#2}}}

\newcommand {\smallfig}[1]{\centerline{\epsfxsize=4in \psfigure{#1}}}

\newcommand {\halffig}[1]{{\epsfxsize=2.5in \psfigure{#1}}}

\newcommand {\normalfig}[1]{\centerline{\psfigure{#1}}}

\newcommand {\ddt}[1]{{{d#1} \over {dt}}}

\newcommand {\sg}{{\cal G}}

\newcommand {\sL}{{\cal L}}

\newcommand {\etal}{{\it et al.\ }}

\newcommand {\eg}{{\it e.g.\ }}

\newcommand {\ie}{{\it i.e.\ }}

\newcommand {\etc}{{\it etc.}}

\newcommand {\camdepth}{\makebox{{\rm Camera-Depth}}}

\newcommand {\bodydepth}{\makebox{{\rm Body-Depth}}}

\newcommand {\pproduct}{\!\parallel\! }

\newcommand {\sproduct}{\!\rightleftharpoons\! }

\newcommand {\zahl}{{\cal Z}}

\newcommand {\const}[1]{{{\cal C}_{#1}}}

\newcommand {\narrowtimes}{\!\!\times\!\!}

\newcommand {\cn}{{\cal N}}

\newcommand {\action}[1]{\stackrel{{\rm #1}}{\rightarrow}}

\newcommand {\chain}{{\cal C}}

\newcommand {\singleton}{{\cal S}}

\newcommand {\actionmap}[1]{{\cal A}_{#1}}

\newcommand {\gloss}[2]{\par \noindent {\bf #1}.  #2}

\newcommand {\mgloss}[2]{\par \noindent $#1$.  #2}

\newcommand {\heading}[1]{\par \bigskip \noindent {\it #1} \par \bigskip}

\def\bbullets{\begin{list}{$\bullet$}{\itemsep -3pt}}

\def\ebullets{\end{list}}

\def\benumerate{\begin{list}{(\arabic{myenumerator})}{\usecounter{myenumerator}\itemsep -3pt}}

\def\eenumerate{\end{list}}

\newcommand {\citeyear}[1]{\cite{#1}}

\def\goesto{$\rightarrow$}

\makeatother
\newenvironment{tex2html_wrap}{}{}
\newwrite\lthtmlwrite
\def\lthtmltypeout#1{{\let\protect\string\immediate\write\lthtmlwrite{#1}}}%
\newbox\sizebox
\begin{document}
\pagestyle{empty}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{lemma}\label{parallel-product-policy}
Let $p_1$ be a policy which solves $D_1$ and halts from all states in
some set of initial states $I_1$, and let $p_2$ be a policy which
solves $D_2$ and halts from all states in $I_2$.  Then the policy
\begin{displaymath} p(x,y) = p_1(x) \!\!\times\!\! p_2(y) \end{displaymath}
solves $D_1\!\parallel\! D_2$ and halts from all
states in $I_1\!\!\times\!\! I_2$.  (Note that here we are using the
convention of treating $p$, a function over pairs, as a function over
two scalars.)
\end{lemma}
}

{\newpage
\clearpage
\samepage \begin{lemma}% latex2html id marker 284
\label{serial-product-policy}
Let $p_1$ be a policy which solves $D_1$ from all states in some set
of initial states $I_1$, and let $p_2$ be a policy which solves $D_2$
{}from all states in $I_2$.  Then any policy for which
\begin{displaymath} p(x,y) = p_1(x) \!\!\times\!\! i {\rm ~or~} i \!\!\times\!\! p_2(y) \end{displaymath}
and
\begin{eqnarray*}
y \in G_2, x\not\in G_1 & \Rightarrow & p(x,y) = p_1(x) \!\!\times\!\! i \\ 
x\in G_1, y\not\in G_2 & \Rightarrow & p(x,y) =  i \!\!\times\!\! p_2(y) 
\end{eqnarray*}
will solve $D_1\!\rightleftharpoons\! D_2$ and halt from all states
in $I_1\!\!\times\!\! I_2$.
\end{lemma}
}

\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{lemma}% latex2html id marker 304
\label{simple-reduction-lemma}
Let $\pi$ be a simple reduction from $E'$ to some environment $E$ and
let $(E',G')$ be a DCP.  If a policy $p$ solves $(E,\pi(G'))$, then
\begin{displaymath} p_{\pi} = {\cal A}_{\pi} \circ p \circ \pi \end{displaymath}
solves $(E', G')$.
\end{lemma}
}

\stepcounter{subsection}
\stepcounter{section}
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{proposition}All single-material worlds of $n$ states are reducible
to $\chain_n$
\end{proposition}
}

{\newpage
\clearpage
\samepage \begin{corollary}If a goal $G$ is solvable in a single-material environment $E$ with no
tools, then it is solved by the policy \label{standard-policy-page}
\begin{displaymath} p_{E,G}(s) = \left\{ \begin{array}{ll}
i, & {\rm if} s \in G \\ 
(action(s))(s), & {\rm otherwise}
\end{array} \right.
\end{displaymath}
\end{corollary}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{proposition}Any environment $M$ is isomorphic to $M\!\parallel\!\singleton^n$.
\end{proposition}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{lemma}Any environment with tool components can be reduced to one in which
the tools have been replaced by singletons.  Specifically, let
$D=((S,A),G)$ be a DCP and let $ready_T \in T$, and $A' = \{ a'\colon
(s, ready_T)\mapsto (a(s), t) | a\in A, s\in S, {\rm and}~t\in T\}$.
Then $D'=((S\times T, A'\cup A_t), G\times \{ ready_T \})$ is reducible to
$D$ when $T$ is a tool in $D'$.
\end{lemma}
}

\stepcounter{subsection}
\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{lemma}Let $\pi$ be a binding of $E$ to $E'$.  Then ${\cal A}_{\pi}$ is
given by
\begin{displaymath} {\cal A}_{\pi}(a) = a_\pi, {\rm~where~} a_\pi(s') = \pi^-(a(\pi(s')),s') \end{displaymath}
That is, the implementation of an $E$-action is simply $\pi$'s
back-projection composed with that action and $\pi$.
\end{lemma}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{lemma}\label{bound-policy}
If policy $p$ is a solution for the problem $(E,G)$ from initial
states $I$, and $\pi$ is a binding from $E'$ to $E$, then
\begin{displaymath} p_{\pi} = {\cal A}_{\pi} \circ p \circ \pi \end{displaymath}
is a solution for $(E',\exists_{E,E'}G)$ from initial states
$\pi^{-1}(I)$, where ${\cal A}_{\pi}$ is the function mapping actions in $E$ to
their corresponding actions under $\pi$ in $E'$.
\end{lemma}
}

\stepcounter{subsubsection}
{\newpage
\clearpage
\samepage \begin{proposition}The policy
\begin{displaymath} p_{M_0}(s) = ({\cal A}_{M_0(s)}\circ p \circ (M_0(s)))(s) \end{displaymath}
is a solution from any state for which $M_0$ is defined.
\end{proposition}
}

\stepcounter{subsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{lemma}\label{interleaved-goals}
Let $p_1 = {\cal A}_{\pi_1} \circ p'_1 \circ \pi_1$ and $p_2 =
{\cal A}_{\pi_2} \circ p'_2 \circ \pi_2$ be policies
that solve the goals $G_1$ and $G_2$, respectively, and halt.  If
$\pi_1$ and $\pi_2$ are independent and $I$ is a fair interleaving for
$p_1$ and $p_2$ then $I_{p_1,p_2}$ solves $G_1 \cap G_2$ and halts.
\end{lemma}
}

{\newpage
\clearpage
\samepage \begin{corollary}\label{interleaved-bindings}
If $p_1 = {\cal A}_{\pi_1} \circ p \circ \pi_1$ and $p_2 =
{\cal A}_{\pi_2} \circ p \circ \pi_2$ be policies
that solve the goals $G_1$ and $G_2$, respectively, and halt, and $I$
is a fair interleaving for $p_1$ and $p_2$, then ${\cal A}_{I_{\pi_1,
\pi_2}} \circ p \circ I_{\pi_1, \pi_2}$ solves $G_1 \cap G_2$ and halts.
\end{corollary}
}

\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
{\newpage
\clearpage
\samepage \begin{proposition}Let $E=(S,A)$ be an environment, $p$ be a policy that solves some goal
$G$ in $E$ and halts, and let $D$ be an environment with two states, 0
and 1, and two actions, $i$ (the identity) and $flip$ which moves the
environment into the opposite state from its present state.  Consider
the product environment:
\begin{displaymath} E' = E \!\rightleftharpoons\! E \!\rightleftharpoons\! D \end{displaymath}
and the binding map from $E'$ to $E$:
\begin{displaymath} M_D (s_0, s_1, d) = s_d \end{displaymath}
Any fair interleaving of the policies:
\begin{displaymath} p_{M_D} = {\cal A}_{M_D} \circ p \circ M_D \end{displaymath}
and
\begin{displaymath} p_{flip}(s_0, s_1, d) = i\times flip \end{displaymath}
is a solution to the problem $(E',(G \times G \times \{0,1\}))$.
\end{proposition}
}

\stepcounter{section}
\stepcounter{section}
\stepcounter{section}
\stepcounter{section}

\end{document}
