(* A demonstartion of how to express mathematical semantics in SML as directly as possible. (1) Forget about parsing, if at all possible, or delay it Think of this as providing "Syntactic Sugar" for the user. (2) Define Abstract syntax as an ML datatype (3) Define compositional semantics using ML functions Example. The Abstract Syntax of While We will fake Num! *) datatype Aexp= Num of int | Sum of Aexp * Aexp | Diff of Aexp * Aexp | Prod of Aexp * Aexp | Var of string; datatype Bval= True | False ; datatype Bexp= V of Bval | And of Bexp * Bexp | Not of Bexp | Eq of Aexp * Aexp | Lt of Aexp * Aexp; (* for Store = Var->Val.... see mapping.sml *) (* fun A:Aexp*Store->Val...*) (* fun B:Bexp*Store->bool *) (* Hiroki I. spotted the omission of Store from these... An alternative is to hide a sto:Store in a data type... *) datatype Stm= Skip | Ass of string * Aexp | Comp of Stm * Stm | If of Bexp * Stm * Stm | While of Bexp * Stm; (* fun S_NS: Stm * Store -> Store OR S_SOS:Stm*Store->Store because we know that S_NS and S_SOS are deterministic on While we know that we have semantic function which can therefore be programmed as an SML function. Note. However, if we had non-deterministic semantics then we would have the problem of coding either ->s' or -> and these would be code (in SML) as fun S_NS: Stm*Store*Store->bool OR S_SOS:Stm*Store*Stm*Store->bool *) Sum( Num(1), Num 2 ); While( V True, Skip); Ass( "x", Num 1); If( Not( Lt ( Var "x", Var "y")), Ass("z", Var "x"), Ass("z", Var "y")); Comp(Comp( Ass ("z", Var "x"), Ass("x", Var "y")), Ass("y", Var "z"));