CSU660 Scheme Evaluation Rules

These are rules for evaluating Scheme using the substitution model. There are separate rules for every kind of Scheme expression we want to handle.

There are certain notational conventions to be aware of:

• Fixed-width font is used for Scheme code.
• Scheme code often contains meta names which stand for some other Scheme code, a different font is used for them.
• For the meta names, we use different letters for things that stand for different types of Scheme code:
  • E₁, E₂, ..., E_n: expressions
  • x₁, x₂, ..., x_n: identifiers
  • v₁, v₂, ..., v_n: values

Note that in DrScheme you can switch to one of the “Student” languages and use the stepper to see these rules in action.

The rules follow, divided into groups.

These rules cover basic Scheme forms that are not special forms.

Eval_prim

Primitive value expressions have their obvious values. To evaluate such an expression, you simply take its value. These include:

• Numbers and strings.
• Primitive operators and functions such as +, - and sin having function values that are given as built-ins (primitive functions aren't actually symbols, but we use the same symbol is used for the name and for its value).
• Lambda expressions are also values.

(Usually primitive values are obvious, so this rule is used implicitly.)

Eval_var

Identifiers denote bindings and are implemented as symbols. To evaluate an expression x which is an identifier, you return this identifier's value which should be a value that you know by the Eval_def rule below. Note that (a) this does not involve further evaluation, and (b) it applies only for global identifiers since local ones are substituted away.

Eval_ap

To evaluate a compound form (E₁ E₂ ... E_n), which is not a special form (see below), you evaluate each of its sub-expressions recursively, getting a list of values (v₁ v₂ ... v_n). Then continue with one of the Apply_• rules to apply the function v₁ on the arguments v₂, ...v_n. This rule is the default that is used only when the expression is not one of the special form cases,so its place should be at the end of the Eval_• rules, but it is here for clarity.

These are the two application rules. Note that these rules deal with evaluated inputs.

Apply_prim

To apply a primitive function f on arguments v₁, v₂, ..., v_n, you simply compute the function result. This uses knowledge about the function which is taken as built-in — it is not part of these rules.
Example:

(+ 3 4) Applyprim⇒ 7 (car (cons v1 v2)) Applyprim+Applyprim⇒ v1 ; after two usages

Apply_lam

To apply a lambda expression (lambda (x₁...x_n) E) on some given value arguments v₁, v₂, ..., v_n, you substitute the values for the argument names in the body of the lambda expression: E[v₁, v₂, ..., v_n/x₁, x₂, ..., x_n]. In other words, you substitute every free occurrence of x_i in E by the corresponding v_i value.
You then (recursively) continue the evaluation process with the result.
Examples:

((lambda (x y) (+ x y)) 3 4) Applylam⇒ (+ 3 4) Applyprim⇒ 7 ((lambda (x) (lambda (y) (+ x y))) 3) Applylam⇒ (lambda (y) (+ 3 y))

The rest are special-form rules. Here we have only two basic rules, and then later a few rules for derived expressions.

Eval_def

To evaluate a simple define expression (define x E) where x is an identifier, you evaluate E recursively to get a value v, and you mark to yourself that now you now know that the value associated with the identifier x is v. By “know” we mean some way that can be used in the Eval_var rules above. Important: this rule can only be applied to top-level expressions.

Eval_if

To evaluate an if form (if E₁ E₂ E₃), you recursively evaluate E₁ to get a value v₁. If v₁ is true (anything other than #f), then continue by evaluating (and returning the value of) E₂, and if v₁ is #f, then continue with E₃.

Finally, these forms are all derived forms, they are evaluated by rewrite rules which transform them into a different form (eventually to a form that uses only primitives).

Eval_fdef

To evaluate a define expression that is a syntactic sugar for a function definition, (define (x₁ x₂ ... x_n) E), you continue by evaluating the form (define x₁ (lambda (x₂ ... x_n) E)).

Eval_let

A let form is evaluated by this rewrite rule:

(let ([x₁ E₁] ... [x_n E_n]) E) ⇒ ((lambda (x₁ ... x_n) E) E₁ ... E_n)

Essentially, what you get is to evaluate E with x_i bound to the result of evaluating E_i. For this reason, it is ok to skip the rewritten form and use this rule together with the Apply_lam rule. For example, instead of writing:

(let ([x 1] [y 2]) (+ x y)) Evallet⇒ ((lambda (x y) (+ x y)) 1 2) Applylam⇒ (+ 1 2)

you can write:

(let ([x 1] [y 2]) (+ x y)) Evallet+Applylam⇒ (+ 1 2)

But keep in mind that in both of these cases you should evaluate the expressions 1 and 2 before you do the substitutions. Also, note that the translation step makes things more verbose but using it makes it harder to make a mistakes, for example, it is clear that if you replace the 2 in the original expression by x, then this x is a free (unbound) identifier.

Eval_let*

This rewrite rule has two cases for a let* form with either zero or more bindings:

• (let* ([x₁ E₁] [x₂ E₂] ... [x_n E_n]) E) ⇒ (let ([x₁ E₁]) (let* ([x₂ E₂] ... [x_n E_n]) E))
• (let* () E) ⇒ (let () E)

Again, you can use your intuition here, and bind the names, keeping in mind that you do it one by one — and you can combine this rewrite with the Eval_let and even combine that further with the Apply_lam rule. For example, instead of:

(let* ([x 1] [y x]) (+ x y)) Evallet*⇒ (let ([x 1]) (let* ([y x]) (+ x y))) Evallet⇒ ((lambda (x) (let* ([y x]) (+ x y))) 1) Applylam⇒ (let* ([y 1]) (+ 1 y)) Evallet*⇒ (let ([y 1]) (let* () (+ 1 y))) Evallet⇒ ((lambda (y) (let* () (+ 1 y))) 1) Applylam⇒ (let* () (+ 1 1)) Evallet*⇒ (let () (+ 1 1)) Evallet⇒ ((lambda () (+ 1 1))) Applylam⇒ (+ 1 1) Applyprim⇒ 2

you can write:

(let* ([x 1] [y x]) (+ x y)) Evallet*+Evallet+Applylam⇒ (let* ([y 1]) (+ 1 y)) Evallet*+Evallet+Applylam⇒ (let* () (+ 1 1)) Evallet*+Evallet+Applylam⇒ (+ 1 1) Applyprim⇒ 2

The same notes as above hold here.

Eval_cond

Again, a rewrite rule with several cases:

• (cond [E_1,1 E_1,2] [E_2,1 E_2,2] ... [E_n,1 E_n,2]) ⇒ (if E_1,1 E_1,2 (cond [E_2,1 E_2,2] ... [E_n,1 E_n,2]))
• (cond [E_1,1 E_1,2]) ⇒ (if E_1,1 E_1,2 #f)
• (cond [else E]) ⇒ E

Note that this makes cond return false when no conditions match and no else clause is given — this is different from “real” Scheme, but we use this due to the lack of undefined values and errors (our if form must have two sides).

Eval_and

• (and) ⇒ #t
• (and E) ⇒ E
• (and E₁ E₂ ... E_n) ⇒ (if E₁ (and E₂ ... E_n) #f)

Eval_or

• (or) ⇒ #f
• (or E) ⇒ E
• (or E₁ E₂ ... E_n) ⇒ (let ([x₁ E₁]) (if x₁ x₁ (or E₂ ... E_n)))

Note the need for a let in the last case.