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

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

1 голос
/ 07 августа 2009

Я читал 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 ]

3 голосов
/ 07 августа 2009

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

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

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

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

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

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

1 голос
/ 11 августа 2009

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

...