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

SCM Repository

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

Diff of /trunk/doc/semantics/semantics.tex

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 714, Thu Mar 31 13:33:50 2011 UTC revision 715, Thu Mar 31 14:58:53 2011 UTC
# Line 29  Line 29 
29  \section{Abstract Syntax}  \section{Abstract Syntax}
30    
31  \noindent{}\point Definitions:  variable := string \textbar{} id := integer  \noindent{}\point Definitions:  variable := string \textbar{} id := integer
  \vspace{12pt}  
32    
33  \noindent{}\point Values:  v := Num(n)  \textbar{}  Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...??  \noindent{}\point Values:  v := Num(n)  \textbar{}  Bool(b) \textbar{} String(s) \textbar{} tensor...?? \textbar{} vecs...??
34    
# Line 45  Line 44 
44    
45    
46  \section{Strand Environment}  \section{Strand Environment}
47  strand\_status  := Active * env \textbar{} Stabilized * env \textbar{} Dead * env  \begin{displaymath}
48                    \begin{array}{l}
49  \noindent{}strand\_env := strand\_status * id * comms                  \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    
 \noindent{}env := variable  $ \rightarrow $ value  
55    
56    
57  \section{Global Environment}  \section{Global Environment}
# Line 71  Line 73 
73    
74  \noindent{}\point Update function: strand\_env * $ \Gamma \rightarrow \Gamma'$  \noindent{}\point Update function: strand\_env * $ \Gamma \rightarrow \Gamma'$
75  \vspace{12pt}  \vspace{12pt}
76  \begin{center}  %\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')}$  
77    
 \end{center}  
78    
79    %$ \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  \vspace{12pt}  \vspace{12pt}
87  \noindent{}\point comm\_eval: strand\_status * commands * id * $ \Gamma \rightarrow $  strand\_status * env * $\Gamma' $  
 \vspace{12pt}  
88  \begin{center}  \begin{center}
89  $ \INFER{comm\_eval((s,env),stabalize,id,\Gamma)\Downarrow (Stablize,env,\Gamma)}{}$  \CommEval{stabalize}{(Stablize,env,\Gamma)}{}
 \vspace{24pt}  
90    
91  $ \INFER{comm\_eval((s,env),die,id,\Gamma)\Downarrow (Dead,env,\Gamma)}{}$  %$ \INFER{comm\_eval((s,env),stabalize,id,\Gamma)\Downarrow (Stablize,env,\Gamma)}{}$
92  \vspace{24pt}  %\vspace{24pt}
93    
94    \CommEval{die}{(Dead,env,\Gamma)}{}
95    
96    %$ \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}} $   %$\INFER{comm\_eval((s,env),x:=e,id,\Gamma)\Downarrow (s,env[x:=v],\Gamma)}{\ExpEval{env}{e}{v}} $
99  \vspace{24pt}  %\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'')}  %$ \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'')}$          %      {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}  %\vspace{24pt}
106    
107  $ \INFER{comm\_eval((s,env), if\:r\:then\:c_1\:else\:c_2,id,\Gamma)\Downarrow (s',env',\Gamma')}  $ \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')}$                {rel\_op(b,env)  \Downarrow Bool(true)  \hspace{.2in} comm\_eval((s,env),c_1,\Gamma) \Downarrow (s',env',\Gamma')}$

Legend:
Removed from v.714  
changed lines
  Added in v.715

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