Language Evaluation question: Eager Vs. Lazy

Question

I was reading Shriram's PLAI and this I got stuck in these questions:

1. Can you prove that the eager and lazy regimes will always produce the same answer? (Shriram asks to look at the language he developed but is there another way to prove this and how?)

2. Will eager evaluation always reduce with fewer steps?

Here is the Code of Substitution and Eager Evaluation in Clojure.

;; Gets W-lang and returns the computed number
;; (evaluate (let x (num 10) (let y x x)) -> 10
;; (evaluate (let x (num 10) (let y (add x (num 10)) y)) ->20
;; (evaluate (let x 10 (let x x x ))) -> 10
;; (evaluate (let x 10 (let x (+ 10 x) 
;;                            (let y (let y (+ 10 x) y)
;;                                   (+ x y))))-> 50

(defn evaluate[W-lang]
  (condp = (first W-lang)
    'num (second W-lang)
    'add (+ (evaluate (second W-lang))
         (evaluate (third W-lang)))
    'sub (- (evaluate (second W-lang))
         (evaluate (third W-lang)))
    'let (evaluate (subst (second W-lang)(third W-lang) 
                          (forth W-lang)))))


;; subst: symbol value W-Lang -> W-lang
;; substitutes the symbol and returns a W-Lang
(defn subst[id value W-lang]
    (cond
      (symbol? W-lang) (if (= id W-lang) value W-lang)
      (seq? W-lang)
      (condp = (first W-lang)
      'num (list 'num (first (rest W-lang)))
      'add (list 'add (subst id value (second W-lang))
                      (subst id value (third W-lang)))
      'sub (list 'sub (subst id value (second W-lang))
                      (subst id value (third W-lang)))
      'let 
      (if (= (second W-lang) id)
        (list 'let (second W-lang) 
                    (subst id value (third W-lang))
                    (forth W-lang))
       (list 'let(second W-lang)
                   (subst id value (third W-lang))
              (subst id value (forth W-lang))))
      W-lang)))

Answer 1

1. You haven't provided enough information, but if Shriram provides a small-step semantics, you're probably looking for a proof by strong induction over the number of steps, and the proof technique you want is probably bisimulation.

2. As for eager versus lazy, which one is capable of more unnecessary computation? Which one puts an upper bound on additional computation?

I had a look at Shriram's latest draft, and he doesn't really hit semantics until chapter 23, and then it's only big-step semantics. I couldn't find where he might show you the techniques you need to answer the questions, unless maybe he has it in mind for you to write interpreters that count reductions.

If you want proofs, I don't think Shriram's book is the right place to learn proof technique for programming languages. Glynn Winskel's book on the formal semantics of programming languages is quite good, but it's fairly advanced. Unless you're mathematically sophisticated, it will be difficult without a teacher.

You're probably better off skipping the proof parts of Shriram's stuff, or trying a more user-friendly textbook like Benjamin Pierce's Types and Programming Languages.

---

Disclaimer: I have written a programming-languages textbook, but as it remains unavailable (I can't seem to finish chapter 8 and get a draft to a publisher), it probably shouldn't be viewed as competition. But one day it will be :-)

Answer 2

I have not read the book in answer to the second question I would say: no, eager evaluation does not always result in fewer reductions. With lazy evaluation you may very well avoid having to do some computation.