▼Fall 2024:
Programming Languages
►Capstone
On this page:
1 Conditionals
2 Syntactic Sugar
3 Reverse It
    contents    up   

Capstone🔗

The following is if are interested in getting capstone credit for the course.

The capstone option is only available to those who do the course for letter-grade credit.

You will have to learn (on your own) the Redex system. Redex is a language/library built atop Racket for defining programming languages formally (i.e., giving them a formal semantics).

Redex should look especially familiar if you have taken or are taking courses like Logic for Systems or Formal Proof and Verification. It resembles the Alloy, Forge, and Lean systems you may have seen in those courses. It behaves more like Alloy or Forge, in that it supports finite executions of specifications, rather than deductive proof à la Lean. However, familiarity with those systems, while helpful, is not essential.

Start with this Redex specification:

#lang racket

(require redex)

 

#|

You must keep all existing kinds of expressions,

but you are welcome to add new kinds, such as `eq?`.

You must keep the `run` tests unchanged.

 

You are welcome to change everything else.

|#

 

(define-language SMoLest

  ; expression

  [e ::=

     ; variable

     x

     ; value

     v

     ; addition

     (+ e ...)

     ; application

     (e e ...)

     ; lambda

     (lambda (x ...) e)]

  ; value

  [v ::=

     number

     (lambda (x ...) e σ)]

  ; environment

  [σ ::= ((x v) ...)]

  ; evaluation context

  ; used in `eval`

  ; these are the compound forms of `e`

  ; with one sub expression replaced by a hole, `C`.

  [C ::=

     (v ... C e ...)

     (+ v ... C e ...)

     hole]

  ; stack

  [s ::=

     ()

     (C σ s)]

  ; variable

  [x ::= variable-not-otherwise-mentioned])

 

; extend the environment with bindings to values

(define-metafunction SMoLest

  extend : ((x v) ...)  (x ...) (v ...) -> ((x v) ...)

  [(extend ((x_1 v_1) ...) (x_2 ...) (v_2 ...))

   ((x_2 v_2) ... (x_1 v_1) ...)])

 

; an example of extend

(test-equal

 (term (extend ((a 1)) (b c) (2 3)))

 (term ((b 2) (c 3) (a 1))))

 

; lookup a value in the environment

(define-metafunction SMoLest

  lookup : σ x -> v

  [(lookup σ x)

   ,(letrec ([maybe-v (assoc (term x) (term σ))])

      (if maybe-v

          (last maybe-v)

          (error 'unbound "~e" (term x))))])

 

; an example of lookup

(test-equal

 (term (lookup ((a 1)) a))

 1)

 

; `eval` reduction relation

(define eval

  (reduction-relation

   SMoLest

   #:domain [e σ s]

   ; +

   (--> [(in-hole C (+ number ...)) σ s]

        [(in-hole C ,(apply + (term (number ...)))) σ s])

   ; variable

   (--> [(in-hole C x) σ s]

        [(in-hole C (lookup σ x)) σ s])

   ; lambda

   (--> [(in-hole C (lambda (x ...) e)) σ s]

        [(in-hole C (lambda (x ...) e σ)) σ s])

   ; application

   (--> [(in-hole C ((lambda (x ...) e σ_1) v ...)) σ_2 s]

        [e (extend σ_1 (x ...) (v ...)) (C σ_2 s)])

   ; return

   (--> [v σ_1 (C σ_2 s)]

        [(in-hole C v) σ_2 s])

   ))

 

; an example of evaluating +

(test-->> eval

          ; The first `()` denotes the empty environment

          ; The second `()` denotes the empty stack

          (term [(+ (+ 1 2) (+ 3 4))

                 ()

                 ()])

          (term [10

                 ()

                 ()]))

 

; HINT: try run the following expression in the REPL.

;   You might find `stepper` a very useful debugger

#;

(stepper eval

         ; The first `()` denotes the empty environment

         ; The second `()` denotes the empty stack

         (term [(+ (+ 1 2) (+ 3 4))

                ()

                ()]))

 

; HINT: You can also test your implementation with `run`

(define (run e)

  (define results (apply-reduction-relation* eval (term [,e () ()])))

  (if ((redex-match? SMoLest ((v σ s))) results)

      (first (first results))

      (error 'run "For details, run\n(stepper eval (term [~a () ()]))" e)))

 

(test-equal (run (term (+ (+ 1 2) (+ 3 4))))

            (term 10))

(test-equal (run (term (((lambda (x) (lambda (y) (+ x y))) 2) 3)))

            (term 5))

(test-equal (run (term ((lambda (x) (+ ((lambda (x) x) 3) x)) 1)))

            (term 4))

 

(test-results)

Now make the following changes/extensions.

1 Conditionals🔗

Modify the SMoLest language definition and eval to add booleans and an eq? predicate (reference equality)—you may find + to be useful inspiration. Then, add a ternary if expression.

2 Syntactic Sugar🔗

Use define-metafunction to add the following constructs:

  1. (let ([x e] ...) e)

  2. (let* ([x e] ...) e)

  3. (begin e ... e)

You do not need to modify the language definition of SMoLest. Introduce a metafunction for each of the above forms. For instance, you might implement an and sugar like this:

(define-metafunction SMoLest

  and : (e ...) -> e

  [(and e_0)

   e_0]

  [(and e_0 e_1 e_n ...)

   (if e_0 (and e_1 e_n ...) #false)])

Then write tests to ensure that each of your sugars work; e.g., for lambda:

(test-equal

 (term (let ((a 1)) (+ a 2)))

 (term ((lambda (a) (+ a 2)) 1)))

 

(test-->> eval

          (term [(let ((a 1)) (+ a 2)) ()])

          (term [3 ((a 1))]))

For implementing let*, you will find your let sugar to be helpful. For implementing begin, you may find your let* sugar and the variable-not-in procedure to be helpful.

3 Reverse It🔗

Finally, modifying only the language definition of SMoLest, reverse the evaluation order of function arguments from left-to-right to right-to-left.

    contents    up