Operational Semantics

Practical Session - Week #5

The operational semantics of a programming language is specified by a set of formal evaluation rules that operate on the AST of an expression. The evaluation process can be specified as an algorithm eval(exp) : [AST -> Value].

In this session, we review:

What is an Environment?

An environment represents a partial function (as opposed to a total function) from symbols (variable names) to values. It supports the operation apply-env(env, var) which either returns the value of var in the environment env, or else throws an error.

We define the environment data type inductively by the following definition:

type Env = EmptyEnv | NonEmptyEnv;
type EmptyEnv = {tag: "EmptyEnv"}
type NonEmptyEnv = {tag: "Env"; var: string; val: Value; nextEnv: Env;}

The apply-env operation is defined recursively according to the structure of the data type:

export const applyEnv = (env: Env, v: string): Result<Value> =>
    isEmptyEnv(env) ? makeFailure("var not found " + v) :
    env.var === v ? makeOk(env.val) :
    applyEnv(env.nextEnv, v);

Example of an environment and a corresponding look-up operation - using the environment implementation used in class:

applyEnv(makeEnv('x', 3,
           makeEnv('y', 2,
              makeEnv('x', 1, makeEmptyEnv())), 'x')
=> { tag: 'Ok', value: 3 }

Note how the external binding for x to 3 hides the internal binding of x to 1.

applyEnv(makeEnv('x', 3,
           makeEnv('y', 2,
             makeEnv('x', 1, makeEmptyEnv())), 'y')
=> { tag: 'Ok', value: 2 }
applyEnv(makeEnv('x', 3,
           makeEnv('y', 2,
             makeEnv('x', 1, makeEmptyEnv())), 'z')
=> { tag: 'Failure', message: 'var not found z' }

Handling Primitives in L1

Let us recall the syntax of L1 using the BNF + Abstract Syntax specification we have developed in the previous lectures:

<program> ::= (L1 <exp>+) // program(exps:List(exp))
<exp> ::= <define-exp> | <cexp>
<define-exp> ::= (define <var-decl> <cexp>) // def-exp(var:var-decl, val:cexp)
<cexp> ::= <num-exp> // num-exp(val:number)
       | <bool-exp>  // bool-exp(val:boolean)
       | <prim-op>   // prim-op(op:string)
       | <var-ref>   // var-ref(var:string)
       | (<cexp> <cexp>*) // app-exp(rator:cexp, rands:List(cexp))
<prim-op> ::= + | - | * | / | < | > | = | not
<num-exp> ::= a number token
<bool-exp> ::= #t | #f
<var-ref> ::= an identifier token
<var-decl> ::= an identifier token

The values that can be returned in L1 are:

Value = number boolean PrimOp

Note: In L1, the only side-effect that we can get is from a define expression.

Representing Primitive Operators

In Scheme, when we compute this expression, we get:

> +
#<procedure:+>

That is, the value of the + expression (which is an expression of type Symbol) is a procedure in Scheme.

On the other hand, in JavaScript, when we evaluate the expression “+” we get:

+;
 ^
Syntax Error: Unexpected token ; ...

(In Node - the reader keeps waiting for the continuation of the expression starting with + or -).

That is, in the syntax of JavaScript - primitive operators alone are not expressions - they are only defined as part of larger expressions that contain them.

In the code reviewed in class, we implemented primitive operators as syntactic expressions of type prim-op. We represented primitive operators as a specific expression type in the AST
PrimOp(op: string). The value of a prim-op expression is itself. When we apply a primitive operator to arguments, we explicitly dispatch to each known primitive operator in the language and apply the corresponding primitive operation in the meta-language. This happens in the procedure
apply-primitive.

Let us implement a different strategy which is the same as in Scheme: primitives are variable references which refer to primitive procedures which are pre-defined in the global environment.

The steps of the change are:

The result of all the changes discussed in this section appears in accompanying zip file.

Change of AST for Primitives

;; The main change is that we remove the expression type prim-op
<cexp> ::= <num-exp> // num-exp(val:number)
       | <bool-exp>  // bool-exp(val:boolean)
       | <var-ref>   // var-ref(var:string)
       | (<cexp> <cexp>*) // app-exp(rator:cexp, rands:List(cexp))

Now, when we parse an expression such as (L1 (* 3 2)) we obtain an AST:

{
    "tag": "Program",
    "exps": [
        {
            "tag": "AppExp",
            "rator": {
                "tag": "VarRef",
                "var": "*"
            },
            "rands": [
                {
                    "tag": "NumExp",
                    "val": 3
                },
                {
                    "tag": "NumExp",
                    "val": 2
                }
            ]
        }
    ]
}

instead of:

{
    "tag": "Program",
    "exps": [
        {
            "tag": "AppExp",
            "rator": {
                "tag": "PrimOp",
                "op": "*"
            },
            "rands": [
                {
                    "tag": "NumExp",
                    "val": 3
                },
                {
                    "tag": "NumExp",
                    "val": 2
                }
            ]
        }
    ]
}

Change the Structure of the Returned Values

The second change is now how to evaluate the sub-expression { "tag": "VarRef", "var": "*" }: in this case, we expect to obtain a value of a different type - which is a primitive procedure mapped to the variable * in the global environment.

This has an impact on the structure of the values the interpreter can return:

where PrimProc is the type of the values returned in the meta-language (TypeScript in our case) when we compute the expressions +, *, -, /, not, <, >, =.

In more details, we define:

export type Value = number | boolean | PrimProc;
type PrimitiveProcedure = (args: Value[]) => Value;
type PrimProc = {
    tag: "PrimProc";
    op: PrimitiveProcedure;
};

Change the applyPrimitive procedure

The original version of applyPrimitive is:

const applyPrimitive = (proc: PrimOp, args: Value[]): Result<Value> =>
    proc.op === "+" ? makeOk(reduce((x, y) => x + y, 0, args)) :
    proc.op === "-" ? makeOk(reduce((x, y) => x - y, 0, args)) :
    proc.op === "*" ? makeOk(reduce((x, y) => x * y, 1, args)) :
    proc.op === "/" ? makeOk(reduce((x, y) => x / y, 1, args)) :
    proc.op === ">" ? makeOk(args[0] > args[1]) :
    proc.op === "<" ? makeOk(args[0] < args[1]) :
    proc.op === "=" ? makeOk(args[0] === args[1]) :
    proc.op === "not" ? makeOk(!args[0]) :
    makeFailure("Bad primitive op " + proc.op);

In the new version - we replace it with the following:

const applyPrimitive = (proc: PrimProc, args: Value[]): Result<Value> =>
    makeOk(proc.op(args));

This is a shorter version of the function - but one that exploits the fact that we have pre-defined the primitive functions and bound them to functions in the meta-language that all expect arguments in the same form (an array of Values).

Initializing the Global Environment with Primitive Values

This last step is where we map variable references to actual TypeScript functions. We initialize the global environment with the bindings of the primitives defined in L1 to the corresponding procedures in the meta-language.

const makeGlobalEnv = (): Env => 
  makeEnv('+', plus,
    makeEnv('-', minus,
      makeEmptyEnv()))

// where:
const plus : (args: number[]) => number =
    reduce((x, y) => x + y, 0, args)
const minus : (args: number[]) => number =
    reduce((x, y) => x - y, 0, args)

And in the procedure evalL1program, we initialize the global environment differently:

const evalL1program = (program: Program): Value =>
    evalExps(program.exps, makeGlobalEnv());  // instead of makeEmptyEnv()

This implementation explains properly what is meant by “primitive functions”: they are the functions which are pre-defined in the global environment when the interpreter starts running - without the need for the programmer to define them.

Adding a Primitive to the Interpreter

With this implementation, it is easy to add a primitive to the interpreter - we need only:

For example:

// Primitive operators are encoded as varRef bound out of the box to
// functions in the meta-language with an appropriate interface.
// The PrimProc wrapper is used to tag such primitive operator values in
// an unambiguous manner.
const makeGlobalEnv = (): Env =>
    makeEnv('+', makePrimProc((args: number[]) => reduce((x, y) => x + y, 0, args)),
    makeEnv('-', makePrimProc((args: number[]) => reduce((x, y) => x - y, 0, args)),
    makeEnv('*', makePrimProc((args: number[]) => reduce((x, y) => x * y, 1, args)),
    makeEnv('/', makePrimProc((args: number[]) => reduce((x, y) => x / y, 1, args)),
    makeEnv('display', makePrimProc((args: Value[]) => console.log(args)),
    makeEnv('newline', makePrimProc((args: Value[]) => console.log("")),
    makeEmptyEnv()))));

and we have two new primitives in our language (display and newline).

Order of Evaluation of Parameters in a Procedure Application

evalL1program(program) receives a program, which includes an ordered sequence of expressions. It iterates over the expressions and depending on the type of each expression, it either evaluates a DefineExp and obtains a new environment, which is then used to evaluate the next steps of the program; or it evaluates the expression.

In expressions such as (+ (+ 1 2) (+ 3 4) (+ 5 6)) the operational semantics does not specify the order of execution among the arguments - we could compute (+ 5 6) first and (+ 1 2) next, or in reverse, or even together (in parallel).

This is the case in the formal semantics of Scheme - the standard explicitly indicates that the order of evaluation of operands in an application is NOT specified.

This means that we can obtain different outputs if we insert side-effects as part of the operands depending on the implementation in Scheme:

(define side-effect
  (lambda (x) (display x) x))

(+ (* (side-effect 2) (side-effect 3))
   (* (side-effect 4) (side-effect 5)))

=> can display 
2345 26

or
4235 26

(or any other variant of the order of parameters)

L2 Evaluation

NOTE: In the rest of the notes, we return to the syntactic treatment of primitives as discussed in the lectures (as opposed to the semantic treatment discussed above).

The syntax of L2 extends that of L1 with two new expression types: IfExp and ProcExp

<program> ::= (L2 <exp>+) // program(exps:List(exp))
<exp> ::= <define-exp> | <cexp>
<define-exp> ::= (define <var-decl> <cexp>) // def-exp(var:var-decl, val:cexp)
<cexp> ::= <num-exp> // num-exp(val:number)
       | <bool-exp>  // bool-exp(val:boolean)
       | <prim-op>   // prim-op(op:string)
       | <var-ref>   // var-ref(var:string)
       | (if <exp> <exp> <exp>) // if-exp(test,then,alt)                                    ##### L2
       | (lambda (<var-decl>*) <cexp>+) // proc-exp(params:List(var-decl), body:List(cexp)) ##### L2
       | (<cexp> <cexp>*) // app-exp(rator:cexp, rands:List(cexp))
<prim-op> ::= + | - | * | / | < | > | = | not
<num-exp> ::= a number token
<bool-exp> ::= #t | #f
<var-ref> ::= an identifier token
<var-decl> ::= an identifier token

The Value types includes closure values in addition to the previous types:

Value = Number Boolean Prim-op Closure

Closure ::= (Closure (<var-decl>*) <cexp>+) // closure(params:List(var-decl), body:List(cexp))

Note that a proc-exp (lambda (x) (* x x)) is an expression while a closure is a value. They are of 2 different types - closures are the result of a computation.

The key change in L2 vs L1 is the support of closures when applying procedure values to arguments:

const L3applyProcedure = (proc: Value, args: Value[], env: Env): Result<Value> =>
    isPrimOp(proc) ? applyPrimitive(proc, args) :
    isClosure(proc) ? applyClosure(proc, args, env) :
    makeFailure("Bad procedure " + JSON.stringify(proc));

const applyClosure = (proc: Closure, args: Value[], env: Env): Result<Value> => {
    let vars = map((v: VarDecl) => v.var, proc.params);
    let body = renameExps(proc.body);
    let litArgs = map(valueToLitExp, args);
    return evalSequence(substitute(body, vars, litArgs), env);
}

The body is evaluated with evalExps - but we only return the last value that is computed: For example:

(lambda (x)
    (+ 1 x)
    (+ 2 x)) 

First we evaluate(+ 1 x) only then we evaluate (+ 2 x). The return value is the return value of the last expression.

The substitution procedure addresses 3 issues:

Renaming and Substitution

Renaming

Bound variables in expressions can be consistently renamed by new variables (that do not occur in the expression) without changing the intended meaning of the expression. That is, expressions that differ only by consistent renaming of bound variables are semantically equivalent.

For example, the following are equivalent pairs:

(lambda (x) x) <==> (lambda (x1) x1)
(lambda (x) (+ x y)) <==> (lambda (x1) (+ x1 y))  // y is not renamed because it occurs free

Why renaming?

(define z not)

(((lambda (x)
      (lambda (z) (x z)))
    (lambda (w) (z w)))
   ;; Note: z occurs free in the parent exp.
   #f)

For renaming we use the renameExps procedure:

const makeVarGen = (): (v: string) => string => {
    let count: number = 0;
    return (v: string) => {
        count++;
        return `${v}__${count}`;
    }
}

/*
Purpose: Consistently rename bound variables in 'exps' to fresh names.
         Start numbering at 1 for all new var names.
*/
const renameExps = (exps: CExp[]): CExp[] => {
    const varGen = makeVarGen();
    const replace = (e: CExp): CExp =>
        isIfExp(e) ? makeIfExp(replace(e.test), replace(e.then), replace(e.alt)) :
        isAppExp(e) ? makeAppExp(replace(e.rator), map(replace, e.rands)) :
        isProcExp(e) ? replaceProc(e) :
        e;
    // Rename the params and substitute old params with renamed ones.
    // First recursively rename all ProcExps inside the body.
    const replaceProc = (e: ProcExp): ProcExp => {
        const oldArgs = map((arg: VarDecl): string => arg.var, e.args);
        const newArgs = map(varGen, oldArgs);
        const newBody = map(replace, e.body);
        return makeProcExp(map(makeVarDecl, newArgs),
                           substitute(newBody, oldArgs, map(makeVarRef, newArgs)));
    }
    return map(replace, exps);
}

Notes on rename-exps:

Substitution

Substitute is an operation which replaces free occurrences of variable references in an expression by other expressions. Definition: A substitution s is a mapping from a finite set of variables to a finite set of expressions.

Substitutions are denoted using set notation. For example:

6 o {x=5} = 6

(+ x y) o {z = 5} = (+ x y)
 
(+ x y) o {x=5, y=6, z=7} = (+ 5 6)

(lambda (x) (+ x 6)) o {x=5} = 
    renaming: E turns into (lambda (x1) (+ x1 6)
    substitute: E turns into (lambda (x1) (+ x1 6))

( + (x z) ((lambda (x) x) y))  o {x = (lambda (x) x) , y = 7 , z =8}
    renaming: E turns into ( + (x z) ((lambda (x1) x1) y)) 
    renaming: s turns into {x = (lambda (x2) x2) , y = 7, z = 8}
    substitute: E turns into  ( + ((lambda (x2) x2) 8) ((lambda (x1) x1) 7))

Composition (combination) of Substitutions s and s′ , denoted s∘s′ , is a substitution s″ that extends s with a binding <x; s’ (x)> for every variable x for which s(x) is not defined.

For example:

#1: {} o {x = 3} = {x = 3}

#2: {x = 3} o {y = #t} = {x = 3, y = #t}

#3: {x = y} o {y = 3} = {x = 3, y = 3}            // Note that the binding of x changed to 3

#4: {x = y} o {y = x} = {x = x, y = x} = {y = x}  // What happens when we apply this substitution?

Let us explain #3 and #4:

Applying {x = y} o {y = 3}] (s o s') to any expression E, we want to obtain the same result as performing first s’ then s - that is:

` For any E, E o [{x = y} o {y = 3}] = [E o {x = y}] o {y = 3} `

Let us take an example for E that contains x and y:

` E = (x y) E o [{x = y} o {y = 3}] = [E o {x = y}] o {y = 3} = (y y) o {y = 3} = (3 3) ` After applying {x = y} there are no more instances of x, only instances of y in the result. Therefore, when we replace simultaneously x and y in the composed substitution, we must make sure x is replaced to 3 and not to y.

Let us look at #4: we apply the same logic as in #3, and obtain that:

` [{x = y} o {y = x}] = [{x = x, y = x}] `

The substitution of x into x is not introducing any modification, therefore, we can drop it - and we obtain:

` [{x = y} o {y = x}] = [{x = x, y = x}] = {y = x} `

Substitution involves renaming as a first step:

((+ x ((lambda (x) (* x 2)) 3))) o {x = 5} =
    Renaming: ((+ x ((lambda (x1) (* x1 2)) 3)))
    Substitute: ((+ 5 ((lambda (x1) (* x1 2)) 3)))

Question: Why do we need renaming?

Let us look at this program:

(lambda (x) (lambda (y) (y x)))

rename x -> a, y -> b - all ok:

(lambda (a) (lambda (b) (b a)))

From this, you might conclude that any substitution is allowed - i.e. any variable in any lambda term can be replaced by any other. This is not so. Consider the inner lambda in the first expression above:

(lambda (y) (y x))

In this expression, x is free - it is not bound by a lambda abstraction. If we were to replace y with x, the expression would become:

(lambda (x) (x x))

But we already specified that when we apply a substitution, we do not replace bound variables - so that:

(lambda (y) (y x)) o {y = x}

is not causing any harm - we return the same value unchanged, because y is bound.

But now consider what happens if we introduce a value into the expression that contains a binding with a name to a variable that occurred free in the original expression. The replacement will lead to a capture of the free variable by the new binding.

(define z not)

(((lambda (x)
      (lambda (z) (x z)))
    (lambda (w) (z w)))
   ;; Note: z occurs free in the parent exp.
   #f)

Work out the capture - step by step…

How it works with renaming:

;; rename z in (lambda (z) (x z)) ==> (lambda (z1) (x z1))
;; rename w in (lambda(w)(z w)) ==> (lambda(w1)(z w1))
;; substitute (lambda(z1)(x z1)) ∘ {x = (lambda(w1)(z w1))} ==> 
(lambda (z1)
    ((lambda (w1)
       (z w1)) ;z remains free!
     z1))

;; substitute ((lambda (w1) (z w1)) z1)∘ {z1 = #f}==>
((lambda(w1)
     (z w1))
   #f)

;;substitute (z w1) ∘ {w1 = #f}==>
(z #f)

;;substitute (z #f) ∘ {z = not}==>
(not #f) 
#t

Applicative Eval

Look at the next code:

((lambda (x z) 
     (* (+ x z) z))
   1 (+ 1 2))

Q: Evaluate the following expression according to the applicative-eval algorithm

A:

applicative-eval     [((lambda (x z) (* (+ x z) z)) 1 (+ 1 2))]
    applicative-eval [(lambda (x z) (* (+ x z) z))] ==> <Closure (x z) (* (+ x z) z)>
    applicative-eval [1] ==> 1
    applicative-eval [(+ 1 2)]
        applicative-eval [+] ==> #<primitive-procedure +>
        applicative-eval [1] ==> 1
        applicative-eval [2] ==> 2
   3
reduce:
    applicative-eval [(* (+ 1 3) 3)]
        applicative-eval [*] ==> #<primitive-procedure *>
        applicative-eval [(+ 1 3)]
            applicative-eval [+] ==> #<primitive-procedure +>
            applicative-eval [1] ==> 1
            applicative-eval [3] ==> 3
        ==> 4
        applicative-eval [3]==> 3
    12

Normal Eval

Q: Evaluate the following expression according to the normal evaluation algorithm:

(((lambda (x) 
      (lambda (y) 
        (* x y))) 
    (+ 1 2)) 
   2)  

A:

normal-eval[ (( (lambda (x)(lambda (y)(* x y)))(+ 1 2))2) ]
  normal-eval [( (lambda (x)(lambda (y)(* x y)))(+ 1 2)) ]
    normal-eval[(lambda (x)(lambda (y)(* x y)))] ==><closure (x) (lambda(y) (* x y))>
    substitute:
    (lambda(y) (* x y) ) ᵒ {x = (+ 1 2) } ==> (lambda(y) (* (+ 1 2) y) )
    reduce:
    normal-eval[lambda(y) (* (+ 1 2) y) ] ==><closure (y) (* (+ 1 2) y)>
    substitute:
    (* (+ 1 2) y) ᵒ { y = 2} ==> (* (+ 1 2) 2)
    Reduce:
    Normal-eval[ * (+ 1 2) 2 ] ==>
      Normal-eval[ * ] ==> <primitive-procedure: *>
      Normal-eval[ ( + 1 2) ] ==>
        Normal-eval[+] ==> <primitive-procedure: +>
        Normal-eval[1] ==> 1
        Normal-eval[2] ==> 2
      ==> 3
      Normal-eval[2] ==> 2
   ==> 6

applicative-eval VS normal-eval

Q:Does the evaluation Strategy matter?

Let us look at the next program:

(define test
  (lambda (x y)
    (if (= x 0)
        0
        y)))

(define zero-div
  (lambda (n)
    (/ n 0))) ; division by zero!

(test 0 (zero-div 5))

Normal Eval

normal-eval[(test 0 (zero-div 5))]
    normal-eval[test] ==> <closure (lambda (x y) (if (= x 0) 0 y))>

(if (= x 0) 0 y))ᵒ{x = 0} ==> (if (= 0 0) 0 y))

(if (= 0 0) 0 y))ᵒ{y = (zero-div 5)} ==> (if (= 0 0) 0 (zero-div 5) ))

reduce:

normal-eval[(if (= 0 0) 0 (zero-div 5)))]
    normal-eval[(= 0 0)]
        normal-eval[ = ] ==>#<primitive-procedure =>
    normal-eval[ 0 ] ==>0
    normal-eval[ 0 ] ==>0
    ==> #t
    normal-eval[0] ==> 0
==>0

Notice that we didn’t evaluate (div-zero 5)!

Applicative Eval

applicative-eval[(test 0 (zero-div 5))]
    applicative-eval[test] ==> <closure (lambda (x y) (if (= x 0) 0 y))>
    applicative-eval[0] ==> 0
    applicative-eval[(zero-div 5)]
        applicative-eval[zero-div]==><closure (lambda (n) (/ n 0))>
        applicative-eval[5]==> 5

We get a “division by zero” error !!!

Another example:

(define loop (lambda (x) (loop x)))

(define g (lambda (x y) y))

(g (loop 0) 7)

normal-eval will return 7 while applicative-eval will get into infinite loop. why is that?

We saw two examples where different manner of evaluation get different result.

Notice: If both evaluations don’t get into an infinte loop and/or an error - they both return the same value!

Distinguish between different evaluation strategies

Q: How can we distinguish what evaluation strategy the interpreter is using?

A: As we saw in the previous questions -

if we understand the differences between the evaluations methods we can write a program that each method will act different on.

for example:

(define applic
  (lambda ()
    (display 'applic)
    0))

(define test (lambda (x) 1))

(test (applic))

Normal eval will not have any side-effects while applicative eval will display “applic” to the screen. They both will return the value 1.

letrec

Let us recall the exp procedure:

; Signature: exp(b e)
; Purpose: to compute the function b^e
; Type: [Number * Number -> Number]
; Pre-conditions: b >= 0, e is natural
; Tests:
; (exp 2 3) => 8
; (exp 2 4) => 16
; (exp 3 4) => 81

(define exp
  (lambda (b e)
    (exp-iter b e 1)))

(define exp-iter
  (lambda (b e acc)
    (cond ((= e 0) acc)
           (else (exp-iter b (- e 1) (* b acc))))))

In this program both “exp” and “exp-iter” are public functions. but the user will only use “exp” so we want “exp-iter” to be non-public procedure.

how can we do that?

First attempt: we will use let

(define exp
  (lambda (b e)
    (let ((exp-iter (lambda (b e acc)
                      (cond ((= e 0) acc)
                      (else (exp-iter b (- e 1) (* b acc)))))))
    (exp-iter b e 1))))

Q: What is the problem with that program?

A: We use exp-iter in its definition (why is that a problem?)

Second attempt:

(define exp
  (lambda (b e)
    (letrec ((exp-iter (lambda (b e acc)
                         (cond ((= e 0) acc)
                         (else (exp-iter b (- e 1) (* b acc)))))))
    (exp-iter b e 1))))

Here we use letrec instead let so a defintion of a procedure can be recusive.

Can we do it better? Yes! By noticing that b stays constant throughout exp-iter, we can just use the existing b instead of passing it around as an argument.

Third attempt:

(define exp
  (lambda (b e)
    (letrec ((exp-iter (lambda (e acc)
                         (cond ((= e 0) acc)
                         (else (exp-iter (- e 1) (* b acc)))))))
    (exp-iter e 1))))