> The dynamic extent of an expression is the sequence of evaluation steps during which the expression contains the redex.

(from https://docs.racket-lang.org/reference/eval-model.html#%28part._cont-model%29)

Should this actually be:

> The dynamic extent of an expression is the sequence of evaluation steps during which the expression contains some redex.

?

No, “the redex” means “the redex in the evaluation step”

…and “the redex” is unambiguous for a given expression because of Racket’s well-defined evaluation order (e.g. in (- (+ x 1) (* y 2)), the redex is (+ x 1) and not (* y 2) because evaluation order is left-to-right).

(But what samth said is true even without that property.)

It’s unambiguous, but varies as we step through the trace, right? E.g., (* [(+ 1 1)] (+ 2 2)) => (* 2 [(+ 2 2)])

I guess my confusion is that, saying the redex seems to suggest that we fix a particular redex, but that’s not true, correct?

the redex in the current evaluation step

Please bear with me—I’m truly confused. So this is actually about one single step, and not a sequence of steps?

the definition was about the dynamic extent of an expression

in any evaluation step, the expression may or may not contain the redex (for the current evaluation step)

the dynamic extent of the expression is the sequence of steps in which the expression contains the redex

Ah, I think I understand it now. Thanks!