\documentclass[11pt]{article} 

\input{defs}

\usepackage{graphicx}
\usepackage{fullpage}
\usepackage{amsfonts}



\title{Diderot Formal Semantics} 
\author { 
	John Reppy \\
	University of Chicago \\
	{\small\tt{}jhr@cs.uchicago.edu} \\
\and
	Lamont Samuels \\
	University of Chicago \\
	{\small\tt{}lamonts@cs.uchicago.edu} \\
}
\date{\today} 

\begin{document} 
\maketitle
\thispagestyle{empty}



\section{Abstract Syntax}

\noindent{}\point Definitions:  variable := string \textbar{} id := integer

\noindent{}\point Values:  v := Num(n)  \textbar{}  Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...?? 

\noindent{}\point Commands (Comms): 
\begin{displaymath} 
	\begin{array}{rclr} 
 	\text{c} &  ::=  &\text{x := e}  & \text{for x = variable, e} \in\text{Aexp}\\
		   & \mid & \text{$c_1 $;  $c_2 $}  &\text{for $c_1$, $c_2$} \in\text{Comms} \\
		   & \mid & \text{$ if\:r\:then\:c_1\:else\:c_2 $}  &\text{for $c_1$, $c_2$} \in\text{Aexp and b} \in\text{Rexp}  \\
		   & \mid & \text{stabalize}  	   
    \end{array}
 \end{displaymath}  


\section{Strand Environment}  
\begin{displaymath} 
		\begin{array}{l} 
		\noindent{}strand \US status  :=  \{ Active, Stabilized, Dead \}  \times{}  env \\
		\noindent{}strand \US env := strand \US status \times{} id  \times{} comms \\
		\noindent{}env := variable   \rightarrow{} value
		\end{array}
\end{displaymath} %



\section{Global Environment} 
The $\cup $ character denotes a parallel construct that states that every stand environment
runs in parallel with each other. 

\begin{center} 
$\displaystyle \bigcup_{\substack {id \in strand\_env \\ 
 \Gamma = id \rightarrow strand\_env} }{update(\Gamma(id),\Gamma)} $
\end{center} 
 \vspace{12pt}
dom($\Gamma$) := all active \& stabilized strand environments 

\noindent{}newId := $\Gamma$ * id $\rightarrow$ id 



\section{Inference Rules} 

\noindent{}\point Update function: strand\_env * $ \Gamma \rightarrow \Gamma'$ 
\vspace{12pt}
%\begin{center} 


%$ \INFER{update((Active,env),id,c),\Gamma)\Downarrow \Gamma'[(new\_status,env')/id]}
%	       {comm\_eval((Active,env),c,id,\Gamma) \Downarrow (new\_status,env',\Gamma')}$

%\end{center}

%\vspace{12pt}
%\noindent{}\point comm\_eval: strand\_status * commands * id * $ \Gamma \rightarrow $  strand\_status * env * $\Gamma' $
\vspace{12pt} 

\begin{center} 
\CommEval{stabalize}{(Stablize,env,\Gamma)}{} 

%$ \INFER{comm\_eval((s,env),stabalize,id,\Gamma)\Downarrow (Stablize,env,\Gamma)}{}$ 
%\vspace{24pt}

\CommEval{die}{(Dead,env,\Gamma)}{} 

%$ \INFER{comm\_eval((s,env),die,id,\Gamma)\Downarrow (Dead,env,\Gamma)}{}$ 
%\vspace{24pt}
% $\INFER{comm\_eval((s,env),x:=e,id,\Gamma)\Downarrow (s,env[x:=v],\Gamma)}{\ExpEval{env}{e}{v}} $
%\vspace{24pt}

\CommEval{c_1; c_2}{(s'',env'',\Gamma'')}{\ExpEval{c_1} {(s,env) + \Gamma)} {(s',env',\Gamma')}}

%$ \INFER{comm\_eval((s,env),c_1; c_2,id,\Gamma)\Downarrow (s',env'',\Gamma'')}
	%      {comm\_eval((s,env),c_1,\Gamma)  \Downarrow  (s',env',\Gamma') \hspace{.2in} comm\_eval((s',env),c_2,\Gamma') \Downarrow (s'',env'',\Gamma'')}$ 
%\vspace{24pt}

$ \INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,id,\Gamma)\Downarrow (s',env',\Gamma')}
	      {rel\_op(b,env)  \Downarrow Bool(true)  \hspace{.2in} comm\_eval((s,env),c_1,\Gamma) \Downarrow (s',env',\Gamma')}$ 
\vspace{24pt}

$ \INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,\Gamma)\Downarrow (s',env',\Gamma')}
	      {rel\_op(b,env)  \Downarrow Bool(false)  \hspace{.2in} comm\_eval((s,env),c_2,\Gamma) \Downarrow (s',env',\Gamma')}$ 
\vspace{24pt}


$ \INFER{comm\_eval((s,env), spawn,id,\Gamma)\Downarrow (s,env,\Gamma[id'])}
	      {newId(\Gamma,id)  \Downarrow id'}$ 
	      
\end{center}

\vspace{12pt}
\noindent{}\point expr\_eval:  Aexp * $ \Gamma \rightarrow $ v
\vspace{12pt} 

\noindent{}\point rel\_op:  Rexp * $ \Gamma \rightarrow $ Bool(b)
\vspace{12pt} 


\end{document}

<script type="text/javascript">//<![CDATA[
		function toggle_ffErrors() {
			var errorsblock = document.getElementById("ffErrorsBlock");
			var errorsgroup = document.getElementById("ffErrors");
			if (errorsblock.style.display == "none") {
				errorsblock.style.display = "block";
				errorsgroup.style.right = "10px";
			} else {
				errorsblock.style.display = "none";
				errorsgroup.style.right = "300px";
			}
		}
//]]></script>
<div id="ffErrors">
<a href="javascript:toggle_ffErrors();">Click to toggle</a>
<div id="ffErrorsBlock">
	<div class="error">does not end with &lt;/html&gt; tag</div>
	<div class="error">does not end with &lt;/body&gt; tag</div>
	<div class="info">The output has ended thus:  

\noindent{}\point rel\_op:  Rexp * $ \Gamma \rightarrow $ Bool(b)
\vspace{12pt} 


\end{document}</div>
</div></div>
</body></html>