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

variable ::= string 
id ::= integer 

Arithmetic expression (Aexp)
e ::=  n       for n ∈ R 
     | 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 * env | Dead * env | Stablized * env 
env = variable → value

/** Global Environment Functions **/
Strand_Env = Strand_Status * id * commands * env 
Γ = id -> Strand_Env  dom(Γ) = all Active & Stablized Strand Environments  
newId = Γ * id -> id 

/** Arithmetic & Relational Expressions Evaluation Functions**/
expr_value = Aexpr * env -> value 
rel_op = Rexpr * env -> value 


comm_eval: Strand_Status * commands  -> status * env 

Rules 
(1)  ------------------------------------------------------
    	comm_eval((s, env),stabalize) ⇓ (Stablized, env) 


(2)  ------------------------------------------------------
    	comm_eval((s, env),die) ⇓ (Dead, env) 
 

                    expr_eval(e,env) ⇓ v 
(3) ----------------------------------------------------------
        comm_eval((s,env),x:=e) ⇓ (s,env[x:=v]) 


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


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


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



update: Strand_Env -> Strand_Env 
Rules

(1) -------------------------------------------------------------
     update(((Stabalized,env),id,comm>)) ⇓ ((Stabalized,env),id,comm) 


       		comm_eval((Active,env),comm) ⇓ (new_status,env')     
(2)  -------------------------------------------------------------
        Update(((Active,env),_,comm>)) ⇓ ((new_status,env'),id,comm)