\documentclass[11pt]{article} \usepackage{proof} \usepackage{amsmath} \usepackage{graphicx} \usepackage{fullpage} \usepackage{amsfonts} \newcommand{\point}{\textbullet~} \newcommand{\INFER}[2]{\begin{array}{c}\infer{#1}{#2}\end{array}} \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 \vspace{12pt} \noindent{}\point Values: v := Num(n) \textbar{} Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...?? \vspace{12pt} \noindent{}\point Arithmetic expression (Aexp): \begin{displaymath} \begin{array}{rclr} \text{e} & ::= & n &\text{for n} \in\mathbb{R} \\ & \mid & \text{x} &\text{for x = variable} \\ & \mid & \text{$e_1$ + $e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1$ - $e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1$ * $e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1$ / $e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ \end{array} \end{displaymath} \noindent{}\point Relational expression (Rexp): \begin{displaymath} \begin{array}{rclr} \text{r} & ::= &\text{true} \\ & \mid & \text{false} \\ & \mid & \text{$e_1 == e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1 < e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1 > e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1 \leq e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ & \mid & \text{$e_1 \geq e_2$} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\ \end{array} \end{displaymath} \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} strand\_status := Active * env \textbar{} Stabilized * env \textbar{} Dead * env \noindent{}strand\_env := strand\_status * id * comms \noindent{}env := variable $\rightarrow$ value \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((Stabalized,env),id,c),\Gamma)\Downarrow \Gamma}{}$ \\ \vspace{24pt} $\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} $\INFER{comm\_eval((s,env),stabalize,id,\Gamma)\Downarrow (Stablize,env,\Gamma)}{}$ \vspace{24pt} $\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)}{expr\_eval(e,env) \Downarrow v}$ \vspace{24pt} $\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}