Open kohlhase opened 11 hours ago
There is a paradigm-shifting assumption in this, which I should emphasize: So far, the assumption was that a definition has as definiendum a symbol. The hover-pop up shows a definition for that symbol. Naturally, some definitions are more adequate to be shown than others, and there's a design question which definition for a given symbol to show.
Your comment implies that "actually, no, a definition has as definiendum a verbalization of a symbol", where "verbalization" is an as-of-yet still poorly understood concept that should be supported somehow but we don't yet know how and where.
Playing the slippery-slope-game, this has far-reaching consequences for every component of the entire system: Chances are that this opens the floodgates for everything that currently operates on symbols to operate on verbalizations instead. If verbalizations are the central definienda of definitions, the natural consequence would be that they're also the objectives/preconditions of problems, and explananda of explanations, etc. - after all, if a verbalization deserves its own definition, it makes sense that there are problems that require knowing that specific verbalization (rather than the symbol itself), etc. => Do verbalizations need their own URIs? Since we then need to be able to distinguish between them and uniquely identify them? => In the extreme case, we're back to where we started, actually, since now every verbalization behaves exactly as symbols do currently, so we just might want to rename symbols to verbalizations :D (of course, different verbalizations of the same symbol are then entirely disconnected, but we also don't yet know how different-verbalizations-of-the-same-symbol are supposed to be connected at all, from an operational POV)
=> Somewhere in this slippery slope is a sweet spot for... something that needs hashing out.
I have stumbled across the following confusing hover for the concept "state":
I think what happens is that the following definition from
MathHub/courses/FAU/AI/course/source/game-play/slides/game-formalization.en.tex
which adds some extra verbalizations (in particular "position" to the symbol
state
for the example above) and is somehow chosen for hover. The problem here is that this is a definition for a different verbalization (i.e. the word "position" instead of the word "state") and it is thus unsuitable for the hover.I am quite willing to assume that the definition above should be annotated differently (any hints welcome), but that does not change the general problem that with multiple possible verbalizations, we should pick a definition which actually introduces the verbalization that coincides with the one used in the term reference.