Home My Page Projects Code Snippets Project Openings diderot

# SCM Repository

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

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

Tue Mar 22 21:23:04 2011 UTC (8 years, 2 months 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}