8 Fraud: Let Bindings and Variables🔗

8.1 Bindings and Variables🔗

Now, let us add local bindings to our language. This will allow us to declare a variable, bind a value to it, and use the variable in expressions.

(let ((id0 e0)) e1)

This form is called a let binding, that binds the identifier id0 to the value of e0 within the scope of the expression e1.

This is a simplification of Racket’s let binding form, that allows binding of multiple variables:

(let ([id0 e0] [id1 e1] ... [idn en]) em)

that allows you to declare multiple identifiers id0 through id1, binding them to values of expressions e0 through e1 respectively in the scope of the expression em.

An example program written using let bindings will look like:

This program binds the value of (add1 6) to x and sum of 6 and x to y and then calculates their sum, evaluating to 20.

We will extend our previous language Defend: Handling Errors to add let bindings, and call this new language Fraud.

8.2 Syntax🔗

We extend the concrete syntax of Defend with a few forms to support bindings. First, we add x to the language, which denotes any identifier, i.e., any string that can be represented as a symbol in Racket (alpha-numeric, and symbols like -, +, =, <, >, and similar). These can denote the name of any variable of declarations in our language: Fraud. Second, we add a (let ((x e)) e) form to the language. This allows us to declare a new variable x and bind the first expression e to it, and this x is only bound locally in the second expression e.

8.3 Substitution🔗

We are done with the syntactic part of extending the language and now move on to defining its semantics:

• the meaning of a let expression (let ((x e0)) e) is the meaning of e (the body of the let) when x means the value of e0 (the right hand side of the let),

• the meaning of a variable x depends on the context in which it is bound. It means the value of the right-hand side of the nearest enclosing let expression that binds x. If there is no such enclosing let expression, the variable is meaningless.

Let us understand these rules with a few examples:

• x: this expression is meaningless on its own.

• (let ((x 7)) x): this means 7, since the body expression, x, means 7 because the nearest enclosing binding for x is to 7, which means 7.

• (let ((x 7)) 2): this means 2 since the body expression, 2, means 2.

• (let ((x 7)) (add1 x)): this means 8 since the body expression, (add1 x), means one more than x and x means 7 because the nearest enclosing binding for x is to 7.

• (let ((x (add1 7))) x): this means 8 since the body expression, x, means 8 because the nearest enclosing binding for x is to (add1 7) which means 8.

• (let ((x 7)) (let ((y 2)) x)): this means 7 since the body expression, (let ((y 2)) x), means 2 since the body expression, x, means 7 since the nearest enclosing binding for x is to 7.

• (let ((x 7)) (let ((x 2)) x)): this means 2 since the body expression, (let ((x 2)) x), means 2 since the body expression, x, means 2 since the nearest enclosing binding for x is to 2.

• (let ((x (add1 x))) x): this is meaningless, since the right-hand side expression, (add1 x) is meaningless because x has no enclosing let that binds it.

• (let ((x 7)) (let ((x (add1 x))) x)): this means 8 because the body expression (let ((x (add1 x))) x) means 8 because the body expression, x, is bound to (add1 x) is in the nearest enclosing let expression that binds x and (add1 x) means 8 because it is one more than x where x is bound to 7 in the nearest enclosing let that binds it.

Make sure you have a good understanding of how binding works in these examples before moving on. Remember: you can always check your understanding by pasting expressions into Racket and seeing what it produces, or better yet, write examples in DrRacket and hover over identifiers to see arrows between variable bindings and their occurrences.

One thing that should be clear from these examples is that the meaning of a sub-expression is not determined by the form of that expression alone. For example, x could mean 7, or it could mean 8, or it could be meaningless, or it could mean 22, etc. It depends on the context in which it occurs. So in formulating the meaning of an expression, this context must be taken into account.

A good analogy where context matters for the meaning of an expression is algebra, where it is common to write expressions as given x = 7 + 3, find the value of expressions like 2x + 7. In such cases, you would first find the value of x to be 10 and substitute into the given expression to find it is 27. Substitution is simple for algebra, but for a programming language it is more involved.

Let us define it as a function subst that takes the expression in which the substitution will take place, what variable will be substituted, and with the value it will be substituted. Notably, our subst function computes a new expression from the in expression where all occurrences of what has been substituted by with:

The subst function keeps values as-is, as there is nothing to substitute. All the other cases, it does what we expect, recursively applies subst to all subexpressions to replace all occurrences. Only two cases are interesting, the ones for the variable x and let bindings. For the case of variables, we only substitute a variable if it has the same name as the one we are substituting. For let, if a let binding is redefining the same variable with a new expression, we only substitute it in the binding expression. We do not substitute in the body of the let, as it should be substituted with the new redefined value, when we give meaning to the redefining let. Conversely, if the let binding is for any other variable, it does not matter and we can substitute in both the binding expression and the body of the let.

8.4 Meaning of let-bindings🔗

We can given meaning to let expression by the following rule:

The above rule states, to give meaning to a let expression, we first need to give meaning to the binding expressions e1 as v1, then all we need to do is substitute all occurrences of the variable x in body of the let expression. We will use the subst function we defined earlier to denote substitution of all occurrences of x with v1 in e2 to produce a new term e3. The meaning of the entire let expression if the meaning of this substituted expression e3.

Crucially, we did not give any meaning to variables x yet. Look at the case for variables x for subst, and you will notice all occurrences of a bound variables will be substituted with their values as we give meaning to an expression. That will leave us only with programs, where we have unbound variables or free variables. For example, (add1 x) or (let ((x 5)) y) where x and y are free variables respectively. Such free variables result in an error.

8.5 Interpreter for Fraud🔗

With the formal semantics defined, we can translate that to our interpreter code trivially. First let us translate the subst definition to a program. Then we add new cases to the interpreter to reflect the above inference rules using ‘subst‘:

fraud/interp.rkt

#lang racket

(require rackunit)

(provide interp)

;; Expr -> Value

;; Interpret given expression

(define (interp e)

(match e

[(? integer?)          e]

[(? boolean?)          e]

[(? symbol?)           (error "Unbound variable:" (symbol->string e))]

; ...

; other cases omitted for brevity

[`(let ((,x ,e1)) ,e2) (interp-let x e1 e2)]

[_                     (error "Parser error!")]))

;; other definitions omitted for brevity

(define (interp-let x e1 e2)

(let ((e3 (subst e2 x (interp e1))))

(interp e3)))

(define (subst in x with)

(match in

[(? integer?)          in]

[(? boolean?)          in]

[(? symbol?)           (if (eq? in x) with in)]

[`(add1 ,e)            `(add1 ,(subst e x with))]

[`(sub1 ,e)            `(sub1 ,(subst e x with))]

[`(+ ,e1 ,e2)          `(+ ,(subst e1 x with) ,(subst e2 x with))]

[`(- ,e1 ,e2)          `(- ,(subst e1 x with) ,(subst e2 x with))]

[`(* ,e1 ,e2)          `(* ,(subst e1 x with) ,(subst e2 x with))]

[`(/ ,e1 ,e2)          `(/ ,(subst e1 x with) ,(subst e2 x with))]

[`(zero? ,e)           `(zero? ,(subst e x with))]

[`(and ,e1 ,e2)        `(and ,(subst e1 x with) ,(subst e2 x with))]

[`(<= ,e1 ,e2)         `(<=  ,(subst e1 x with) ,(subst e2 x with))]

[`(if ,e1 ,e2 ,e3)     `(if ,(subst e1 x with) ,(subst e2 x with) ,(subst e3 x with))]

[`(let ((,y ,e1)) ,e2) (if (eq? x y)

`(let ((,y ,(subst e1 x with))) ,e2)

`(let ((,y ,(subst e1 x with))) ,(subst e2 x with)))]

[_                      (error "Parser error!")]))

The above interpreter only has two new cases for variables and let directly reflecting the rules with relation. See how we are raising an error because programs with free variables have no meaning?

We can try running this on a few examples:

8.6 Testing🔗

We can write a few cases for the interpreter to see if it behaves as we would expect: