语言评估问题：Eager Vs. 懒惰的
我正在读 Shriram 的 PLAI，我陷入了这些问题：
你能证明急切和懒惰的政权总是会产生相同的答案吗？ （Shriram 要求查看他开发的语言，但是否有另一种方法来证明这一点以及如何证明？）
急切求值总是会以更少的步骤减少吗？
这是 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)))
I was reading Shriram's PLAI and this I got stuck in these questions:
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?)
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)))
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
您还没有提供足够的信息，但是如果 Shriram 提供了小步语义，您可能正在寻找通过步骤数强归纳的证明，而您想要的证明技术可能是互模拟。
至于 eager 与 lazy，哪一个能够进行更多不必要的计算？ 哪一个对额外计算设置了上限？
我看了 Shriram 的最新草稿，他直到第 23 章才真正触及语义，然后只是大步语义。 我找不到他可以在哪里向您展示回答问题所需的技巧，除非他可能想让您编写计算减少的解释器。
如果你想要证明，我认为 Shriram 的书不是学习编程语言证明技术的合适地方。 Glynn Winskel 关于编程语言的形式语义的书相当不错，但相当先进。 除非你精通数学，否则如果没有老师，这将是困难的。
您最好跳过 Shriram 的内容的证明部分，或者尝试使用更加用户友好的教科书，例如 Benjamin Pierce 的类型和编程语言。
免责声明：我已经写了一本编程语言教科书，但由于它仍然不可用（我似乎无法完成第 8 章并向出版商获取草稿），因此它可能不应该被视为竞争。 但有一天它会是:-)
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.
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 :-)
我还没有读过这本书，在回答第二个问题时我会说：不，热切的评估并不总是导致更少的减少。 通过惰性求值，您可以很好地避免进行一些计算。
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.