I'm pretty sure I understand tail position, but I want to understand the formal definition in The Racket Reference.
Does the definition seem pretty clear to you? Would you re-write any of the statements in that section for clarity?
To tip my cards, the first line gets me:
An expression expr1 is in tail position with respect to an enclosing expression expr2 if, whenever expr1 becomes a redex, its continuation is the same as was the enclosing expr2’s continuation.
The only way I can see expr1's continuation being the same as expr2's is if the continuation for both was []. Or, as the first example says "just C".
I also think it's confusing to bring in C as "some continuation C" (unspecified). In the examples, both expr1 and expr2 are shown/considered (ie. not "C"). Why do we need to think about the next level up enclosing continuation? The stuff in the brackets will never depend on it, right?
(Yes I asked Claude, but what came back seemed like gobbledegook word salad)
When (if (zero? 0) (+ 1 1) 3)begins evaluation, its continuation is (add1 []). When its sub-expression (+ 1 1) becomes a redex, its continuation is also (add1 []).
(Edit: After thinking some more, I believe that the definition's use of "becomes a redex" is incorrect. It should be "begins evaluation" or "occurs in an evaluation context". Whether an expression is in tail position should not depend on whether that expression is a redex, or ever reduces to a redex. For example, I would like to be able to say that 1 and (add1 (error)) occur in tail position, but neither expression is a redex nor reduces to one. There's also the issue that, for example, (+ 1 1) is vacuously in tail position with respect to (+ (error) (+ 1 1)).)
To your next question: no, the stuff in the brackets might in fact depend on the continuation. For example:
Is (+ 1 1) in tail position with respect to the whole expression? If the expression is evaluated in the empty context, then (+ 1 1) is also evaluated in the empty context. But if the expression is evaluated in the context created by (call-with-continuation-prompt (lambda () []) my-prompt), then (+ 1 1) is not evaluated in the same context; it has an extra (void []) frame.
Continuation marks and control operators like call/cc provide more reasons that the continuation might matter.
I'm pretty sure I understand tail position, but I want to understand the formal definition in The Racket Reference.
Does the definition seem pretty clear to you? Would you re-write any of the statements in that section for clarity?
To tip my cards, the first line gets me:
An expression expr1 is in tail position with respect to an enclosing expression expr2 if, whenever expr1 becomes a redex, its continuation is the same as was the enclosing expr2’s continuation.
There are four components here: expr1, expr2, expr1's continuation
(when it becomes a redex) and expr2's continuation (which all the
examples call "C" in the notation).
I also think it's confusing to bring in C as "some continuation C" (unspecified). In the examples, both expr1 and expr2 are shown/considered (ie. not "C"). Why do we need to think about the next level up enclosing continuation?
Thus we have to think about some (in these examples, unspecified)
continuation one level up; it's one of the 4 components.
The stuff in the brackets will never depend on it, right?
Well, I'm sure there's an argument to be made involving one of the
continuation primitives which intertwines things.
The only way I can see expr1's continuation being the same as expr2's is if the continuation for both was . Or, as the first example says "just C".
The example with "if" if the docs uses an arbitrary continuation; it
need not be empty.
(Ryan's message came in while I was typing this, and I think it's a
bit more concrete, so I'll leave the examples to them! I think it's
still worth being explicit about the connection between the components
of the definition and the need to thus label the enclosing expr2's
continuation.)
An expression expr1 is in tail position with respect to an enclosing expression expr2 if, whenever expr1 becomes a redex, its continuation is the same as was the enclosing expr2’s continuation.
I think maybe you are being confused by conflating different notions of what a "continuation" is.
The definition of tail-position is best understood using the simplest notion of "continuation" which is just the next thing to do. An expression is in tail-position if the next thing to be done following it is to "continue" in an enclosing expression.
[To go even lower level, the continuation of a particular CPU instruction is the next instruction to execute. In the case of a conditional branch that "next instruction" may be immediately adjacent or may be far away.]
The heavyweight "function" notion of Racket [Scheme] continuations may be relevant to actually understanding some particular chunk of code, but it isn't needed to understand the concept of tail-position.