Operational Semantics: Substitution Model for Procedure Application

PPL 2023

We continue our exploration of operational semantics by addressing the case of procedure application. The \(L2\) language extends \(L1\) by introducing:

User defined procedures (lambda expressions)
Conditional expressions (if expressions)

These two constructs combine well - so that we can construct recursive functions (which require a condition between the base case and the recursive case).

\(L2\) Syntax

The syntax of \(L2\) extends that of \(L1\) with two new expression types - if-exp and proc-exp:

<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,else)                                   ##### 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 corresponding TypeScript implementation of this AST (and its extension into L3) with a parseL3 function is provided in L3-ast.ts

\(L2\) Value Type

A program in \(L2\) can now use user defined procedures such as:

(L2 
  (define square (lambda (x) (* x x)))
  (+ (square 2) (square 3)))

To determine which values can be computed by \(L2\) programs, we proceed inductively on the structure of \(L2\)-ASTs. The same values as those in \(L1\) can be computed, and we must analyze the two new types of expressions:

IfExp expressions return the value of either the then-branch or the else-branch, which can be any cexp expressions. Thus if-exp does not compute new types of values.
ProcExp expressions return a new type of value - which we have called a closure.

We must then extend the definition of the Value type to include closure values:

Value = Number | Boolean | Prim-op | Void | Closure

We define the closure data type as a record with two fields:

Params: a list of var-decl values
Body: a list of cexp values

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

Note that a ProcExp (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.

\(L2\) Evaluation Rules

The evaluation rules that define the operational semantics of \(L2\) include the same rules as those of \(L1\) for the \(L1\) expression types. We must specify evaluation rules for the new expression types:

Evaluation of Conditional Expressions

eval(IfExp(test, then, else), env) => 
    // test, then, else are of type cexp
    let c:Value = eval(test, env)
        If c is considered a true value:
            return eval(then, env)
        else
            return eval(else, env)

We must define what counts as a true value in the testing of the condition in an IfExp. This definition of what counts as true is a semantic decision - which is different in different languages.

In Scheme, a true value is anything that is not #f. We implement this in this procedure in our interpreter code:

// Purpose: Define what is considered a true value in an if-exp
export const isTrueValue = (x: Value): boolean =>
    ! (x === false);

In JavaScript, the definition of what counts as true in an IfExp is more complicated - it is any value that is:

not false
not undefined
not null
not +0, not -0, not NaN (not a number, the result of performing an arithmetic operation which cannot return a valid number)
not an empty string

Evaluation of Procedure Expressions

eval(proc-exp(params, body), env) =>
    // Construct a closure value
    return makeClosure(params, body)

When we compute the value of a procedure expression, there is no actual computation going on besides the packaging of the parameters and the body into a closure record.
The body is not computed as this stage. It will only be computed when the procedure is actually applied to arguments.

This property is important: it means we can delay the computation of an expression by wrapping it inside a procedure, and invoking the procedure only later. We will exploit this property in Chapter 4.

Procedure Application

We have covered the two new types of expressions with the evaluation rules above – but another place in the operational semantics must now be updated because of the presence of closures: procedure application.

In the \(L1\) case, the only procedure value that could be applied to arguments was a primitive operator. This was covered in the evaluation rule for AppExp expressions:

eval(AppExp(rator, rands) =>
    // rator is of type Cexp
    // rands is of type List(Cexp)
    let proc = eval(rator,env)
        args = [eval(r,env) for r in rands]
        return applyProc(proc, args)

ApplyProc defines how a procedure value is applied to values. We must now define how a closure value is applied to argument values.

In order to evaluate an AppExp whose operator evaluates to a closure, we followed the same process as for primitive procedures: first evaluate the elements of the combination, then apply the closure (which is the value of the operator) to the arguments (which are the values of the operands). This strategy is what is called applicative order evaluation. It is the standard evaluation strategy in most programming languages, but we will discuss an alternative strategy in the next section (normal evaluation).

To apply a closure to arguments, we define the substitution model: evaluate the body of the closure with each formal parameter replaced by the corresponding argument.

Let’s follow an example:

(define square (lambda (x) (* x x)))
(square 5)

The evaluation process is the following:

1. Evaluate defineExp:
    1.1 Evaluate (lambda (x) (* x x)) => (closure (x) (* x x))
    1.2 Bind square to the value (closure (x) (* x x)) in the global environment
2. Evaluate (square 5) (an AppExp) in the global environment:
    2.1 Evaluate square (a VarRef expression) => (closure (x) (* x x))
    2.2 Evaluate 5 (a NumExp expression) => 5
    2.3 ApplyProc[ (closure (x) (* x x)) (5) ]
        ;; To clarify the process let us use full AST for the closure elements
        ;; (closure [(VarDecl x)] [(AppExp (PrimOp *) [(VarRef x), (VarRef x)])])
        2.3.1 Substitute the VarRef free occurrences of the VarDecl in body 
              with the corresponding value
              Substituted-body = [(AppExp (PrimOp *) [5, 5])]
        2.3.2 Evaluate the resulting substituted body:
            return eval(substituted-body)
                2.3.2.1 Eval (PrimOp *) => (PrimOp *)
                2.3.2.2 Eval 5 => 5
                2.3.2.3 Eval 5 => 5
                2.3.2.4 ApplyProc( (PrimOp *), [5, 5] )
                    2.3.2.4.1 ApplyPrimitive( (PrimOp *), [5, 5] ) => 25

We must clarify three aspects of the applicative-eval substitution model:

Type of the substituted elements into the AST of the body
Substitute only free occurrences of the params in the body
Need to rename bound variables inside the body to avoid variable capture

Substitute Expressions instead of Values

Let us analyze the types of the objects manipulated in the substitution operation above:

    ;; (closure [(VarDecl x)] [(AppExp (PrimOp *) [(VarRef x), (VarRef x)])])
    2.3.1 Substitute the VarRef free occurrences of the VarDecl in body 
            with the corresponding value
            Substituted-body = [(AppExp (PrimOp *) [5, 5])]

The applyProc procedure receives arguments which are all of type Value (proc is a Value which can be either a PrimOp or a Closure value, rands is a list of Values).

The body of the closure is a list of CExp expressions. Our objective is to replace all VarRef occurrences in the body with the corresponding values of the arguments (in our example, we want to replace (VarRef x) with 5).

There is a typing problem with this operation: 5 is a Value, while (VarRef x) is an expression. If we replace (VarRef x) with the value 5 (a number), the resulting body is not a valid AST.

To address this discrepancy, we must map the values of the arguments to corresponding expressions. This mapping is performed in our interpreter with the following function:

// Purpose: Transform a value into a literal expression denoting this value
// Pre-conditions: val is not void
const valueToLitExp = (v: Value): NumExp | BoolExp | StrExp | LitExp | PrimOp | ProcExp =>
    isNumber(v) ? makeNumExp(v) :
    isBoolean(v) ? makeBoolExp(v) :
    isString(v) ? makeStrExp(v) :
    isPrimOp(v) ? v :
    isClosure(v) ? makeProcExp(v.params, v.body) :
    makeLitExp(v);

As a result, the closure application above is processed as follows:

    ;; (closure [(VarDecl x)] [(AppExp (PrimOp *) [(VarRef x), (VarRef x)])])
    2.3.1 Substitute the VarRef free occurrences of the VarDecl in body 
            with the corresponding value
            Substituted-body = [(AppExp (PrimOp *) [NumExp(5), NumExp(5)])]

and we confirm that the resulting substituted-body is a valid AST.

In summary, the substitution procedure has type:

// @Pre: vars and exps have the same length
export const substitute = (body: CExp[], vars: string[], exps: CExp[]): CExp[]

Substitute Only Free Variable Occurrences in the Body

When we apply a closure to arguments, we consider the body and the params of the closure separately. If you look at:

(closure (x) (* x y))

in the body of the closure - the variable x occurs bound (it is bound by the parameter of the closure) and the variable y occurs free.

If we now look at the body separately - (* x y) - then the variables which were bound to the params now appear free in the body.

These variable references are the occurrences we must replace with the value of the argument.

Consider the case of another bound occurrence of the x variable in the body as in this example:

(closure (x)            ; 1
  ((lambda (x) (* x x)) ; 2
   (+ x x)))            ; 3

In this case, the var-ref occurrences in line 2 are bound in the body to the var-decl in line 2, while the occurrences in line 3 are free.

When we apply this closure to the value 2, we must replace the free occurrences in line 3 but leave those in line 2 unchanged.

The substitution algorithm is implemented in the following function - which is a typical syntax-driven function, which traverses a list of ASTs, and recursively transforms the nodes. The only expression type where an actual transformation is performed is VarRef.

Observe how the code of the transformation is similar to the code of applyEnv we discussed in the previous lecture.

When traversing a proc-exp within the body (as in the example we just reviewed above), substitute removes from the list of variables to be substituted the variables which are now bound by the new var-decls of the proc-exp. This is performed with the call to filter.

// @Pre: vars and exps have the same length
export const substitute = (body: CExp[], vars: string[], exps: CExp[]): CExp[] => {
    const subVarRef = (e: VarRef): CExp => {
        const pos = indexOf(e.var, vars);
        return ((pos > -1) ? exps[pos] : e);
    };
    
    const subProcExp = (e: ProcExp): ProcExp => {
        const argNames = map((x) => x.var, e.args);
        const subst = zip(vars, exps);
        const freeSubst = filter((ve) => !includes(first(ve), argNames), subst);
        return makeProcExp(e.args, substitute(e.body, 
                                              map((x: KeyValuePair<string, CExp>) => x[0], freeSubst), 
                                              map((x: KeyValuePair<string, CExp>) => x[1], freeSubst)));
    };
    
    const sub = (e: CExp): CExp => isNumExp(e) ? e :
        isBoolExp(e) ? e :
        isPrimOp(e) ? e :
        isLitExp(e) ? e :
        isStrExp(e) ? e :
        isVarRef(e) ? subVarRef(e) :
        isIfExp(e) ? makeIfExp(sub(e.test), sub(e.then), sub(e.alt)) :
        isProcExp(e) ? subProcExp(e) :
        isAppExp(e) ? makeAppExp(sub(e.rator), map(sub, e.rands)) :
        e;
    
    return map(sub, body);
};

Avoid Capturing Free Variables During Substitution

Consider the following program:

(define z (lambda (x) (* x x)))

(((lambda (x) (lambda (z) (x z))) ; 1
  (lambda (w) (z w)))             ; 2
 2)

If we apply the substitution model as presented so far when computing the 2nd expression - we replace x with the expression (lambda (w) (z w)) (which is the parameter passed as the x argument in line 1).

The resulting substituted body is:

(lambda (z) ((lambda (w) (z w)) z))

The problem in this substitution is that the inner var-ref z coming from the function (lambda (w) (z w)) is now captured by the (lambda (z) ...) context in which we operated the substitution.

As a result, this z var-ref now refers to the (lambda (z) ...) var-decl instead of referring to the global (define z ...) var-decl as it should.

This effect is called free variable capture and we must avoid it.

The simplest solution to address this problem is to ensure that before we perform substitution, we rename consistently all the bound variables that occur in the body with fresh names.

This solution relies on the observation we mentioned in 2.4 Syntactic Operations that the actual name of variables does not modify the semantics of expressions as long as their lexical address remains consistent.

The renaming algorithm is performed consistently through a syntax-driven traversal of the body AST. It is implemented in the following manner in the interpreter. Note that the only type of expressions which are transformed in this AST transformation are proc-exp constituents.

/*
    Purpose: create a generator of new strings of the form v__n
    with n is incremented at each call. 
    Note the typical usage of a closure with side effect of the closed variable.
    
    Example:
    const gen = makeVarGen();
    console.log(gen("v")) => "v__1"
    console.log(gen("v")) => "v__2"
*/
export 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.
Example: renameExps([parse("(lambda (x) ((lambda (x) x) (+ x x)))")])
  ==> [(lambda (x__1) ((lambda (x__2) x__2) (+ x__1 x__1)))]
*/
export 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);
};

The Apply Procedure Summarized

Putting all elements discussed above together, the apply-proc procedure implements the following algorithm:

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

When evaluating a procedure call:

we make sure the body is renamed so that we avoid capturing free variables
we map arguments to lit-exps
then we perform the substitution

When describing the apply procedure operation, we use the following terminology:

Substitute formal parameters
Reduce (evaluate the substituted body)

Renaming and Substitution Operations

Let us review the properties of the two operations we defined over ASTs: 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 considered equivalent.

For example, the following are equivalent pairs:

(lambda (x) x) ==> (lambda (x1) x1)

(+ x ( (lambda (x) (+ x y)) 4)) ==> (+ x ( (lambda (x1) (+ x1 y)) 4))

;; Incorrect renaming:
(+ x ( (lambda (y) (+ y y)) 4)) ==> (+ x1 ( (lambda (x1) (+ x1 y)) 4))

Compare this operation of renaming with the Lexical Address transformation we defined in Section 2.4. If we transform an expression E1 and its renamed version rename(E1) into lexical address notation and remove the names of the variables (x depth pos) - we will obtain identical expressions.

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:

{x = 3, y = a, z = #t, w = (lambda (x) (+ x 1))} 
is a substitution

{x = 3, x = a, z = #t, w = (lambda (x) (+ x 1))} 
is not a substitution because the variable x is mapped to 2 distinct values.

In these expressions, we denote expressions in their unparsed form instead of the more verbose AST form - but remember that substitutions map variable names to expressions. For example,

{x = 3, y = a, z = #t}

really denotes:

{x = (num-exp 3), y = (lit-exp a), z = (bool-exp #t)}

Composition (combination) of Substitutions

The composition of substitutions \(s\) and \(s'\), denoted \(s \circ 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:

{x = 3, y = a} o {z = #t, w = (lambda (x) (+ x 1))} =
{x = 3, y = a, z = #t, w = (lambda (x) (+ x 1))}

The empty substitution {} is the neutral element of the substitution-composition operation: For every substitution \(s\), \(\{\} \circ s = s \circ \{\} = s\).

Substitution Application

By definition, The substitute operation consists of applying a substitution \(s\) to an expression \(E\). This operation is denoted \(E \circ s\) (or just \(Es\) if no confusion arises), and involves replacing free variable occurrences in \(E\) by other expressions. Substitution is performed in two steps:

Consistent renaming of the expression \(E\) and the expressions in \(s\).
Simultaneous replacement of all free occurrences of the variables of \(s\) in the renamed \(E\) by the corresponding renamed expressions of \(s\).

Substitution Examples

10 o {x = 5} = 10: No renaming; no replacement.
(+ x y) o {x = 5} = (+ 5 y): No renaming; just replacement.
(+ x y) o {x = 5, y = 'x} = (+ 5 'x): No renaming; just replacement.
((+ x ((lambda (x) (+ x 3)) 4))) o {x = 5} =
1. Renaming: \(E\) turns into ((+ x ((lambda (x1) (+ x1 3)) 4)))
2. Substitute: \(E\) turns into ((+ 5 ((lambda (x1) (+ x1 3)) 4)))
(lambda (y) (((lambda (x) x) y) x)) o {x = (lambda (x) (y x))} =:

Variable y in the substitution is free. It should stay free after the substitution application.
1. Renaming: The substitution turns into {x = (lambda (x1) (y x1))}; \(E\) turns into (lambda (y2) (((lambda (x3) x3) y2) x))
2. Substitute: \(E\) turns into (lambda (y2) ( ((lambda (x3) x3) y2) (lambda (x1) (y x1)))

Observe: What would be the result without renaming? Note the difference in the binding status of the variable y.

NOTE: In manual derivation exercies, if we observe there is no need for renaming, we skip the renaming step. For example:

((+ x ((lambda (x) (+ x 3)) 4))) o {x = 5} = ((+ 5 ((lambda (x) (+ x 3)) 4)))

Applicative Eval Examples

Let us trace the evaluation of the applicative eval algorithm on the following \(L2\) program:

(L2
  (define square (lambda (x) (* x x)))
  (define sum-of-squares (lambda (x y) (+ (square x) (square y))))
  (define f (lambda (a) (sum-of-squares (+ a 1) (* a 2)))
  (f 5)) ;; 136

We skip the evaluation of the three def-exp expressions, which bind the variables to closures - and trace the evaluation of (f 5):

applicative-eval[ (f 5) ] ==>
    applicative-eval[ f ] ==> <Closure (a) (sum-of-squares (+ a 1) (* a 2) )>
    applicative-eval[ 5 ] ==> 5
==>
applicative-eval[ (sum-of-squares (+ 5 1) (* 5 2)) ] ==>
    applicative-eval[sum-of-squares] ==> <Closure (x y) (+ (square x) (square y))>
    applicative-eval[ (+ 5 1) ] ==>
        applicative-eval[ + ] ==> <prim-op +>
        applicative-eval[ 5 ] ==> 5
        applicative-eval[ 1 ] ==> 1
    ==> 6
    applicative-eval[ (* 5 2) ] ==>
        applicative-eval[ * ] ==> <prim-op *>
        applicative-eval[ 5 ] ==> 5
        applicative-eval[ 2 ] ==> 2
    ==> 10
==>
applicative-eval[ (+ (square 6) (square 10)) ] ==>
    applicative-eval[ + ] ==> <prim-op +>
    applicative-eval[ (square 6) ] ==>
        applicative-eval[ square ] ==> <Closure (x) (* x x)>
        applicative-eval[ 6 ] ==> 6
    ==>
    applicative-eval[ (* 6 6) ] ==>
        applicative-eval[ * ] ==> <prim-op *>
        applicative-eval[ 6 ] ==> 6
        applicative-eval[ 6 ] ==> 6
    ==> 36
    applicative-eval[ (square 10) ]
        applicative-eval[ square ] ==> <Closure (x) (* x x)>
        applicative-eval[ 10 ] ==> 10
    ==>
    applicative-eval[ (* 10 10) ] ==>
        applicative-eval[ * ] ==> <primitive-procedure *>
        applicative-eval[ 10 ] ==> 10
        applicative-eval[ 10 ] ==> 10
    ==> 100
==> 136

Example with Renaming

Let us trace the evaluation of the following program:

(L2
  (define y 4)
  (define f (lambda (g) 
              (lambda (y) (+ y (g y)))))
  (define h (lambda (x) (+ x y)))
  (f h)) 
==> 
<Closure (y1) (+ y1 ((lambda (x) (+ x y)) y1))>

Trace of the algorithm:

applicative-eval[ (f h) ] ==>
    applicative-eval[ f ] ==> <Closure (g) (lambda (y) (+ y (g y)))>
    applicative-eval[ h ] ==> <Closure (x) (+ x y)>
==>
Substitute – rename both expressions and replace:
    Map the closure value of f to the corresponding lambda expression
    (lambda (y2) (+ y2 (g y2))) o {g = (lambda (x1) (+ x1 y))}
==>
Reduce - applicative-eval[ (lambda (y2) (+ y2 ((lambda (x1) (+ x1 y)) y2 ) )) ]
==>
<Closure (y2) (+ y2 ((lambda (x1) (+ x1 y)) y2) ) >

Renaming plays here an essential role. Without it, the application ((f h) 3) would replace all free occurrences of y by 3, yielding 9 as the result, instead of 10 - the correct value when the inner y variable reference remains bound to the global var-decl of y to 4.

Parameter Passing Mode: By Value

The substitution model – applicative order uses the call-by-value method for parameter passing.

This is the standard evaluation model in Scheme, and the most frequent method in other languages as well (JavaScript, C++, Java).

\(L3\): Compound Values and Quoted Literal Expressions

Let us extend \(L2\) with support for compound values, leading to the definition of the \(L3\) language.

In this language, the AST is extentend with new primitives to support compound values (lists), we also introduce a special value for the empty list ('()) which the parser must recognize and support for compound literal expressions: up to this point, the only literal expressions we supported were numbers, strings and booleans.

The expanded AST for \(L3\) is:

;; <program> ::= (L3 <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,else)                                   ## L2
;;        | (lambda (<var-decl>*) <cexp>+) // proc-exp(params:List(var-decl), body:List(cexp)) ## L2
;;        | (quote <sexp>) // lit-exp(val:Sexp)                                                ##### L3
;;        | (<cexp> <cexp>*) // app-exp(rator:cexp, rands:List(cexp))
;; <prim-op> ::= + | - | * | / | < | > | = | not |  and  |  or  |  eq? 
;;        | cons | car | cdr | pair? | list? | number? | boolean? | symbol?                    ##### L3
;;        | display | newline                                                                  ##### L3
;; <num-exp> ::= a number token
;; <bool-exp> ::= #t | #f
;; <var-ref> ::= an identifier token
;; <var-decl> ::= an identifier token
;; <sexp> ::= a symbol token | ( <sexp>* ) | ( <sexp> . <sexp> )                               ##### L3

The main additions in \(L3\) is the fact that the set of computed values now includes complex composite values (lists). The set of computed values is now:

Value = Number | Boolean | Prim-op | Closure | Void | SExp
SExp = Symbol | Number | Boolean | EmptySExp | Pair(SExp, SExp)

To support these composite datatypes, we introduce value constructors and accessors as primitives (cons, car, cdr) and the corresponding type predicates as primitives as well (pair?, list?, symbol?) and equality predicate (eq?) which must be capable to recognize the empty-list value. We also introduce side effect primitives (display and newline).

The empty list special value (which is a value which is not a number, not a boolean and not a symbol) must be supported in the syntax.

The last modification we introduce is to support literal expressions for the new compound values. We use the Scheme quote special operator to support these. An expression:

(quote <sexp>)

is a special expression which is computed according to the following computation rule:

eval((quote <sexp>)) =>
    return <sexp>

For example:

(quote a) => 'a
(quote (a b)) => '(a b)

The special form (quote <sexp>) is written in Scheme in a shorthand notation '<sexp> - for example, 'a for a symbol or '(a b) for a list.

To support the apply-procedure and substitution of values back as expressions, we took care in the procedure to turn values into expressions with a special case for Literal Expressions that wrap SExp values:

const valueToLitExp = (v: Value): NumExp | BoolExp | StrExp | LitExp | PrimOp | ProcExp =>
    isNumber(v) ? makeNumExp(v) :
    isBoolean(v) ? makeBoolExp(v) :
    isString(v) ? makeStrExp(v) :
    isPrimOp(v) ? v :
    isClosure(v) ? makeProcExp(v.params, v.body) :
    makeLitExp(v);

Since SExps are not a type that exists in TypeScript, we must implement this type as part of the possible values computed by \(L3\). This is implemented in the definition of the L3-Value module:

// ========================================================
// SExp
export type CompoundSExp = {
    tag: "CompoundSexp";
    val1: SExpValue;
    val2: SExpValue;
}
export type EmptySExp = {
    tag: "EmptySExp";
}
export type SymbolSExp = {
    tag: "SymbolSExp";
    val: string;
}

export type SExpValue = number | boolean | string | PrimOp | Closure | SymbolSExp | EmptySExp | CompoundSExp;
export const isSExp = (x: any): x is SExpValue =>
    typeof(x) === 'string' || typeof(x) === 'boolean' || typeof(x) === 'number' ||
    isSymbolSExp(x) || isCompoundSExp(x) || isEmptySExp(x) || isPrimOp(x) || isClosure(x);

export const makeCompoundSExp = (val1: SExpValue, val2: SExpValue): CompoundSExp =>
    ({tag: "CompoundSexp", val1: val1, val2 : val2});
export const isCompoundSExp = (x: any): x is CompoundSExp => x.tag === "CompoundSexp";

export const makeEmptySExp = (): EmptySExp => ({tag: "EmptySExp"});
export const isEmptySExp = (x: any): x is EmptySExp => x.tag === "EmptySExp";

export const makeSymbolSExp = (val: string): SymbolSExp =>
    ({tag: "SymbolSExp", val: val});
export const isSymbolSExp = (x: any): x is SymbolSExp => x.tag === "SymbolSExp";

The SExp datatype must also be supported in the parser for \(L3\) - so that we expand the L3-AST module with support for parsing SExp values and returning quoted SExp values accordingly. This is supported in the following function:

// In L3-AST

// sexps has the shape (quote <sexp>)
export const parseLitExp = (param: Sexp): Result<LitExp> =>
    mapv(parseSExp(param), (sexp: SExpValue) => 
         makeLitExp(sexp));

export const isDottedPair = (sexps: Sexp[]): boolean =>
    sexps.length === 3 && 
    sexps[1] === "."

export const makeDottedPair = (sexps : Sexp[]): Result<SExpValue> =>
    bind(parseSExp(sexps[0]), (val1: SExpValue) => 
        mapv(parseSExp(sexps[2]), (val2: SExpValue) =>
             makeCompoundSExp(val1, val2)));

// x is the output of p (sexp parser)
export const parseSExp = (sexp: Sexp): Result<SExpValue> =>
    sexp === "#t" ? makeOk(true) :
    sexp === "#f" ? makeOk(false) :
    isString(sexp) && isNumericString(sexp) ? makeOk(+sexp) :
    isSexpString(sexp) ? makeOk(sexp.toString()) :
    isString(sexp) ? makeOk(makeSymbolSExp(sexp)) :
    sexp.length === 0 ? makeOk(makeEmptySExp()) :
    isDottedPair(sexp) ? makeDottedPair(sexp) :
    isArray(sexp) ? (
        // fail on (x . y z)
        sexp[0] === '.' ? makeFailure(`Bad dotted sexp: ${sexp}`) : 
        bind(parseSExp(first(sexp)), (val1: SExpValue) =>
             mapv(parseSExp(rest(sexp)), (val2: SExpValue) =>
                  makeCompoundSExp(val1, val2))) 
        ) :
    sexp;

The interpreter which implements all of the changes is available in:

L3 AST - Abstract syntax and parser including literal expressions
L3 Value - Definition of values (SExp and Closures)
L3 Env - Environment (empty and extended)
L3 Eval - Interpreter
evalPrimitive - Type safe evaluation of primitive calls
substitute - substitute and rename algorithms
L3.Tests - Tests

With this interpreter, we can write programs such as the following - many examples are shown in the Tests:

(L3 (define empty? (lambda (x) (eq? x '())))
    (define filter
      (lambda (pred l)
        (if (empty? l)
            l
            (if (pred (car l))
                (cons (car l) (filter pred (cdr l)))
                      (filter pred (cdr l))))))
    (filter (lambda (x) (not (= x 2)))
            '(1 2 3 2)))

Error Handling

Both the parser and the interpreter of \(L3\) handle possible errors - either in the syntax of the program to be parsed or in the semantics of the program, that is, the interpreter must be capable of detecting an error at runtime and to report this error properly.

We implement error handler in the parser using the Result monad approach:

export const parseL3 = (x: string): Result<Program>

That is, the parser either returns a valid Program result wrapped in an Ok value or a Failure. Similarly, we define the interpreter with the following signature:

const L3applicativeEval = (exp: CExp, env: Env): Result<Value>

That is, the interpreter can obtain as parameter a valid CExp, and it returns either an OK Value or a Failure. We must make sure the interpreter is never passed a Failure value in one of the recursive calls.
This is ensured by consistently adopting the pattern of bind(<call returning a Result<Value> >, (value: Value) => continuation)

This means that we do not change the definition of the AST data type or the Value data type to include Error as a possible values. There are two reasons for this decision:

Errors are not real ASTs or Values - they are semantically outside the domains of the syntax and the interpreter.
Errors are absorbing elements of the interpreter.

Absorbing means that if we compose an Error with any other value when interpreting a compound expression, then the whole value must become an Error - regardless of the rules of evaluation of the expression (whether it is a special form or an application). For example, consider the rule of evaluation of an IfExp expression: it is a special form - that is, not all sub-expressions are evaluated before the value of the compound IfExp is computed. The semantic definition is:

To eval: IfExp(then, else, alt) in env:
   if isTruValue(eval(then, env)) then
       eval(then, env)
   else
       eval(alt, env)

With error processing, the definition is implemented using the bind pattern:

const evalIf = (exp: IfExp, env: Env): Result<Value> =>
    bind(L3applicativeEval(exp.test, env), (test: Value) => 
         isTrueValue(test) ? L3applicativeEval(exp.then, env) : 
         L3applicativeEval(exp.alt, env));

We first test whether the evaluation of the exp.test sub-expression returns an error. If it is the case, the whole expression is reduced to this error - without evaluating any of the sub-expressions exp.then or exp.alt.

Similarly, when evaluating an application expression (AppExp) - the semantic rule is:

To eval: AppExp(rator, rands) in env:
   let proc = eval(rator, env)
       args = map(eval, rands)
       applyProc(proc, args)

With error processing, the processing is expanded into:

    isAppExp(exp) ? bind(L3applicativeEval(exp.rator, env), (rator: Value) =>
                         bind(mapResult(param => L3applicativeEval(param, env), exp.rands), (rands: Value[]) =>
                              L3applyProcedure(rator, rands, env))) :

In addition to the general bind and mapv patterns which push a Result<T> value into a diagonal function T -> Result<T> or a flat function T -> T, we also introduce the mapResult function:

mapResult applies a procedure f of type [T1 => Result<T2>] to an array T1[] and executes f on each of the elements of the array. If one of them returns a Failure, this failure is returned, else an Ok wrapper of the array of results is returned.
mapResult is a safe version of map for functions that can return a Failure. It does not return an array Result<T2>[] but instead a value of type Result<T2[]>.

export const bind = <T, U>(r: Result<T>, f: (x: T) => Result<U>): Result<U> =>
    isOk(r) ? f(r.value) : r;

// bind a result value into a happy path function that does not fail
export const mapv = <T, U>(r: Result<T>, f: (x: T) => U): Result<U> =>
    isOk(r) ? makeOk(f(r.value)) : r;

// Purpose: Like map on an array - but when the transformer function applied returns a Result<T>
//          With f: T=>Result<U> and list: T[] return a Result<U[]> 
//          If one of the items of the list fails on f - returns the Failure on the first item that fails.
// Example: 
// mapResult((x) => x === 0 ? makeFailure("div by 0") : makeOk(1/x), [1,2]) ==> {tag:"Ok", value:[1, 0.5]}
// mapResult((x) => x === 0 ? makeFailure("div by 0") : makeOk(1/x), [1,0,2]) ==> {tag:"Failure", message:"div by 0"}
export const mapResult = <T, U>(f: (x: T) => Result<U>, list: T[]): Result<U[]> =>
    isEmpty(list) ? makeOk([]) :
    bind(f(first(list)), 
         (fa: U) => bind(mapResult(f, rest(list)), 
                         (fas: U[]) => makeOk(cons(fa, fas))));

The net result of guarding against errors at all stages of the parsing and evaluation process allows us to handle errors in a proper manner without using exception in the meta-language.
We do not throw exceptions. Instead, we return Result values, and properly guard against composing Failure values against other types of values along the whole evaluation process.

This is an important methodological point: we can implement a process of evaluation which is in essence equivalent to throwing exceptions without requiring exceptions in the meta-language. In a sense, we have explained what throwing an exception would mean in the semantic domain by enforcing the fact that Failure is an absorbing element for all semantic operations that operate over Result<Value>.

Normal Order Evaluation Algorithm

applicative-eval implements an eager approach in evaluation: arguments are evaluated immediately, before the closure is reduced.

An alternative algorithm implements a lazy approach in evaluation: it avoids evaluating arguments until the last moment it is necessary. When is a value necessary in the evaluation process?

When we need to decide a computation branch.
When we need to apply a primitive procedure.

The normal evaluation algorithm is similar to the applicative-eval we have just reviewed. The only difference, which leads to the lazy approach, moves the step of argument evaluation just before a primitive procedure is applied. Otherwise, the algorithm is unchanged, and the computation rules for the special operators are the same.

This is a remarkably small change in the algorithm with a deep change to the way the language behaves.

To describe the Normal Order evaluation algorithm, we only need to change a single evaluation rule - that for application expressions:

The applicative-eval form we first saw is:

applicative-eval(app-exp(rator, rands)) =>
    // rator is of type cexp
    // rands is of type List(cexp)
    let proc = applicative-eval(rator,env)
        ;; First evaluate parameters
        args = [applicative-eval(r,env) for r in rands]
        ;; Then invoke the procedure on the values
        return apply-proc(proc, args)

To obtain the normal order lazy strategy, we change the evaluation rule to the following:

normal-eval(app-exp(rator, rands)) =>
    // rator is of type cexp
    // rands is of type List(cexp)
    let proc = normal-eval(rator,env)
        ;; invoke the procedure on the arguments WITHOUT evaluating them
        return normal-apply-proc(proc, rands)

The apply procedure process must be adapted to this slight change:

normal-apply-proc(proc: Closure, rands: CExp[]): Value
    if proc is a primitive:
        ;; We must evaluate all the args to apply a primitive
        let args = [normal-eval(r) for r in rands]
            return apply-primitive(proc, args)
    else // proc is a closure
        // Substitute the rands and reduce
        let subst-body = substitute params in body of proc with rands
            return normal-eval(subst-body)

Note that we do not need to turn the values back into expression before we apply the substitution in the body, since the rands are passed as non-evaluated expressions.

The code of the normal-evaluation interpreter is available in:

Normal Evaluation Example

Let us consider the normal evaluation of the same example as above:

(define square (lambda (x) (* x x)))
(define sum-of-squares (lambda (x y) (+ (square x) (square y))))
(define f (lambda (a) (sum-of-squares (+ a 1) (* a 2)))
(f 5) ;; 136

normal-eval[ (f 5) ] ==>
    normal-eval[f] ==> <Closure (a) (sum-of-squares (+ a 1) (* a 2))>
    ==>
    normal-eval[ (sum-of-squares (+ 5 1) (* 5 2)) ] ==>
        normal-eval[ sum-of-squares ] ==> <Closure (x y) (+ (square x) (square y))>
    ==>
    normal-eval[ (+ (square (+ 5 1)) (square (* 5 2))) ] ==>
        normal-eval[ + ] ==> <prim-op +>
        normal-eval[ (square (+ 5 1)) ] ==>
            normal-eval[ square ] ==> <Closure (x) (* x x)>
            ==>
            normal-eval[ (* (+ 5 1) (+ 5 1)) ] ==>
            normal-eval[ * ] ==> <prim-op *>
            normal-eval[ (+ 5 1) ] ==>
                normal-eval[ + ] ==> <prim-op +>
                normal-eval[ 5 ] ==> 5
                normal-eval[ 1 ] ==> 1
            ==> 6
            normal-eval[ (+ 5 1) ] ==>
                normal-eval[ + ] ==> <prim-op +>
                normal-eval[ 5 ] ==> 5
                normal-eval[ 1 ] ==> 1
            ==> 6
        ==> 36
        normal-eval[ (square (* 5 2)) ] ==>
            normal-eval[ square ] ==> <Closure (x) (* x x)>
            ==>
            normal-eval[ (* (* 5 2) (* 5 2)) ] ==>
            normal-eval[ * ] ==> <prim-op *>
            normal-eval[ (* 5 2) ] ==>
                normal-eval[ * ] ==> <prim-op *>
                normal-eval[ 5 ] ==> 5
                normal-eval[ 2 ] ==> 2
            ==> 10
            normal-eval[ (* 5 2) ] ==>
                normal-eval[ * ] ==> <prim-op *>
                normal-eval[ 5 ] ==> 5
                normal-eval[ 2 ] ==> 2
            ==> 10
        ==> 100
    ==> 136

Observe how the same computations are repeated in the normal evaluation algorithm, while they were processed only once in applicative order: for example (* 5 2) when it is passed to the function square is not computed before the substitution into the body of square - which leads to the computation of (* (* 5 2) (* 5 2)) in normal order instead of (* 10 10) in applicative order.

Normal Order Parameter Passing Mode: Call by Name

The normal order strategy of passing arguments to procedures without pre-computing them is called call by name - as opposed to the call by value defined by applicative-eval.

Normal-order evaluation is also called lazy evaluation because it delays the evaluation of arguments to the last moment when it is needed.

Comparison Applicative Order vs. Normal Order Evaluation

Normal order and applicative order are different algorithms applied to expressions in order to compute their value. Do they compute the same values?

The Church Rosser Theorem is a fundamental result in lambda calculus which states that: when applying reduction rules to terms in the lambda calculus, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions. Lecture Notes on the Lambda Calculus (Selinger, 2013) provides a readable formal proof of this theorem (Read up to Section 4.4, p.36).

In the context of the substitution model of the operational semantics of our language which is a variant of Lambda Calculus rewriting, the Church Rosser theorem leads to the following statement:

If both applicative-eval and normal-eval terminate (compute a value without an infinite loop and without exceptions), then they compute the same value.

More precisely, the differences between applicative-eval and normal-eval are:

If both orders terminate (no infinite loop and no exception): They compute the same value.
Normal order evaluation may repeat computations which applicative-eval does not.
Whenever applicative order evaluation terminates, normal order terminates as well.
There are expressions where normal order evaluation terminates, while applicative order does not
Side effects (like printing) are executed in different ways by applicative-eval and normal-eval - this fact can be used to identify the evaluation order of an interpreter. In applicative order, side-effects included in parameters will be executed only once before the reduction step; in normal order, these side-effects can be executed 0 to many times - depending on the logic of the execution, and in different orders than what is executed in applicative-order.

Different behavior on loops

Consider the example:

(L3
    (define loop (lambda (x) (loop x)))
    (define g (lambda (x) 5))
    (g (loop 0)))

In normal order, the application (loop 0) is not evaluated. In applicative order: the call (g (loop 0)) enters into an infinite loop.

Different behavior on exceptions

Consider the example:

(L3 
    (define try 
        (lambda (a b) 
            (if (= a 0)
                1
                b)))
    (try 0 (/ 1 0)))

In normal order, this program returns 1. In applicative order, it throws a divide by 0 exception.

Different behavior on side effects

Consider, for example,

(L3
    (define f (lambda (x) (display x) (newline) (+ x 1)))
    (define g (lambda (x) 5))
    (g (f 0)))

With applicative-eval, this program prints 0 then returns 5. In contrast, in normal-eval, this program returns 5 without printing anything.

Summary

Applicative Eval Algorithm

The definition of the evaluation rule for if-expressions relies is a special evaluation rule: only 2 of the 3 components of the if-expression are evaluated; In order to determine whether the value of the condition is true for the test, a function true-value? determines which values are considered true in the language. This part of the semantic specification of the language changes from language to language (compare Scheme and JavaScript for example).
The evaluation rule for lambda-expressions (procedures) is also a special form. None of the 2 components of the form are evaluated. Instead, they are packaged as-is into a new value type called a closure. No computation is performed at closure-creation time. Instead, the body of the closure will be evaluated when the closure is applied to actual parameters.
The key complexity of supporting user-defined procedures holds in the definition of the apply-procedure process. We defined the process of call by value - also called applicative eval: arguments to a procedure are first recursively evaluated; then the values are passed to the procedure.
To apply a closure value to values, we defined the substitution operation which replaces all free occurrences of variables with simple expressions (number, boolean, lambda or literal expressions).
To avoid capturing free variables by error, we apply a substitution to the body of a closure only after all bound variables in the body have been consistently renamed.

Substitution

Substitute is an operation which replaces free occurrences of variable references in an expression by other expressions.
A substitution \(s\) is a mapping from a finite set of variables to a finite set of expressions.
A substitution \(s\) can be applied to an expression \(E\) to produce a new expression \(E' = E \circ s\). values.
Substitution is performed in two steps:
- Consistent renaming of the expression \(E\) and the expressions in \(s\).
- Simultaneous replacement of all free occurrences of the variables of \(s\) in the renamed \(E\) by the corresponding renamed expressions of \(s\).
2 substitutions \(s\) and \(s'\) can be composed into a new substitution \(s'' = s \circ s'\) such that for all expression \(E\), \(E \circ s'' = [E \circ s] \circ s'\).

Supporting Compound Values

To support compound values, like lists and pairs, in the language, we introduce:
- new primitives (cons, car, cdr, pair?, list?)
- a new syntactic form to support literal symbols and compound expressions (introduced by the quote operator in Scheme) and the special empty-list value
- and new Value types for empty-list and SExpressions.
The evaluation rule for literal-expressions (quote <val>) (also written in Scheme as '<val>) is to return the corresponding value <val>.

Normal Evaluation

applicative-eval implements an eager approach to evaluation: arguments are evaluated immediately, before the procedure is reduced.
normal-eval implements a lazy approach to evaluation: it avoids evaluating arguments until the last moment it is necessary:
- When we need to decide a computation branch.
- When we need to apply a primitive procedure.
The only difference between normal-eval and applicative-eval is the handling of parameters in apply-procedure:
- In applicative-eval, we first evaluate the parameters, then substitute, then reduce.
- In normal-eval, we substitute the parameters non-evaluated, then reduce.
Mathematical results in \(\lambda-calculus\) demonstrate that:
- If an expression can be reduced to a value (that is, the program returns a value without entering in loops or throwing exceptions), the normal-eval algorithm will return this value.
- In some cases, applicative-eval may enter in a loop or throw exceptions in cases where normal-eval would find the value.
- If applicative-eval returns a value, it is the same one as that returned by normal-eval.
Usually, applicative-eval is more efficient than normal eval, as it executes sub-expressions less times than the normal-eval.

Principles of Programming Languages

Course Website

Operational Semantics: Substitution Model for Procedure Application

PPL 2023

\(L2\) Syntax

\(L2\) Value Type

\(L2\) Evaluation Rules

Evaluation of Conditional Expressions

Evaluation of Procedure Expressions

Procedure Application

Substitute Expressions instead of Values

Substitute Only Free Variable Occurrences in the Body

Avoid Capturing Free Variables During Substitution

The Apply Procedure Summarized

Renaming and Substitution Operations

Renaming

Substitution

Composition (combination) of Substitutions

Substitution Application

Substitution Examples

Applicative Eval Examples

Example with Renaming

Parameter Passing Mode: By Value

\(L3\): Compound Values and Quoted Literal Expressions

Error Handling

Normal Order Evaluation Algorithm

Normal Evaluation Example

Normal Order Parameter Passing Mode: Call by Name

Comparison Applicative Order vs. Normal Order Evaluation

Different behavior on loops

Different behavior on exceptions

Different behavior on side effects

Summary

Applicative Eval Algorithm

Substitution

Supporting Compound Values

Normal Evaluation