Due date: 11/2 @ at the beginning of class

Purpose: The goal of this problem set is to understand abstract register machines and their relationship to the standard reduction semantics (textual machine).

---

Background:

The module 8-provided.rkt specifies another (standard) semantics for the simple-lang language:

  (define ->sl-standard 
    (reduction-relation 
     sl+c
     [==> (block (d_1 ... (x n) d_2 ...) (in-hole S (+ n_1 n_2)) s_2 ...)
	  (block (d_1 ... (x n) d_2 ...) (in-hole S n_3) s_2 ...)
	  (where n_3 ,(+ (term n_1) (term n_2)))
	  "add"]
     [==> (block (d_1 ... (x n) d_2 ...) (in-hole S x) s_2 ...)
	  (block (d_1 ... (x n) d_2 ...) (in-hole S n) s_2 ...)
	  (side-condition (term (no-binding-for x S)))
	  "ref"]
     [==> (block (d_1 ... (x n_o) d_2 ...) (in-hole S (x = n_n)) s_2 ...)
	  (block (d_1 ... (x n_n) d_2 ...) (in-hole S void) s_2 ...)
	  (side-condition (term (no-binding-for x S)))
	  "set"]
     [==> (block ((x n) ...) void s ...) (block ((x n) ...) s ...) "void"]
     [==> (in-hole S (block ((x_1 n_1) ...))) 
	  (in-hole S void)
	  (side-condition (not (equal? (term S) (term hole))))
	  "pop"]
     with 
     [(--> (in-hole S s_red) (in-hole S s_con))
      (==> s_red s_con)]))

In contrast to the original semantics, this one implements a stack-based evaluation; inner blocks are "pushed" and, once their statement sequence is worked off, "popped".

You must require the file into your homework solution.

Problem 1:

Design a CEK-reduction relation that corresponds to the above standard reduction relation. Here are specifications of the machine states and their components:

  (define-extended-language sl+cek sl+c
    (CEK (s (D ...) (S ...))) ;; states 
    (FIN ??? ??? ???)         ;; final states
    (D (d ...))               ;; environments (declaration stack)
    (S (s ...)))              ;; continuations (control stack)
 

As you can see, a machine state consists of

1. the current statement, which corresponds to the statement in the hole of the evaluation context;
2. the environment, which collects the declarations that surround the hole in the evaluation context; and
3. the continuation, which collects the statements to be executed after the current one is evaluated.

Your design must include a precise specification of the set of final states and a eval-cek function.

Like the original CEK machine, the CEK machine for simple-lang must implement search instructions that find the next assignment statement through the nest of blocks. Help Consider deriving your CEK machine in a step-by-step fashion, following the text book's strategy in the chapter on abstract register machines for ISWIM. If you follow this path, do not turn in any intermediate steps.

Explanation Your CEK machine must use evaluation context to evaluate expressions. A full-fledged machine would use an expression stack and an expression continuation. Once you understand the basic idea, there is no need to spell out these details too.

Problem 2:

Formulate and test a conjecture concerning eval-cek and eval-s.

Deliverable:

Send in a single Racket file. Its name should consist of the two last names in alphabetical order separated with a hyphen; its suffix must be .rkt.

Your file must start with the following two lines:

  ;; NameOfPartner1, NameOfPartner2 
  ;; email@of.partner1.com, email@of.partner2.com

appropriately instantiated of course. Also separate problems with lines of the shape ";; " followed by 77 "-". That gives you a width of 80 chars. Try to stick to this width for all of your code; it ensures basic readability.