▼Fall 2021:
Programming Languages
►Capstone
On this page:
1 Conditionals
2 Syntactic Sugar
3 Reverse It
    ← prev  up  next → 

Capstone

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

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)

 

(define-language SMoLest

  ; an expression

  [e ::=

     ; variable

     x

     ; value

     v

     ; addition

     (+ e ...)

     ; application

     (e e ...)

     ; lamda

     (lambda (x ...) e)]

 

  ; values

  [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]

 

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

 

; extend the environment with bindings to values

(define-metafunction SMoLest

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

  [(extend ((x any) ...) (x_1 ...) (any_1 ...))

   ((x_1 any_1) ... (x any) ...)])

 

; 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 : ((any_k any_v) ...) any_n -> any

  [(lookup ((any_k any_v) ...) any_n)

   ,(letrec ([maybe-v (assoc (term any_n) (term ((any_k any_v) ...)))])

      (if maybe-v

          (last maybe-v)

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

 

; an example of lookup

(test-equal

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

 1)

 

; `eval` reduction relation

(define eval

  (reduction-relation

   SMoLest

   #:domain (e σ)

   ; +

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

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

   ; lookup

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

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

   ; lambda

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

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

   ; application

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

        [(in-hole C e) (extend σ (x ...) (v ...))])

   ))

 

; example of evaluating +

(test-->> eval

          ; note the `()`, which denotes the empty environment

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

                 ()])

          (term [10

                 ()]))

 

(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

  2. let*

  3. begin

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.

    ← prev  up  next →