[racket] Q. about 'nostops' in MTWT paper

I’m reading through MTWT for the nth time, and this time I have a question about the ‘nostops’ metafunction, part of local expansion.

Specifically: ‘nostops’ takes an environment xi, and strips out everything bound to 'STOP’. This prevents the ’STOP’s from an enclosing local expand from being in force in this one.  However, it seems to me that the ’nostops’ metafunction should restore the bindings that were in place before they were mapped to STOP. More specifically; suppose a local-expand specifies, say, ‘lambda’ as a STOP. This replaces the mapping from ‘lambda’ to FUN with a mapping from ‘lambda’ to ’STOP’. Then, a nested local-expand uses a different stop-list, that doesn’t include ‘lambda’. If I’m reading the paper correctly, this local expansion would then take place in a ‘xi’ where there was no binding for lambda at *all*, which would presumably lead to an error during that expansion.

I checked out the model, to see if this was a typesetting issue, but it seems pretty clear to me that the model linked to by the paper has exactly this property; it’s simply filtering the ‘xi’ environment to throw out things that were bound to STOP.

I tried to construct a racket program to illustrate my question, and here’s what I came up with:

#lang racket

(let-syntax ([boring (lambda (stx) (cadr (syntax->list stx)))])
  
  (let-syntax ([a (lambda (stx)
                    (local-expand (cadr (syntax->list stx))
                                  'expression
                                  (list #'boring)))])
    (let-syntax ([b (lambda (stx)
                      (local-expand (cadr (syntax->list stx))
                                    'expression
                                    (list)))])
      (a (b (boring 34))))))

Unsurprisingly, this evaluated to the “correct” value, 34.  This means that either the model doesn’t match Racket, or (more likely) I’m misunderstanding the model. Or possibl

Ah, what the heck; I’ll cc: the whole racket list. I’ll take help wherever I can get it :).

John