1

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

  1. 你能证明急切和懒惰的政权总是会产生相同的答案吗？（Shriram 要求查看他开发的语言，但还有其他方法可以证明这一点以及如何证明吗？）

  2. 急切的评估总是会随着更少的步骤而减少吗？

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

2 回答 2

3

  1. 您没有提供足够的信息，但如果 Shriram 提供了小步语义，那么您可能正在通过对步数的强归纳来寻找证明，而您想要的证明技术可能是双模拟。

  2. 至于渴望与懒惰，哪一个能够进行更多不必要的计算？哪一个设置了额外计算的上限？

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

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

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

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

于 2009-08-07T16:26:55.257 回答
1

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

于 2009-08-11T16:40:00.820 回答