In this lesson we will develop the operational semantics of a quite simple functional language. The language has integer of boolean expression, the possibility of building complex expressions with operators like Sum, Or, has an if then else, and variables (with the usual functional memaning). We will add later what is now left to make the language Turing powerful.

We start recalling that a functional language returns expressible values, hence we have to introduce a type for the result of the evaluation of an expression written in the functional language:

type eval = None 
          | Int of int 
          | Bool of bool

The syntax of the language is the following:

type exp = 
    	Eint of int 
      | Ebool of bool 
      | Den of ide
      | Prod of exp * exp
      | Sum of exp * exp
      | Diff of exp * exp
      | Eq of exp * exp
      | Minus of exp
      | Iszero of exp
      | Or of exp * exp
      | And of exp * exp
      | Not of exp
      | Ifthenelse of exp * exp * exp

where the type ide is the one for variables:

type ide = string

Recall the implementation of an environment introduced in the last lesson of the crash course, we adapt it to our purpose.

Suppose we want to define a partial function f with domain 'b and codomain 'a. Then, we can model f as a total function from 'b to the “lifted” codomain 'a partial (lifted means that we add an element to explicitly say that the function on an argument is not defined).

We do not have to introduce a new “lifted” (co)domain, as we have already it: eval is a lifted domain (the elements are integers and boolean, with the proper constructor, and the value None represents no result).

The following function, given a predicate p: 'a → bool, a function f : 'a → eval and a list, finds the first element of the list (if any) that satisfies the predicate.

# let rec find p f = function
    [] -> None
  | x::l -> if p x then f x else find p f l;;
 
val find : ('a -> bool) -> ('a -> eval) -> 'a list -> eval = <fun>

This function can be used to implement an environment, i.e. a partial mapping from identifiers to values, as a list of pairs (id,value).

First, we define a function bind, that binds an identifier x to a value v in the given environment.

# let rec bind x v = function
    [] -> [(x,v)]
  | (y,v')::l when x=y -> (x,v)::l
  | (y,v')::l -> (y,v')::(bind x v l);;
 
val bind : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list = <fun>

Then, we define the function applyenv, that searches the environment for the value bound to the identifier x. We model it as a partial function that produces None if x is not bound in the environment, or v if x is bound to v.

# let applyenv env x = (find (fun (y,v) -> x=y) (fun (y,v) -> v)) env;;
 
val applyenv : ('a * eval) list -> 'a -> eval = <fun>

Here are some examples:

# let rho0 = [("x",Int 3);("y",Int 5)];;
val rho0 : (string * eval) list = [("x", Int 3); ("y", Int 5)]
 
# applyenv rho0 "z";;
- : eval = None
 
# applyenv rho0 "x";;
- : eval = Int 3

The behaviour of the function bind does not change:

# let rho1 = bind "x" (Int 7) rho0;;
val rho1 : (string * eval) list = [("x", Int 7); ("y", Int 5)]
 
# applyenv rho1 "x";;
- : eval = Int 7
 
# let rho2 = bind "z" (Int 9) rho1;;
val rho2 : (string * eval) list = [("x", Int 7); ("y", Int 5); ("z", Int 9)]
 
# applyenv rho2 "z";;
- : eval = Int 9

We have now almost all the ingredients to write the interpreter for exp, namely a function sem : exp → env → eval, where

# type env = (ide*eval) list;;

The run time support is the collections of data and functions that allow the execution of the code written in the programming language (and in our case interpreted). Thus the environment, implemented as we have suggested, is a part of the run time support (we will point out later that there are alternative implementations of the environment).

Recall that an expression returns an eval (integer and boolean of our language) whereas the machine code of our abstract machine (Ocaml) gives int and bool. We have to implement part of the rts to cope with the values of our language.

For instance, if we want to sum two integers (Int 3 and Int 4) we have to sum 3 and 4 to obtain Int 7. Clearly we can sum numbers, so we have to be sure that the two eval we have to combine represent integers:

Let us start to implement a type-checker (we can do at top level, but in this way it can be more readable):

let typecheck (x, y) = match x with
      | "int" ->
	  (match y with 
	  |  Int(u) -> true
	  | _ -> false)
      | "bool" ->
	  (match y with 
	  |  Bool(u) -> true
	  | _ -> false)
      | _ -> failwith ("not a valid type")

We can use this to implement operations at machine level:

let plus (x,y) = if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u+w))
      else failwith ("type error")

A solution to the exercise:

(* Operations on Eval *)
 
   let typecheck (x, y) =
      match x with
      | "int" ->
	  (match y with 
	  |  Int(u) -> true
	  | _ -> false)
      | "bool" ->
	  (match y with 
	  |  Bool(u) -> true
	  | _ -> false)
      | _ -> failwith ("not a valid type")
 
    let minus x =
      if typecheck("int",x) 
      then 
    	(match x with
    	| Int(y) -> Int(-y) )
      else 
    	failwith ("type error")
 
    let iszero x =
      if typecheck("int",x) 
      then 
     	(match x with
     	| Int(y) -> Bool(y=0) )
      else 
     	failwith ("type error")
 
    let equ (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Bool(u = w))
      else failwith ("type error")
 
    let plus (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u+w))
      else failwith ("type error")
 
    let diff (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u-w))
      else failwith ("type error")
 
    let mult (x,y) =
      if typecheck("int",x) & typecheck("int",y) 
      then 
   	(match (x,y) with
   	| (Int(u), Int(w)) -> Int(u*w))
      else failwith ("type error")
 
    let et (x,y) =
      if typecheck("bool",x) & typecheck("bool",y) 
      then 
   	(match (x,y) with
   	| (Bool(u), Bool(w)) -> Bool(u & w))
      else failwith ("type error")
 
    let vel (x,y) =
      if typecheck("bool",x) & typecheck("bool",y) 
      then 
   	(match (x,y) with
   	| (Bool(u), Bool(w)) -> Bool(u or w))
      else failwith ("type error")
 
    let non x =
      if typecheck("bool",x) 
      then 
     	(match x with
     	| Bool(y) -> Bool(not y) )
      else failwith ("type error");;

As we said, our target is to write an interpreter for exp.

Complete the following:

let rec sem (e:exp) (r:env) = match e with
      | Eint(n) -> Int(n)
      | Ebool(b) -> Bool(b)
      | ...

The solution of the exercise, as we have seen in class, can be the following:

(*SEMANTIC EVALUATION FUNCTIONS  *)
let rec sem (e:exp) (r:env) =
      match e with
      | Eint(n) -> Int(n)
      | Ebool(b) -> Bool(b)
      | Den(i) -> (applyenv r i)
      | Iszero(a) -> iszero((sem a r) )
      | Eq(a,b) -> equ((sem a r) ,(sem b r) )
      | Prod(a,b) ->  mult ( (sem a r), (sem b r))
      | Sum(a,b) ->  plus ( (sem a r), (sem b r))
      | Diff(a,b)  ->  diff ( (sem a r), (sem b r))
      | Minus(a) ->  minus( (sem a r))
      | And(a,b) ->  et ( (sem a r), (sem b r))
      | Or(a,b) ->  vel ( (sem a r), (sem b r))
      | Not(a) -> non( (sem a r))
      | Ifthenelse(a,b,c) -> 
            let g = sem a r in
            if typecheck("bool",g) then
               (if g = Bool(true) 
               then sem b r
               else sem c r)
            else failwith ("nonboolean guard") 

Just one comment: any other different but correct implemetation would do.

Once you have completed the interpreter (and it runs), add to the language the local declarations. The complete syntax of the language is now

type ide = string 
type exp = Eint of int 
      | Ebool of bool 
      | Den of ide 
      | Prod of exp * exp 
      | Sum of exp * exp 
      | Diff of exp * exp 
      | Eq of exp * exp 
      | Minus of exp 
      | Iszero of exp 
      | Or of exp * exp 
      | And of exp * exp 
      | Not of exp 
      | Ifthenelse of exp * exp * exp 
      | Let of ide * exp * exp

The Let(“x”,e1,e2) construct binds to the identifier “x” the evaluation of the expression e1 and the identifier may appear in the expression e2.

Solution of the exercise: just add to the interpreter the following line: Let(x,a,b) → sem b (bind x (sem a r) r)

The language supports integer and boolean. First let us identify what you have to change in order to add characters to the language, and second let us modify accordingly what has to be modified.

First of all, as we have added a new data type, we have to decide whether or not this type would be a value that the evaluation of an expression can give as result, and it is trivial to decide positively. The consequence is that we have to add this to out eval:

type eval = None 
          | Int of int 
          | Bool of bool
          | Char of char

Once we have done this, we can introduce the syntax of the language (on characters we can define an equality and an operation that converts a charcter in an integer (its coding). We may use the ocaml function int_of_char : char → int:

type ide = string 
type exp = Eint of int 
      | Ebool of bool 
      | Echar of char
      | Den of ide 
      | Prod of exp * exp 
      | Sum of exp * exp 
      | Diff of exp * exp 
      | Eq of exp * exp 
      | Eqchar of exp * exp
      | Minus of exp 
      | Iszero of exp 
      | Or of exp * exp 
      | And of exp * exp 
      | Not of exp 
      | Casttoint of exp
      | Ifthenelse of exp * exp * exp 
      | Let of ide * exp * exp

where we have added the possibility of having constants of the type char, and equality on character and the required cast operator.

We then modify the function checking whether the evaluated expression is of the proper type:

   let typecheck (x, y) =
      match x with
      | "int" ->
	  (match y with 
	  |  Int(u) -> true
	  | _ -> false)
      | "bool" ->
	  (match y with 
	  |  Bool(u) -> true
	  | _ -> false)
      | "char" -> 
          (match y with
          | Char(u) -> true
          | _ -> false)
      | _ -> failwith ("not a valid type")

and the implementation of the Eqchar and Casttoint:

let equchar(x,y) = if typecheck("char",x) & typecheck("char",y) 
      then 
   	(match (x,y) with
   	| (Char(u), Char(w)) -> Bool(u = w))
      else failwith ("type error") 
 
let casttoint(x) = if typecheck("char",x)
      then 
   	(match c with
   	| Char(u) -> Int(int_of_char u))
      else failwith ("type error") 

Now the modification of the interpreter is trivial, as we have to add just some lines:

let rec sem (e:exp) (r:env) =
      match e with
      | Eint(n) -> Int(n)
      | Ebool(b) -> Bool(b)
      | Echar(c) -> Char c
      | Den(i) -> applyenv(r,i)
      | Iszero(a) -> iszero((sem a r) )
      | Eq(a,b) -> equ((sem a r) ,(sem b r) )
      | Eqchar(a,b) -> equchar((sem a r) ,(sem b r) )
      | Prod(a,b) ->  mult ( (sem a r), (sem b r))
      | Sum(a,b) ->  plus ( (sem a r), (sem b r))
      | Diff(a,b)  ->  diff ( (sem a r), (sem b r))
      | Minus(a) ->  minus( (sem a r))
      | And(a,b) ->  et ( (sem a r), (sem b r))
      | Or(a,b) ->  vel ( (sem a r), (sem b r))
      | Not(a) -> non( (sem a r))
      | Casttoint(a) -> casttoint (sem a r)
      | Ifthenelse(a,b,c) -> 
            let g = sem a r in
            if typecheck("bool",g) then
               (if g = Bool(true) 
               then sem b r
               else sem c r)
            else failwith ("nonboolean guard")
      | Let(x,a,b) -> sem b (bind x (sem a r) r)

Ocaml allows to define function, so why bother with lists? Here is an alternative implementation. It has the operation emptyenv that create the partial function always undefined.

# type 't env = ide -> 't;;
 
# let emptyenv x = function (y:ide) -> x;;
val emptyenv : 'a -> 'b -> 'a = <fun>
 
# let applyenv x y = x y;;
val applyenv : ('a -> 'b) -> 'a -> 'b = <fun>
 
# let bind l e r = 
      function lu -> if lu = l then e else applyenv r lu;;
val bind :  'a -> 'b -> ('a -> 'b) -> 'a -> 'b = <fun>

and we can write

# let rho0 = emptyenv None;;
val rho0 : '_a -> eval = <fun>
 
# let rho1 = bind "x" (Int 3) rho0;;
val rho1 : string -> eval = <fun>
 
# applyenv rho1 "z";;
- : eval = None
 
# applyenv rho1 "x";;
- : eval = Int 3

Both implementations can be used, provided we force the type of variables in ocaml:

# type env = ide -> eval;;
 
# let emptyenv (x:eval) = function (y:ide) -> x;;
val emptyenv : eval -> ide -> eval = <fun>
 
# let applyenv (x:env) (y:ide) = x y;;
val applyenv : env -> ide -> eval = <fun>
 
# let bind (l:ide) (e:eval) (r:env) = 
      ((function lu -> if lu = l then e else applyenv r lu):env);;
val bind :  ide -> eval -> env -> env = <fun>

We want extend the language with functions: like in Ocaml we add functions and the recursive functions. Clearly functions should be used and can be the result of an evaluation of an expression, hence functions should belong to the type eval. Here is possibility:

type eval =	None   
     | Int of int 
     | Bool of bool
     | Funval of efun   
and efun = exp * eval env

A function has a name (which will be put in the environment) and, as we are dealing with statically scoped language, it is a closure, i.e., a pair exp and eval env, which is the environment in which the function has to be evaluated.

A function receive a list of arguments that should match the formal parameter in the definition of the function. Here is the implementation a new operation on the environment that can ease the actual write of the interpreter:

#   exception WrongBindlist;;
exception WrongBindlist
 
# let rec bindlist (r,il,el) = match (il,el) with
        | ([],[]) -> r
    	| i::il1, e::el1 -> bindlist ((bind  i e r), il1, el1)
	| _ -> raise WrongBindlist;;
val bindlist : ('a -> 'b) * 'a list * 'b list -> 'a -> 'b = <fun>

The syntax of the language is

type exp = Eint of int 
      | Ebool of bool 
      | Den of ide
      | Prod of exp * exp
      | Sum of exp * exp
      | Diff of exp * exp
      | Mod of exp * exp
      | Div of exp * exp
      | Less of exp * exp
      | Eq of exp * exp
      | Minus of exp
      | Iszero of exp
      | Or of exp * exp
      | And of exp * exp
      | Not of exp
      | Ifthenelse of exp * exp * exp
      | Let of ide * exp * exp      
      | Fun of ide list * exp
      | Appl of exp * exp list

the function bindlist receives two lists: one of identifiers anda the other of eval values, and it inserts all of them in the environment. In case they do not match in length, an exception is raised.

Solution of the exercise, as we have seen it during the lecture.

let rec sem (e:exp) (r:eval env) =
      match e with
      | Eint(n) -> Int(n)
      | Ebool(b) -> Bool(b)
      | Den(i) -> applyenv r i 
      | Iszero(a) -> iszero((sem a r) )
      | Eq(a,b) -> equ((sem a r) ,(sem b r) )
      | Prod(a,b) ->  mult ( (sem a r), (sem b r))
      | Sum(a,b) ->  plus ( (sem a r), (sem b r))
      | Diff(a,b)  ->  diff ( (sem a r), (sem b r))
      | Minus(a) ->  minus( (sem a r))
      | And(a,b) ->  et ( (sem a r), (sem b r))
      | Or(a,b) ->  vel ( (sem a r), (sem b r))
      | Not(a) -> non( (sem a r))
      | Ifthenelse(a,b,c) -> 
            let g = sem a r in
            if typecheck("bool",g) then
               (if g = Bool(true) 
               then sem b r
               else sem c r)
            else failwith ("nonboolean guard") 
      | Let(i,e1,e2) -> sem e2 (bind i (sem e1 r) r)          
      | Fun(i,a) ->  makefun(Fun(i,a), r)
      | Appl(a,b) -> applyfun(sem a r, semlist b r)
 
and semlist el r = match el with
	  | [] -> []
	  | e::el1 -> (sem e r) :: (semlist el1 r)
 
and makefun ((a:exp),(x:eval env)) =
      (match a with
      |	Fun(ii,aa) -> Funval(a,x)
      |	_ -> failwith ("Non-functional object")) 
 
and applyfun ((ev1:eval),(ev2:eval list)) =
      ( match ev1 with
      | Funval(Fun(ii,aa),r) -> sem aa (bindlist(r,ii,ev2))
      | _ -> failwith ("attempt to apply a non-functional object"));;    

Here are some example of how to use it:

# let fesempio = Fun(["x"],Fun(["y"],Sum(Den("x"),Den("y"))));;
val fesempio : exp = Fun (["x"], Fun (["y"], Sum (Den "x", Den "y")))

This is the definition of a function that takes an argument x and return a function that will sum the argument to the argument of the returned function. To use it we apply it to some arguments:

# let aexp1 = Appl(fesempio,[Eint 3]);;
val aexp1 : exp =
  Appl (Fun (["x"], Fun (["y"], Sum (Den "x", Den "y"))), [Eint 3])
# let ris = sem aexp1 rho;;
val ris : eval = Funval (Fun (["y"], Sum (Den "x", Den "y")), <fun>)

Observe that ris is a function in our language.

# let aexp = Appl(Appl(fesempio,[Eint 3]),[Eint 5]);;
val aexp : exp =
  Appl (Appl (Fun (["x"], Fun (["y"], Sum (Den "x", Den "y"))), [Eint 3]),
   [Eint 5])
 
# let execution = sem aexp rho;;
val execution : eval = Int 8

Solution to the exercise on dynamic scope: as in dynamic scope the function has to be evaluated in the environment at the moment of its use, we do not need to have as functions result a closure as before, but we need simply an expression. Clearly, as we have not yet implemented any binding policy (except the one forced by the dynamic/static rules), the previous example with the function returning a function fails (why?)

Here we list the relevant changes:

type eval =	None   
     | Int of int 
     | Bool of bool
     | Funval of efun   
and efun = exp

and

let rec sem (e:exp) (r:eval env) =
      match e with
      ...
      | Fun(i,a) ->  makefun(Fun(i,a))
      | Appl(a,b) -> applyfun(sem a r, semlist b r, r)
 
and semlist ...
 
and makefun (a:exp) =
      (match a with
      |	Fun(ii,aa) -> Funval(a)
      |	_ -> failwith ("Non-functional object")) 
 
and applyfun ((ev1:eval),(ev2:eval list),(r:eval env)) =
      ( match ev1 with
      | Funval(Fun(ii,aa)) -> sem aa (bindlist(r,ii,ev2))
      | _ -> failwith ("attempt to apply a non-functional object"))  

We have changed the makefun that now returns an expression and we have added to the applyfun the environment where the function has to be evaluated.

The usual test: the factorial function (observe that as now we use the name of the function to apply to it an argument, we have to use also the Let construct:

# let fact = Let("fatt",
                Fun(["x"],
                Ifthenelse(Eq(Den("x"),Eint 1), Eint 1,
                   Prod(Appl(Den("fatt"),[Diff(Den("x"),Eint 1)]),Den("x")))),
                Appl(Den("fatt"),[Eint 5]));;
val fact : exp =
  Let ("fatt",
   Fun (["x"],
    Ifthenelse (Eq (Den "x", Eint 1), Eint 1,
     Prod (Appl (Den "fatt", [Diff (Den "x", Eint 1)]), Den "x"))),
   Appl (Den "fatt", [Eint 5]))
 
# sem fact (emptyenv None);;
- : eval = Int 120

Solution:

The syntax changes in this way, conveying the idea that a recursive function must have the keyword rec somewhere (and we expect that exp is a function where the ide appears):

type exp = 
       ....
      | Rec of ide * exp;;

and the interpreter is modified as follows:

let rec sem (e:exp) (r:eval env) =
      match e with
      ...
      | Rec(f,e) -> makefunrec (f,e,r)
 
 
and semlist el r = ...
 
 
and makefun ((a:exp),(x:eval env)) = ...
 
and applyfun ((ev1:eval),(ev2:eval list)) = ...
 
and makefunrec (i, e1, (r:eval env)) = 
    let calculateenv (rr: eval env)  = 
       (bind i (makefun(e1,rr)) r) in 
         let rec rfix =  
          function x -> calculateenv rfix x in makefun(e1,rfix);;  

The makefunrec calculate the environment rfix that have to be associated to the recursive function. It uses a function calculateenv that receives an environment rr and returns an environment where to the identifier of the recursive function is associated the function and the proper environment. What it really does is to calculate the smallest environment where this works.

Here the usal example of how it works:

# let fact = Rec("fatt",
      Fun(["x"],
       Ifthenelse(Eq(Den("x"),Eint 1),
          Eint 1,
          Prod(Appl(Den("fatt"),[Diff(Den("x"),Eint 1)]),Den("x")))));;
val fact : exp =
  Rec ("fatt",
   Fun (["x"],
    Ifthenelse (Eq (Den "x", Eint 1), Eint 1,
     Prod (Appl (Den "fatt", [Diff (Den "x", Eint 1)]), Den "x"))))
 
 
# let exec = Appl(fact,[Eint 5]);;
val exec : exp =
  Appl
   (Rec ("fatt",
     Fun (["x"],
      Ifthenelse (Eq (Den "x", Eint 1), Eint 1,
       Prod (Appl (Den "fatt", [Diff (Den "x", Eint 1)]), Den "x")))),
   [Eint 5])
 
# sem exec (emptyenv None);;
- : eval = Int 120