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

DRAFT

Purpose: The goal of this problem set is to extend simple-lang with if statements and while loops. In addition, you will gather some experience simulating abstractions in languages.

---

Background:

The module 9-provided.rkt provides a language definition of simple-lang extended with if and while. Import everything from this file into your solution file with (require redex "9-provided.rkt").

Problem 1:

Define the language sl+cek as a minimal extension of sl+cek-without-if-while.

Define the metafunction eval-cek. It maps statements s from sl+cek to results r. Naturally the definition requires an extension of the ->CEK-without-if-whilereduction relation.

Problem 2:

The simple-lang is now a programming language that is computationally equivalent to Turing machines. When such programming languages lack some abstractions (e.g., functions or classes with methods), it is almost always possible to mimic such abstractions via code duplication and possibly a protocol. Here is a way to implement a call-by-reference function that increments its input variable by twice the right-hand side:

  ;; assign x_result to itself and twice the value of e_n
  (define-metafunction sl+cek-without-if-while
    +=2x : x e -> s
    [(+=2x x_result e_n)
     (x_result = (+ x_result (+ e_n e_n)))])

  (test-equal (term (eval-cek-without-if-while (block ((x 5)) (+=2x x 2))))
	      (term (block ((x 9)))))

By using a metafunction, you can realize code duplication without doing the work yourself.

Suggestion: The expression e_n is evaluated twice. How can you eliminate this double-evaluation?

Implement a multiplication procedure for sl+cek. That is, define a metafunction s-* that consumes a variable and two expressions that evaluate to natural numbers. It produces a statement s that stores the product of the two expressions in the given variable.

Implement a factorial procedure for sl+cek. That is, define a metafunction s-! that consumes a variable and an expression that evaluates to a natural number. It produces a statement s that stores the factorial of the expression in the given variable.

Problem 3:

One way to verify a program/function is to prove that it is equal to a function in some other language (often called a "meta" language). The imports from 9-provided.rkt include a Racket-level factorial function. Formulate a conjecture as the metafunction !=s! concerning the relationship between the simulated factorial procedure from problem 2, s-!, and the imported ! function.

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.