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

SCM Repository

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

Annotation of /trunk/doc/semantics/semantics.tex

Parent Directory Parent Directory | Revision Log Revision Log


Revision 665 - (view) (download) (as text)

1 : lamonts 665 \documentclass[11pt]{article}
2 :    
3 :     \usepackage{proof}
4 :     \usepackage{amsmath}
5 :     \usepackage{graphicx}
6 :     \usepackage{fullpage}
7 :     \usepackage{amsfonts}
8 :    
9 :     \newcommand{\point}{\textbullet~}
10 :     \newcommand{\INFER}[2]{\begin{array}{c}\infer{#1}{#2}\end{array}}
11 :    
12 :     \title{Diderot Formal Semantics}
13 :     \author {
14 :     John Reppy \\
15 :     University of Chicago \\
16 :     {\small\tt{}jhr@cs.uchicago.edu} \\
17 :     \and
18 :     Lamont Samuels \\
19 :     University of Chicago \\
20 :     {\small\tt{}lamonts@cs.uchicago.edu} \\
21 :     }
22 :     \date{\today}
23 :    
24 :     \begin{document}
25 :     \maketitle
26 :     \thispagestyle{empty}
27 :    
28 :    
29 :    
30 :     \section{Abstract Syntax}
31 :    
32 :     \noindent{}\point Definitions: variable := string \textbar{} id := integer
33 :     \vspace{12pt}
34 :    
35 :     \noindent{}\point Values: v := Num(n) \textbar{} Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...??
36 :    
37 :     \vspace{12pt}
38 :     \noindent{}\point Arithmetic expression (Aexp):
39 :     \begin{displaymath}
40 :     \begin{array}{rclr}
41 :     \text{e} & ::= & n &\text{for n} \in\mathbb{R} \\
42 :     & \mid & \text{x} &\text{for x = variable} \\
43 :     & \mid & \text{$e_1 $ + $ e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
44 :     & \mid & \text{$e_1 $ - $ e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
45 :     & \mid & \text{$e_1 $ * $ e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
46 :     & \mid & \text{$e_1 $ / $ e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
47 :     \end{array}
48 :     \end{displaymath}
49 :    
50 :     \noindent{}\point Relational expression (Rexp):
51 :     \begin{displaymath}
52 :     \begin{array}{rclr}
53 :     \text{r} & ::= &\text{true} \\
54 :     & \mid & \text{false} \\
55 :     & \mid & \text{$e_1 == e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
56 :     & \mid & \text{$e_1 < e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
57 :     & \mid & \text{$e_1 > e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
58 :     & \mid & \text{$e_1 \leq e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
59 :     & \mid & \text{$e_1 \geq e_2 $} &\text{for $e_1$, $e_2$} \in\text{Aexp} \\
60 :    
61 :    
62 :     \end{array}
63 :     \end{displaymath}
64 :    
65 :     \noindent{}\point Commands (Comms):
66 :     \begin{displaymath}
67 :     \begin{array}{rclr}
68 :     \text{c} & ::= &\text{x := e} & \text{for x = variable, e} \in\text{Aexp}\\
69 :     & \mid & \text{$c_1 $; $c_2 $} &\text{for $c_1$, $c_2$} \in\text{Comms} \\
70 :     & \mid & \text{$ if\:r\:then\:c_1\:else\:c_2 $} &\text{for $c_1$, $c_2$} \in\text{Aexp and b} \in\text{Rexp} \\
71 :     & \mid & \text{stabalize}
72 :     \end{array}
73 :     \end{displaymath}
74 :    
75 :    
76 :     \section{Strand Environment}
77 :     strand\_status := Active * env \textbar{} Stabilized * env \textbar{} Dead * env
78 :    
79 :     \noindent{}strand\_env := strand\_status * id * comms
80 :    
81 :     \noindent{}env := variable $ \rightarrow $ value
82 :    
83 :    
84 :     \section{Global Environment}
85 :     The $\cup $ character denotes a parallel construct that states that every stand environment
86 :     runs in parallel with each other.
87 :    
88 :     \begin{center}
89 :     $\displaystyle \bigcup_{\substack {id \in strand\_env \\
90 :     \Gamma = id \rightarrow strand\_env} }{update(\Gamma(id),\Gamma)} $
91 :     \end{center}
92 :     \vspace{12pt}
93 :     dom($\Gamma$) := all active \& stabilized strand environments
94 :    
95 :     \noindent{}newId := $\Gamma$ * id $\rightarrow$ id
96 :    
97 :    
98 :    
99 :     \section{Inference Rules}
100 :    
101 :     \noindent{}\point Update function: strand\_env * $ \Gamma \rightarrow \Gamma'$
102 :     \vspace{12pt}
103 :     \begin{center}
104 :     $ \INFER{update((Stabalized,env),id,c),\Gamma)\Downarrow \Gamma}{}$ \\
105 :     \vspace{24pt}
106 :     $ \INFER{update((Active,env),id,c),\Gamma)\Downarrow \Gamma'[(new\_status,env')/id]}
107 :     {comm\_eval((Active,env),c,id,\Gamma) \Downarrow (new\_status,env',\Gamma')}$
108 :    
109 :     \end{center}
110 :    
111 :     \vspace{12pt}
112 :     \noindent{}\point comm\_eval: strand\_status * commands * id * $ \Gamma \rightarrow $ strand\_status * env * $\Gamma' $
113 :     \vspace{12pt}
114 :     \begin{center}
115 :     $ \INFER{comm\_eval((s,env),stabalize,id,\Gamma)\Downarrow (Stablize,env,\Gamma)}{}$
116 :     \vspace{24pt}
117 :    
118 :     $ \INFER{comm\_eval((s,env),die,id,\Gamma)\Downarrow (Dead,env,\Gamma)}{}$
119 :     \vspace{24pt}
120 :    
121 :     $ \INFER{comm\_eval((s,env),x:=e,id,\Gamma)\Downarrow (s,env[x:=v],\Gamma)}{expr\_eval(e,env) \Downarrow v}$
122 :     \vspace{24pt}
123 :    
124 :     $ \INFER{comm\_eval((s,env),c_1; c_2,id,\Gamma)\Downarrow (s',env'',\Gamma'')}
125 :     {comm\_eval((s,env),c_1,\Gamma) \Downarrow (s',env',\Gamma') \hspace{.2in} comm\_eval((s',env),c_2,\Gamma') \Downarrow (s'',env'',\Gamma'')}$
126 :     \vspace{24pt}
127 :    
128 :     $ \INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,id,\Gamma)\Downarrow (s',env',\Gamma')}
129 :     {rel\_op(b,env) \Downarrow Bool(true) \hspace{.2in} comm\_eval((s,env),c_1,\Gamma) \Downarrow (s',env',\Gamma')}$
130 :     \vspace{24pt}
131 :    
132 :     $ \INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,\Gamma)\Downarrow (s',env',\Gamma')}
133 :     {rel\_op(b,env) \Downarrow Bool(false) \hspace{.2in} comm\_eval((s,env),c_2,\Gamma) \Downarrow (s',env',\Gamma')}$
134 :     \vspace{24pt}
135 :    
136 :    
137 :     $ \INFER{comm\_eval((s,env), spawn,id,\Gamma)\Downarrow (s,env,\Gamma[id'])}
138 :     {newId(\Gamma,id) \Downarrow id'}$
139 :    
140 :     \end{center}
141 :    
142 :     \vspace{12pt}
143 :     \noindent{}\point expr\_eval: Aexp * $ \Gamma \rightarrow $ v
144 :     \vspace{12pt}
145 :    
146 :     \noindent{}\point rel\_op: Rexp * $ \Gamma \rightarrow $ Bool(b)
147 :     \vspace{12pt}
148 :    
149 :    
150 :     \end{document}

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