Some more Problems to Study By (CMSC 631)

1)  LISP and Meta-Circularity

remember the "ev" (eval) function we wrote in class:

(defun ev (e env)
   (cond (((eq e 'NIL) NIL)
          ((eq e "T) t)
          ((numberp e) e)
          ((atom e) (lookup e env))
	  ((eq (first e) 'QUOTE) (second e))
          ((eq (first e) 'IF) (ev-if (second e) (third e) (fourth e) env))
	  ((eq (first e) 'LAMBDA) (list 'CLOSURE e env))
          (t (ev-apply (first e) (ev_list (cdr e) env) env)))))


a)  Change the general application from call-by-value to call-by-name.

b)  Change the if to be call-by-value (instead of call-by-name).

c)  Extend the language definition to include "LET"

         (LET (v E) expr)  (like "let val v=E in expr end" in ML)
    
    and extend the ev function to take care of it.

2) Typed Lambda Calculus

a) What are the types of the following:

   i)  \f a b. (f [l=a], f [r=b])

   ii) \f p g. (g [l= (f (fst p))])

   iii) \f:!P. \x:P. f x


b) Write functions of the following types:

   i) 'a -> 'b -> 'c -> ('a + 'b + 'c)

   ii) (!P * !Q) -> !(P + Q) 

   iii) !(P + !P) -> !!P



3)  Hoare Logic

a)  {M>=0}  X:=0; N:=1; while N<=M do begin X:=X+N; N:=N+1; end: 
                                   {X = M*(M+1) DIV 2 }


b)  {X=x ^ Y=y}
    S:=0;
    while ~(X=0) do
       begin 
         while ~(odd X) do
           begin Y:=2*Y; X:=X DIV 2 end;
         S:=S+Y;
         X:=X-1;
       end;
     {S = x*y }