语言评估问题：渴望与。懒惰的答案

【问题标题】：Language Evaluation question: Eager Vs. Lazy语言评估问题：渴望与。懒惰的
【发布时间】：2010-11-17 18:09:15
【问题描述】：

我正在阅读 Shriram 的 PLAI，但我陷入了以下问题：

你能证明急切和懒惰的政权总是会产生相同的答案吗？（Shriram 要求查看他开发的语言，但是否有其他方法可以证明这一点以及如何证明？）
Eager evaluation 总是会随着步骤的减少而减少吗？

这是 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)))

【问题讨论】：

标签： language-agnostic functional-programming clojure scheme language-theory

【解决方案1】：

您没有提供足够的信息，但是如果 Shriram 提供了小步语义，那么您可能正在寻找通过对步数的强归纳的证明，而您想要的证明技术可能是双模拟.
对于急切和懒惰，哪一个能够进行更多不必要的计算？哪一个设置了额外计算的上限？

我看了 Shriram 的最新草稿，他直到第 23 章才真正触及语义，然后只是大步语义。我找不到他可以在哪里向您展示回答问题所需的技巧，除非他可能想让您编写计算减少的解释器。

如果您想要证明，我认为 Shriram 的书不是学习编程语言证明技术的合适场所。 Glynn Winskel 关于编程语言的形式语义的书相当不错，但它相当先进。除非你在数学上很复杂，否则没有老师会很困难。

您可能最好跳过 Shriram 的证明部分，或者尝试像 Benjamin Pierce 的 Types and Programming Languages 这样对用户更友好的教科书。

免责声明：我已经编写了一本编程语言教科书，但由于它仍然不可用（我似乎无法完成第 8 章并将草稿提交给出版商），它可能不应该被视为竞争。但总有一天会是:-)

【讨论】：

我不知道你在回答中说了什么：)..我是一个完整的新手。如果您需要更多信息，请告诉我。我也添加了我的代码。您能否提供一些关于“小步语义”和“双模拟”的信息/外部链接？

【解决方案2】：

我没有读过这本书来回答我要说的第二个问题：不，急切的评估并不总是导致减少的减少。通过惰性求值，您可以很好地避免进行一些计算。

【讨论】：