On this page:
5.1 PCF and Global Function Definitions
5.2 Context-sensitive Rules
5.3 Exercises
6.10.0.2

5 Modeling Functional Languages

Goals

context-sensitive modeling

the power of Redex pattern matching

5.1 PCF and Global Function Definitions

Say you want to add global, mutually recursive function definitions to PCF. Here is a simple way of extending the syntax:

(define-language PCF
  (p ::=
     (prog (f ...) e))
 
  (f ::=
     (define x (lambda (x) e)))
 
  (e ::=
     x
     (lambda (x) e)
     (e e)
 
     ; booleans
     tt
     ff
     (if e e e)
 
     ; arithmetic
     n
     (+ e e))
  (n ::=
     integer)
 
  (x ::= variable-not-otherwise-mentioned)
 
  #:binding-forms
  (lambda (x) e #:refers-to x))

Stop! When you revise a model, first get all the test cases to work again. Here you will need to change E contexts to P contexts, that is, progs with holes in the expression position.

Then. Come up with an program that gets stuck because it uses the new syntactic features.

5.2 Context-sensitive Rules

Your revised model gets stuck because the tree root of any program now have prog as its marker. We need a new kind of context.

(define-extended-language PCF-eval PCF
  (P-name ::=
          (prog (f ...) E-name))
 
  (E-name ::=
          hole
          (E-name e)
          (E-name + e)
          (if E-name e e)
          (v + E-name))
 
  (v ::=
     n
     tt
     ff
     (lambda (x) e)))

Your revised model gets stuck because expressions now have free variables. These free variables point to function definitions and show up in the hole of an E context.

Now we have two options:
  1. Use the lookup function from yesterday’s lab.

  2. Exploit Redex’s extremely powerful pattern matching.

We use option 2:
(--> (prog ((define x_1 v_1) ... (define x v) (define x_2 v_2) ...)
           (in-hole E-name x))
     (prog ((define x_1 v_1) ... (define x v) (define x_2 v_2) ...)
           (in-hole E-name v)))
The complete reduction relation is available in figure 3; figure 4 shows how to revise the eval function plus its test suite.

5.3 Exercises

Exercise 9. Check that the model works for a simple recursion function. No, you won’t get very far with the recursion we have. image

Exercise 10. Implement option 1. image

Exercise 11. Revise your call-by-value model of PCF to include global definitions. image

(define ->name
  (reduction-relation
   PCF-eval
   #:domain p
   (--> (in-hole P-name ((lambda (x) e_1) e_2))
        (in-hole P-name (substitute e_1 x e_2))
        beta-name)
   (--> (in-hole P-name (if tt e_1 e_2))
        (in-hole P-name e_1)
        if-tt)
   (--> (in-hole P-name (if ff e_1 e_2))
        (in-hole P-name e_2)
        if-ff)
   (--> (in-hole P-name (n_1 + n_2))
        (in-hole P-name ,(+ (term n_1) (term n_2)))
        plus)
   (--> (prog (d ... (defun (x x_y) e) d_2 ...)
              (in-hole E-name x))
        (prog (d ... (defun (x x_y) e) d_2 ...)
              (in-hole E-name (lambda (x_y) e))))))

Figure 3: The complete reduction relation for defun

; evaluate term e with the transitive closure of ->name
(define-metafunction PCF-eval
  eval : p -> v or (shu any)
  [(eval p)
   v_one-term
   (where ((prog (d ...) v_one-term))
          ,(apply-reduction-relation* ->name (term p)))]
  [(eval p)
   (shu
    ,(apply-reduction-relation* ->name (term p)))])
 
(define e3
  (term
   (prog ()
         ((lambda (x) (lambda (y) x))
          ((lambda (x) x) 2)))))
 
(define e4
  (term
   (prog ()
         (((lambda (x) (lambda (y) x))
           (1 + (1 + 1)))
          (2 + 2)))))
 
(define e5
  (term
   (prog ((defun (h why) (why + 1)))
         42)))
 
(define e6
  (term
   (prog ((defun (h why) (why + 1)))
         ((h 31) + 2))))
 
(test-equal (term (eval ,e6))
            34)
(test-equal (term (eval ,e5))
            42)
(test-equal (term (eval ,e3))
            (term (lambda (y) ((lambda (x) x) 2))))
(test-equal (term (eval ,e4))
            3)

Figure 4: The eval function for PCF plus defun