johnwcowan / r7rs-work

96 stars 12 forks source link

"Each use of a variable is associated with a lexically apparent binding of that variable" is wrong #28

Open safinaskar opened 2 years ago

safinaskar commented 2 years ago

In https://github.com/johnwcowan/r7rs-spec/blob/errata/spec/r7rs.pdf on page 5 I see: "Each use of a variable is associated with a lexically apparent binding of that variable". My interpretation of this sentence is: "It is possible to find binding (if it exists) of any used variable (i. e. to find place where the variable was introduced) merely by parsing, without need to evaluate anything". But this is not true! Consider this code:

(define-syntax dd (syntax-rules () ((dd x) (define x 0))))
(dd xx)
xx

(I tested this code on mit-scheme.)

It is not possible to find binding for variable xx merely by parsing, you need to actually expand macros dd for this. Moreover, syntax-rules are based on term rewriting, which are Turing complete! I. e. you need to evaluate Turing-complete sublanguage to find a binding!

Consider this more complex example:

(define-syntax if-add-peano (syntax-rules (succ zero)
  ((if-add-peano zero     zero     zero     a b) a)
  ((if-add-peano (succ x) zero     (succ y) a b) (if-add-peano x zero y a b))
  ((if-add-peano x        zero     y        a b) b)
  ((if-add-peano x        (succ y) z        a b) (if-add-peano (succ x) y z a b))
))
(if-add-peano (succ (succ zero)) (succ (succ zero)) (succ (succ (succ (succ zero)))) (define xxx 33) (begin))
(write xxx)

(Tested on mit-scheme.)

Here we verify that 2 + 2 = 4 using Peano arithmetic. And if so, we define xxx as 33. So, Scheme implementation should perform this complex macro expanding just to know whether xxx is defined.

So, please remove or change somehow that phrase "Each use of a variable is associated with a lexically apparent binding of that variable" and similar phrases