User Tools

Site Tools


sem_op_imp_proc

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sem_op_imp_proc [2015/10/08 15:20] (current)
Line 1: Line 1:
 +<note warning>​This page is a draft</​note>​
 +
 +====== Functions in imperative languages ======
 +
 +We add functions to the language IMP defined [[sem_op_imp|here]].
 +  * A function is composed by a local declaration,​ a command, and an expression that represents the value to be returned to the caller.
 +  * Declarations have a [[wp>​Scope_(programming)#​Static_scoping|static scope]].
 +  * A single parameter can be passed to a function, either in a [[wp>​Evaluation_strategy#​Call_by_value|call-by-value]] or in a [[wp>​Evaluation_strategy#​Call_by_name|call-by-name]] fashion.
 +  * Functions do //not// modify the value of global variables.
 +  * In this version of the semantics, I do not require that functions can be passed as parameters, or returned by other functions.
 +
 +\\
 +===== Syntactic domains =====
 +
 +The syntax of declarations is extended as follows:
 +<code ocaml>
 +type dec = ...
 +  | Fun of ide * ide * mode * dec * com * exp
 +</​code>​
 +
 +The first item is the function identifier. ​
 +The second item is the parameter identifier, and ''​mode''​ is the parameter passing style.
 +The last three items are the local declaration,​ the command, and the expression for the return value.
 +
 +<code ocaml>
 +type mode = Value | Name
 +</​code>​
 +
 +For instance, this is a fuction (named ''​succ''​) to compute the successor of the integer parameter ''​x'':​
 +<code ocaml>
 +Fun(Ide "​succ",​ Ide "​x",​ Value, Empty, Skip, Add(Val(Ide "​x"​),​ N 1));;
 +</​code>​
 +
 +The syntax of expressions is extended as follows:
 +<code ocaml>
 +type exp = ...
 +  | Apply of ide * exp
 +</​code>​
 +
 +For instance, this expression applies the function ''​succ''​ to the integer 3:
 +<code ocaml>
 +Apply(Ide "​succ",​ N 3);;
 +</​code>​
 +
 +The syntax of commands is unchanged, as well as that of programs.
 +
 +\\
 +===== Semantic domains =====
 +
 +The semantic domain of denotable values is extended with two constructors.
 +''​DFun''​ is for denoting a function, while ''​DName''​ is for denoting a //​closure// ​
 +used to evaluate a parameter passed by name (more details below).
 +To implement static scoping, the value denoted by a function includes the environment where the function is  defined (last item in ''​DFun''​).
 +
 +<code ocaml>
 +type dval = ...
 +  | DFun of ide * mode * dec * com * exp * env
 +  | DName of exp * env
 +</​code>​
 +
 +<note tip>
 +To save time and focus on the core aspects of this lecture, you can copy&​paste [[sem_op_imp_proc_hint|this code]].
 +It contains the basic definitions of the syntactic and semantic domains, and the specification of environment and memory.
 +</​note>​
 +
 +\\
 +
 +===== Operational semantics =====
 +
 +The operational semantics of expressions and declarations is extended to deal with the 
 +expression ''​Apply(f,​e)''​ and the declaration ''​Fun(f,​x,​m,​d,​c,​e)''​. ​
 +Moreover, the case ''​Val(x)''​ has to be revised to deal with closures (see below).
 +
 +  * The semantics of a function declaration ''​Fun(f,​x,​m,​d,​c,​e)''​ in the environment ''​r''​ extends ''​r''​ with a binding for ''​f''​. The denoted value associated to ''​f''​ is a closure ''​DFun(x,​m,​d,​c,​e,​r)''​. The value of the parameter passing style ''​m''​ is immaterial.
 +  * The semantics of the expression ''​Apply(f,​a)''​ depends on the parameter passing style ''​m''​.
 +    * if ''​m = Value'',​ then the semantics of ''​a''​ is computed in the current environment,​ and its value is bound to the formal parameter ''​x''​ in the static environment. Then, the local declaration ''​d'',​ the command ''​c''​ and the expression ''​e''​ are evaluated in sequence, starting from the extended static environment.
 +    * if ''​m = Name'',​ then ''​a''​ is not yet evaluated. Instead, the formal parameter ''​x''​ is bound to the closure ''​DName(a,​r)'',​ where ''​r''​ is static environment. Then, evaluation proceeds as in the previous case.
 +  In both cases, to allow for recursive functions we have to bind the function identifier ''​f''​ to its closure ​ ''​DFun(x,​m,​d,​c,​e,​r)''​ before evaluating the command ''​c''​.
 +  * The semantics of the expression ''​Val(x)''​ has to consider the case when ''​x''​ is bound to a closure ''​DName(a,​r)''​. This requires evaluating ''​a''​ in the enviroment ''​r''​.
 +
 +The semantics of commands is unchanged.
 +
 +<code ocaml>
 +exception TypeMismatch;;​
 +exception AssignNonVariable of ide;;
 +
 +let rec intval e (r,s) = match (sem_exp e (r,s)) with 
 +  Int n -> n
 +| _ -> raise TypeMismatch
 +
 +and boolval e (r,s) = match sem_exp e (r,s) with 
 +  Bool b -> b
 +| _ -> raise TypeMismatch
 +
 +and sem_exp e (r, s) = match e with
 +  N n -> Int n
 +| Val x ->  (match applyenv r x with
 +    DVar l -> applystore s l
 +  | DConst c -> c
 +  | DName (e',​r'​) -> sem_exp e' (r',s)
 +  | _ -> raise (UnboundIde x))
 +| Add (e1,e2) ->  Int (intval e1 (r,s) + intval e2 (r,s))
 +| Sub (e1,e2) ->  Int (intval e1 (r,s) - intval e2 (r,s))
 +| Mul (e1,e2) ->  Int (intval e1 (r,s) * intval e2 (r,s))
 +| Div (e1,e2) ->  Int (intval e1 (r,s) / intval e2 (r,s))
 +| True -> Bool true
 +| False -> Bool false
 +| Eq (e1,e2) -> Bool (intval e1 (r,s) = intval e2 (r,s))
 +| Leq (e1,e2) -> Bool (intval e1 (r,s) <= intval e2 (r,s))
 +| Not e' -> Bool (not (boolval e' (r,s)))
 +| And (e1,e2) -> Bool (boolval e1 (r,s) && boolval e2 (r,​s)) ​
 +| Or (e1,e2) -> Bool (boolval e1 (r,s) || boolval e2 (r,​s)) ​
 +| Apply (f,a) -> (match applyenv r f with
 +    DFun (x,​m,​d,​c,​e',​r'​) -> 
 +      let r1 = bind r' f (DFun(x,​m,​d,​c,​e',​r'​)) in
 +      let r2 = (match m with
 + Value -> bind r1 x (DConst (sem_exp a (r,s)))
 +      | Name ->  bind r1 x (DName (a,r1))) in 
 +      let (r3,s3) = sem_dec d (r2,s) in 
 +      let s4 = sem_com c (r3,s3) in
 +      sem_exp e' (r3,s4))
 +
 +and sem_dec d (r,s) = match d with
 +  Empty -> (r,s)
 +| Const(x,e) -> (bind r x (DConst (sem_exp e (r,s))),s)
 +| Var x -> let l = newloc() in (bind r x (DVar l), s)
 +| Fun(f,​x,​m,​d',​c,​e) -> (bind r f (DFun(x,​m,​d',​c,​e,​r)),​ s)
 +| Dseq(d1,d2) -> sem_dec d2 (sem_dec d1 (r,s))
 +
 +and sem_com c (r,s) = match c with
 +    Skip -> s
 +  | Assign(x,e) -> (match applyenv r x with
 +      DVar l -> update s l (Mem (sem_exp e (r,s)))
 +    | _ -> raise (AssignNonVariable x))
 +  | Cseq(c1,c2) -> sem_com c2 (r,sem_com c1 (r,s))
 +  | If(b,c1,c2) -> if boolval b (r,s) then sem_com c1 (r,s) else sem_com c2 (r,s)
 +  | While(b,​c'​) -> if boolval b (r,s) then sem_com c (r,sem_com c' (r,s)) else s
 +
 +and sem_prog (Program (d,c)) =
 +    sem_com c (sem_dec d (emptyenv(),​emptystore()))
 +;;
 +</​code>​
 +
 +\\
 +===== Examples =====
 +
 +<note important>​
 +To facilitate copy&​paste,​ I have reversed the use of the symbol ''#''​.
 +From now on, it will always be used to represent output of the ocaml environment,​ instead that user input. ​
 +</​note>​
 +
 +First, an example to show recursion:
 +<code ocaml>
 +let factfun = Fun(Ide "​fact",​ Ide "​x",​ Value, Var (Ide "​res"​),​
 +    ​If(Leq (Val (Ide "​x"​),​ N 0),
 +       Assign (Ide "​res",​ N 1),
 +       Assign (Ide "​res",​ Mul(Val (Ide "​x"​),​ Apply(Ide "​fact",​ Sub(Val (Ide "​x"​),​N 1))))),
 +    Val (Ide "​res"​));; ​
 +
 +let fact x = Program(Dseq(factfun,​ Var (Ide "​f"​)), ​
 +      ​Assign(Ide "​f",​ Apply (Ide "​fact",​ N x)));;
 +
 +inspect ["​f"​] (debug_prog (fact 5));;
 +
 +# - : (string * eval) list = [("​f",​ Int 120)]
 +</​code>​
 +
 +The following example shows that the application of a function does not modify global variables.
 +If not, the final value of the variable ''​z''​ would have been ''​2''​ instead of ''​1''​.
 +<code ocaml>
 +let f0 = Fun(Ide "​f0",​ Ide "​x",​ Value, Empty, Assign(Ide "​z",​ N 2), N 10);;
 +
 +let sideeffect = Program(Dseq(Var (Ide "​z"​),​ Dseq(f0, Var (Ide "​res"​))),​
 + Cseq(Assign(Ide "​z",​ N 1),
 +       Assign(Ide "​res",​ Apply(Ide "​f0",​ N 11))));;
 +
 +inspect ["​z"​] (debug_prog sideeffect);;​
 +# - : (string * eval) list = [("​z",​ Int 1)]
 +</​code>​
 +
 +The following example illustrates static scoping. If we had implemented //dynamic// scoping, the result would have been 12 instead of 11.
 +
 +<code ocaml>
 +let f1 = Fun(Ide "​f1",​ Ide "​x",​ Value, Empty, Skip, Add(Val(Ide "​x"​),​Val(Ide "​z"​)));;​
 +let f2 = Fun(Ide "​f2",​ Ide "​y",​ Value, Const (Ide "​z",​ N 2), Skip, Apply(Ide "​f1",​ Val(Ide "​y"​)));;​
 +
 +let scoping = Program(Dseq(Const (Ide "​z",​ N 1),​Dseq(f1,​Dseq(f2,​Var (Ide "​res"​)))),​
 +       Assign(Ide "​res",​ Apply(Ide "​f2",​ N 10)));;
 +
 +inspect ["​res"​] (debug_prog scoping);;
 +# - : (string * eval) list = [("​res",​ Int 11)]
 +</​code>​
 +
 +<code ocaml>
 +
 +
 +let f m k = Fun(Ide "​f",​ Ide "​x",​ m, 
 + Var (Ide "​res"​), ​
 + Cseq(Assign(Ide "​res",​ N k), 
 +      ​If(Leq(Val (Ide "​res"​),​ N 9),
 + Skip,
 + Assign(Ide "​res",​ Val (Ide "​x"​)))),​
 + Val (Ide "​res"​));;​
 +
 +let fmismatch = Fun(Ide "​fmismatch",​ Ide "​z",​ Value, Empty, Skip, Add(True, N 1));;
 +
 +let pmismatch m k = Program(
 +                     ​Dseq(fmismatch,​ Dseq(f m k, Var (Ide "​res"​))), ​
 +      ​Assign(Ide "​res",​ Apply (Ide "​f", ​
 +                            Apply(Ide "​fmismatch",​ N 1))));;
 +
 +inspect ["​res"​] (debug_prog (pmismatch Value 5));;
 +# Exception: TypeMismatch.
 +
 +inspect ["​res"​] (debug_prog (pmismatch Value 10));;
 +# Exception: TypeMismatch.
 +
 +inspect ["​res"​] (debug_prog (pmismatch Name 5));;
 +# - : (string * eval) list = [("​res",​ Int 5)]
 +
 +inspect ["​res"​] (debug_prog (pmismatch Name 10));;
 +# Exception: TypeMismatch.
 +</​code>​
 +
 +<code ocaml>
 +let bot = Fun(Ide "​bot",​ Ide "​y",​ Value, Empty, While(True,​Skip),​ N 51);;
 +
 +let pbot m k = Program(Dseq(bot,​ Dseq(f m k, Var (Ide "​res"​))), ​
 +      ​Assign(Ide "​res",​ Apply (Ide "​f",​ Apply(Ide "​bot",​ N 1))));;
 +
 +inspect ["​res"​] (debug_prog (pbot Name 5));;
 +
 +# (* non-termination *)
 +</​code>​
 +
 +\\
 +
 +===== Type-checking =====
 +
 +The type-checking algorithm defined [[typecheck|here]] is refined to deal with functions.
 +Roughly, one has to check that the type of the parameter and the type of the returned value are used consistently in a program.
 +
 +The types are extended as follows:
 +<code ocaml>
 +type etype = ...
 +  | TFunction of (etype * etype)
 +</​code>​
 +
 +The typed declarations are extended with functions. ​
 +Respect to the syntax of ''​dec''​ seen above, we have added the type for the parameter and the type for the return value.
 +
 +<code ocaml>
 +type tdec = ...
 +  | TFun of ide * ide * mode * etype * tdec * com * exp * etype
 +</​code>​
 +
 +The functions ''​idetypes'',​ ''​typecheck_exp''​ and ''​typecheck_tdec''​ have to be extended to deal with functions. ​
 +
 +Here are some examples.
 +
 +<code ocaml>
 +let tfactfun = TFun(Ide "​fact",​ Ide "​x",​ Value, TInt, TVar (Ide "​res",​ TInt),
 +    ​If(Leq (Val (Ide "​x"​),​ N 0),
 +       Assign (Ide "​res",​ N 1),
 +       Assign (Ide "​res",​ Mul(Val (Ide "​x"​),​ Apply(Ide "​fact",​ Sub(Val (Ide "​x"​),​N 1))))),
 +    Val (Ide "​res"​),​ TInt);; ​
 +
 +let tfact x = TProgram(TDseq(tfactfun,​ TVar (Ide "​f",​ TInt)), ​
 +      ​Assign(Ide "​f",​ Apply (Ide "​fact",​ N x)));;
 +
 +typecheck_prog (tfact 5);;
 +# - : bool = true
 +</​code>​
 +
 +The program ''​wrong1''​ below is not well-typed, because it applies the function ''​fact''​ to a boolean value.
 +<code ocaml>
 +let wrong1 = TProgram(TDseq(tfactfun,​ TVar (Ide "​f",​ TInt)), ​
 +      ​Assign(Ide "​f",​ Apply (Ide "​fact",​ True)));;
 +
 +typecheck_prog wrong1;;
 +# - : bool = false
 +</​code>​
 +
 +The program ''​wrong2''​ below is not well-typed, because it assigns an integer value (the result of invoking the ''​fact''​ function) to a variable ''​f''​ declared as boolean.
 +<code ocaml>
 +let wrong2 = TProgram(TDseq(tfactfun,​ TVar (Ide "​f",​ TBool)), ​
 +      ​Assign(Ide "​f",​ Apply (Ide "​fact",​ N 5)));;
 +
 +typecheck_prog wrong2;;
 +# - : bool = false
 +</​code>​
 +
  
sem_op_imp_proc.txt ยท Last modified: 2015/10/08 15:20 (external edit)