User Tools

Site Tools


sem_op_imp_proc

This page is a draft

Functions in imperative languages

We add functions to the language IMP defined 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 static scope.
  • A single parameter can be passed to a function, either in a call-by-value or in a 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:

type dec = ...
  | Fun of ide * ide * mode * dec * com * exp

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.

type mode = Value | Name

For instance, this is a fuction (named succ) to compute the successor of the integer parameter x:

Fun(Ide "succ", Ide "x", Value, Empty, Skip, Add(Val(Ide "x"), N 1));;

The syntax of expressions is extended as follows:

type exp = ...
  | Apply of ide * exp

For instance, this expression applies the function succ to the integer 3:

Apply(Ide "succ", N 3);;

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).

type dval = ...
  | DFun of ide * mode * dec * com * exp * env
  | DName of exp * env

To save time and focus on the core aspects of this lecture, you can copy&paste this code. It contains the basic definitions of the syntactic and semantic domains, and the specification of environment and memory.


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.

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()))
;;


Examples

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.

First, an example to show recursion:

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)]

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.

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)]

The following example illustrates static scoping. If we had implemented dynamic scoping, the result would have been 12 instead of 11.

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)]
 
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.
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 *)


Type-checking

The type-checking algorithm defined 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:

type etype = ...
  | TFunction of (etype * etype)

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.

type tdec = ...
  | TFun of ide * ide * mode * etype * tdec * com * exp * etype

The functions idetypes, typecheck_exp and typecheck_tdec have to be extended to deal with functions.

Here are some examples.

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

The program wrong1 below is not well-typed, because it applies the function fact to a boolean value.

let wrong1 = TProgram(TDseq(tfactfun, TVar (Ide "f", TInt)), 
		     Assign(Ide "f", Apply (Ide "fact", True)));;
 
typecheck_prog wrong1;;
# - : bool = false

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.

let wrong2 = TProgram(TDseq(tfactfun, TVar (Ide "f", TBool)), 
		     Assign(Ide "f", Apply (Ide "fact", N 5)));;
 
typecheck_prog wrong2;;
# - : bool = false
sem_op_imp_proc.txt · Last modified: 2015/10/08 15:20 (external edit)