Fall 99, CSE 520: Assignment 4

Distributed: Published on the web on November 9.
Due: Nov 21 (in class).
Total maximum score: 100 points.

The purpose of this assignment is to provide experience with PCF, interpretation of functional languages, and ML programming

Definition of a ML interpreter for Lazy PCF

The exercise of this assignment is to define in ML the eval function for Lazy PCF enriched with streams and with recursive definitions (see Lecture Notes 16, 17, 18 and 19). Namely, the syntax should be based on the following grammar:
   Term ::= Var| \Var.Term | Term Term         % lambda terms 
          | Num | true | false                 % numerical and boolean constants
          | Term Op Term                       % numerical ops and comparison
          | (Term,Term) | fst Term | snd Term  % pairs         
          | Term::Term                         % stream constructor
          | hd Term | tl Term                  % stream selectors
          | if Term then Term else Term        % conditional
          | let Var = Term in Term             % term with a local declaration 
          | let fun f x = Term in Term         % term with a local recursive definition 
Please define the datatype for the representation of the PCF terms above, the type environment and its operations, and the interpreter eval.

The interpreter eval should be environment-based (see Lecture Notes 18 and 19), and treat the scope correctly, i.e. it should have static scope. Please use the interepreter developed in Lecture Notes 18 and 19 (for the eager semantics) as a basis for your interpreter.

Testing the interpreter

Additionally please define
  1. A term Facts representing the PCF term
       let fun nats n = n :: nats(n+1)                        % stream of natural numbers 
        in let fun mult p = (hd (fst p) * hd (snd p)) 
                            :: mult (tl (fst p), tl (snd p))  % multiplication on streams                                   
            in let fun facts k = 1::(mult (nats 1,facts 1))   % stream of factorials
                in hd(tl(tl(tl(facts 1))))
    Note: the functions nats, mult and facts are explained in Lecture Notes 16 and 17. In those LNs, "mult" is called "times" and its definition is in ML style i.e. it uses pattern matching). The definition given here is in PCF style. Note also that the function "facts", in the LNs, is without arguments. Here we need to use a dummy argument (k) just to respect the format of the let fun construct, which wants always an argument.

  2. A term Test_static representing the PCF term
    let x = 1 
     in let fun f y = x + y
         in let x = 2 
             in f 1

Please use ML val declaration to give these definitions, i.e.

   val Facts = < ML expression of type term, representing the first PCF term above >
   val Test_static  = < ML expression of type term, representing the second PCF term above >
Note: the result of (eval Facts emptyenv) should be 6, and the result of (eval Test_static emptyenv) should be 2.

What to submit, and how

The solution of the assignment should contain the following code: Plus, any auxiliary function and type that you may find helpful to use, and comments and explanations that can help us to understand and evaluate your solution.

Please submit a hard-copy of the code by the deadline, as usual. In addition, please submit the electronic version (for testing purposes) by sending an email to herescu@cse.psu.edu by the deadline.