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 715 - (view) (download) (as text)

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

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