\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}
Click to toggle
does not end with </html> tag
does not end with </body> tag
The output has ended thus: \noindent{}\point rel\_op: Rexp * $\Gamma \rightarrow$ Bool(b) \vspace{12pt} \end{document}