Вопрос об оценке языка: Eager Vs. ленивый

Я читал PLAI Ширама, и я застрял в следующих вопросах:

  1. Можете ли вы доказать, что нетерпеливые и ленивые режимы всегда будут давать один и тот же ответ? (Шрирам просит взглянуть на язык, который он разработал, но есть ли другой способ доказать это и как?)

  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)))
Источник

2 ответа

Решение

  1. Вы не предоставили достаточно информации, но если Шрирам предоставляет семантику с небольшими шагами, вы, вероятно, ищете доказательство с помощью сильной индукции по числу шагов, и вы хотите использовать метод доказательства, вероятно, бисимуляцию.

  2. Что касается нетерпеливых и ленивых, кто из них способен на более ненужные вычисления? Какой из них ставит верхнюю границу для дополнительных вычислений?

Я взглянул на последний черновик Шрирама, и он до сих пор не затронул семантику до 23-й главы, а потом это только семантика большого шага. Я не мог найти, где он мог бы показать вам методы, необходимые для ответа на вопросы, если, возможно, он не имеет в виду, чтобы вы написали переводчиков, которые считают сокращения.

Если вам нужны доказательства, я не думаю, что книга Шрирама - это то место, где нужно изучать технику доказательств для языков программирования. Книга Глинна Винскеля о формальной семантике языков программирования довольно хороша, но она довольно продвинута. Если вы не математически искушены, без учителя будет трудно.

Возможно, вам лучше пропустить проверочные части материалов Шрирама или попробовать более удобный для пользователя учебник, такой как " Типы и языки программирования" Бенджамина Пирса.

Отказ от ответственности: я написал учебник по языкам программирования, но, поскольку он по-прежнему недоступен (кажется, я не могу закончить главу 8 и передать черновик издателю), его, вероятно, не следует рассматривать как соревнование. Но однажды это будет:-)

Источник

Я не читал книгу в ответ на второй вопрос, который я бы сказал: нет, энергичная оценка не всегда приводит к меньшим сокращениям. С ленивым вычислением вы можете избежать вычислений.

Источник
Другие вопросы по тегам