R5RS Spe c letre c пример для eqv? - PullRequest
Новая
       20

R5RS Spe c letre c пример для eqv?

0 голосов
/ 22 марта 2020

Я читаю spe c для R5RS, и у него есть два примера для eqv?

(letrec ((f (lambda () (if (eqv? f g) 'both 'f)))
         (g (lambda () (if (eqv? f g) 'both 'g))))
  (eqv? f g))
                               ;; ===>  unspecified

(letrec ((f (lambda () (if (eqv? f g) 'f 'both)))
         (g (lambda () (if (eqv? f g) 'g 'both))))
  (eqv? f g))
                               ;; ===>  #f

Я не понимаю, что это ошибка в коде, от меня это выглядит подобно тому, как они сравнивают разные функциональные объекты, они являются двумя лямбда-выражениями, означает ли это первый пример, каким образом можно вернуть true, если это не указано, из-за оптимизации? Разве это не должно быть полностью изменено? Не указано для (if (eqv? f g) 'f 'both), что обе функции возвращают один и тот же символ.

Spe c link

1 Ответ

1 голос
/ 22 марта 2020

Это удивительно тонкий пример. В первом примере: 

(letrec ((f (lambda () (if (eqv? f g) 'both 'f)))
         (g (lambda () (if (eqv? f g) 'both 'g))))
  (eqv? f g))

Ну, f и g отличаются друг от друга по тексту, верно? Так что это должно быть ложным. За исключением того, что, если мы предполагаем , что (eqv? f g) истинно - мы предполагаем, что f и g на самом деле - тогда мы могли бы оптимизировать условные выражения и переписать каждый из f и g в: 

(letrec ((f (lambda () 'both))
         (g (lambda () 'both)))
  (eqv? f g))

И теперь мы можем оптимизировать их в одну и ту же функцию, как указано в eqv?. Таким образом, предположение о том, что функции такие же, как рассмотренные eqv?, приводит нас к состоянию, в котором они могут быть оптимизированы, чтобы фактически быть эквивалентными при eqv?.

Во втором примере : 

(letrec ((f (lambda () (if (eqv? f g) 'f 'both)))
         (g (lambda () (if (eqv? f g) 'g 'both))))
  (eqv? f g))

Ну, если мы снова предположим, что f и g одинаковы, то мы можем попытаться снова оптимизировать условия: 

(letrec ((f (lambda () 'f))
         (g (lambda () 'g)))
  (eqv? f g))

И это очевидно, ложно. Таким образом, мы не можем предположить, что f и g одинаковы. И теперь у нас возникли проблемы, потому что если мы предположим, что они отличаются , то мы могли бы, возможно, оптимизировать их снова ... и теперь они имеют ту же функцию и, возможно, могут быть оптимизированы, чтобы быть такими же под eqv? ... кроме того, что сейчас мы находимся в oop. Таким образом, они должны считаться различными в eqv?, даже если они могут возвращать одно и то же значение.

Второй пример очень близок к парадоксу лжеца: он ускользает, потому что eqv? разрешено не знать что две вещи - это одно и то же (для определения «одного и того же», о котором я бы подумал сложнее), даже если они на самом деле таковы.

Личное замечание: хотя я думаю, что эти примеры чрезвычайно умный и тонкий, я бы не стал помещать их в спецификацию c, или, по крайней мере, без очень подробного объяснения того, что системе разрешено или запрещено делать и почему.

...