[texhax] Some puzzling TeX (\@sptoken)

[Uwe Lueck]

Von: "Philip TAYLOR (Webmaster, Ret'd)" <P.Taylor at Rhul.Ac.Uk> wrote 01.06.2011 13:23:42:
> Uwe Lueck wrote:
>>
>> "The quantity<space token>, which was used in the syntax of<optional
>> spaces> above, stands for an explicit or implicit space. In other words,
>> it denotes either a character token of category 10, or a control sequence
>> or active character whose current meaning has been made equal to such a
>> token by \let or \futurelet."
>>
>> What seems *not to be said explicitly*, indeed!! (see
>> announcement above), is that <one optional space>
>> may be an implicit space token. (Of course it is said
>> *implicitly*.)
>
> So you would argue that although there is an explicit definition
> of the sort of spaces that may form <optional spaces>, this does
> not provide an explicit definition of the sort of spaces that may
> form <one optional space>. I am not sure I agree.

Indeed, when I distinguish "explicit" statements from "implicit"
statements here, there must be something that is implicit
rather than explicit. By "explicit" I mean that a machine
(such as TeX) can derive that \@sptoken is an instance of
<one optional space>, straightforwardly implemented along
the derivation rules given in the TeXbook. When you think you
understand what <one optional space> means, and you even
think this derives from the definition of <optional spaces>,
I call this "implicit". I do deny that you can formally
derive a replacement rule for <one optional space>
from the rules for <optional spaces>. Of course
<one optional space> is "most probably" a sequence
of <optional spaces> with at most one member,
but that is pragmatic, natural language, not formal
derivation, not the result of something explicitly said.

I was saying that I could not find a formal definition of
<one optional space> in the TeXbook, not even with a
text editor.

But the reason for this failure was that I did not notice
in time that `\is' in texbook.tex produces the long arrow
in the derivation rules, and actually this definition is at the
bottom of my TeXbook p. 269 -- it's a separate definition,
not a "consequence" of something earlier!

Sorry Grand Wizzard, sorry all!

Before I found that, I looked up the appendix of
Wolfgang Appelt's `TEX für Fortgeschrittene'.
This appendix *numbers* the rules, and the replacement
terms in all the rules have a superscript pointing to the rule
that defines the term. I may have needed to see

  <one optional space> --> <space token> | <empty>

(Appelt's (48)) to enable an unconscious function of my brain
and eyesto suddenly discover the same line in the TeX book
when I wasn't actually trying to.

Now it has been explicitly said that <one optional space>
may be an implicit space token, because it is said
explicitly that a <space token> may be an implicit
space token.

At least it is now formally derivable from explicit statements,
rather than explicitly said, as it is problematic to say
that mere consequences of explicit statements
have been explicitly stated, these consequences are
infinitely many ... cf. the so-called "logical omniscience problem"
in epistemic logic. (Oh, there "implicit" could be used
for logical consequences of explicit statements,
as opposed to an idea of "implicit" using pragmatics.)

Other words for the distinction: If I had found in The TeXbook
that <one optional space> is either <empty> or a "real"
(explicit) space token, I would not have considered it a
contradiction to the other formal rules.

Cf.

    http://en.wiktionary.org/wiki/implicit

BTW, the definition of "implicit characters" on TeXbook p. 269
is not very explicit (somewhat at odds with my celebrations above),
it tries to indicate the meaning of "implicit characters" by
the metaphor `masquerade' and examples only, and by a
too general reference to \let and \futurelet.
I think an explicit definition could be: An implicit character token
is a non-character token or an active character token that
after \meaning behaves like a non-active-character token.

Cheers,

  Uwe.