Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

[diderot] View of /trunk/doc/semantics/semantics.tex
ViewVC logotype

View of /trunk/doc/semantics/semantics.tex

Parent Directory Parent Directory | Revision Log Revision Log


Revision 665 - (download) (as text) (annotate)
Tue Mar 22 21:23:04 2011 UTC (8 years ago) by lamonts
File size: 5038 byte(s)
Removing old semantics directory and adding doc/semantics and latex components
\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} 

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0