bound-identifier=? returns #t yet free-identifier=? returns #f

[symingz]

In version 9.5.8 of ChezScheme, the result of evaluating

(let ([x 10])
  (define sx #'x)
  (let ([x 11])
    (list    
      (free-identifier=? sx #'x)
      (bound-identifier=? sx #'x))))

at the top level is (#f #t), but according to page 304 of TSPL4 (https://scheme.com/tspl4/syntax.html#./syntax:s37), " ... identifiers that are bound-identifier=? are free-identifier=? ...". This TSPL4 assertion is consistent with the "marks and substitutions" operational model mentioned in R6RS. For the test case here, it is correct for (free-identifier=? sx #'x) to be #f, so I think (bound-identifier=? sx #'x) should be corrected to return #f.

[dybvig]

They key is in the end of the partially quoted sentence: "as long as the identifiers have valid bindings in the context where they are compared". If this were code implementing a macro transformer intending to insert references to either or both x's into its output, the references to x would not be valid. (They would be run-time references to expand-time variables.) The predicates bound-identifier=?and free-identifier=? both relate only to equivalence of identifiers appearing in the output of a transformer.

[symingz]

I'm having difficulty rationalizing this in terms of marks and substitutions. #'x between the outer let and inner let is wrapped by the substitution from the outer let, #'x in the inner let is wrapped first by the substitution from the outer let and then the substitution from the inner let. This difference in substitutions makes free-identifier=? return #f, but according to the algebra referenced by R6RS (i.e., section 2.4 of Oscar Waddell’s PhD thesis), this difference in substitutions should make bound-identifier=? return #f as well.

Also, if I change the test case to

(let ()   
  (define-syntax mx                                
    (lambda (stx)                                 
      (syntax-case stx ()                        
        [(_ v)                                  
         (let ([x 10])                         
           (with-syntax ([sx #'x])            
             (let ([x 11])                   
               (with-syntax ([ssx #'x])     
                 (printf "~a~%" (free-identifier=? #'sx #'ssx))
                 (printf "~a~%" (bound-identifier=? #'sx #'ssx))
                 #'(let ([sx 12]) (+ v ssx))))))])))
  (mx 100))

then the output is

#f
#t
112

In this case free-identifier=? and bound-identifier=? are used on identifiers that will appear in the output of a transformer.

[dybvig]

The Chez Scheme expander uses a different algebra, which is described starting at line 339 of syntax.ss. It's behavior differs from our original algebra in cases where an introduced reference would be invalid, including cases like yours where an introduced reference to either of the first or second bindings for x would result in an out-of-phase error.

[symingz]

I see. I do like the "more theoretically appealing" option better. Anyway, now I understand that this is not a bug but an explicit choice. Thanks for the explanation!