Diderot Formal Semantics 
===============================

variable ::= string 
id ::= integer 

Arithmetic expression (Aexp)
e ::=  n       for n ∈ R or n ∈ Z 
     | x       for x = variable 
     | e1 + e2 for e1,e2 ∈ Aexp, Aexp 
     | e1 - e2 for e1,e2 ∈ Aexp, Aexp 
     | e1 * e2 for e1,e2 ∈ Aexp, Aexp 
     | e1 / e2 for e1,e2 ∈ Aexp, Aexp 

Relational expression (Rexp) 
b ::=   true 
	  | false
     | e1 == e2 for e1,e2 ∈ Aexp, Aexp 
     | e1 < e2  for e1,e2 ∈ Aexp, Aexp 
     | e1 > e2  for e1,e2 ∈ Aexp, Aexp 
     | e1 <= e2 for e1,e2 ∈ Aexp, Aexp 
     | e1 >= e2 for e1,e2 ∈ Aexp, Aexp 
     
Commands (Comm)
c ::=   x := e  			 for x = variable, e ∈ Aexp 
	  | c1; c2				 for c1,c2  ∈ Comm
	  | if b then c1 else c2 for c1,c2  ∈ Comm and b  ∈ Rexp
	  | stabalize  


Values 
v := Num(n) | Bool(b) | String(s) | tensor...?? 


Strand_Status := Active | Dead | Stablized 

env = variable → value
Σ = id -> Strand_Env
Strand_Env = Strand_Status * id * commands * env 
expr_value = Aexpr * env -> value 
rel_op = Rexpr * env -> value 


comm_eval: status * commands * env -> status * env 
Rules 

(1)  ------------------------------------------------------
    	comm_eval(status,Stablized,env) ⇓ (Stablized,env) 
 
                    expr_eval(e,env) ⇓ v 
(2) ----------------------------------------------------------
        comm_eval(status,x:=e,env) ⇓ (status,env[x:=v]) 

          comm_eval(s,c1,env) ⇓ (s',env')   comm_eval(s',c2,env') ⇓ (s'',env'')  
(3) -------------------------------------------------------------------------
                   comm_eval(s,c1;c2,env) ⇓ (s'',env'') 


          rel_op(b,env) ⇓ true   comm_eval(s,c1,env) ⇓ (s',env')  
(4) -------------------------------------------------------------------------
                   comm_eval(s,if b then c1 else c2,env) ⇓ (s',env') 

          rel_op(b,env) ⇓ false   comm_eval(s,c2,env) ⇓ (s',env')  
(5) -------------------------------------------------------------------------
                   comm_eval(s,if b then c1 else c2,env) ⇓ (s',env') 

update: Strand_Env -> Strand_Env 
Rules
(1) -------------------------------------------------------------
     update(<Stabalized,id,comm,env>) ⇓ <Stabalized,id,comm,env> 


(2)     (Doubt this will ever happen...?) 
    -------------------------------------------------------------
           Update(<Dead,id,comm,env>) ⇓ <Dead,id,comm,env> 

       				 comm_eval(Comm,env) ⇓ <new_status,env'>     
(3)  -------------------------------------------------------------
        Update(<Active,_,x:=e,env>) ⇓ <new_status,id,comm,env'>