Symbol invokation in notation component

[kohlhase]

In MiKoMH/AI/source/prolog/slides/prolog-resolution.en.tex I have

  $\PrologLanguage$ as \symref{FOResolutionCalc}{resolution in $\PREDLOG$}.

and get the error

/Users/kohlhase/localmh/MathHub/MiKoMH/AI/source/prolog/slides/prolog-resolution.en.tex:12: Package stex Error: Symbol invokation
(stex)                http://mathhub.info/sMglom/logic/mod?pl1?PREDLOG not
(stex)                allowed in notation component of
(stex)               
http://mathhub.info/MiKoMH/CompLog/atp1/slides/resolution?fo-resolution?first-order-resolution

Type <return> to continue.
 ...                                              

l.12 ...OResolutionCalc}{resolution in $\PREDLOG$}

But this feels natural to me in this instance. I wonder why this restriction is necessary. If this is only that the "action-on-hover" or "onclick" is ambiguous, that is something I would let the user interface sort out.

[Jazzpirate]

It's debatable whether it's "necessary" - it probably isn't. But I think it's meaningful. The action-on-hover is "just" a reflection of the the underlying semantics, which in this case is unclear - by putting \PREDLOG in the symref, you are basically saying that whatever \PREDLOG outputs is part of a representation of FOResolutionCalc, but by virtue of \PREDLOG being a semantic macro, it is determined that its output is a representation of pl1?PREDLOG.

I personally would prefer either something like \symref{FOResolutionCalc}{resolution in $(something purely syntactic)$}, or alternatively \symref{FOResolutionCalc}{resolution in} $\PREDLOG$, depending on what you actually want the \PREDLOG to represent and (by extension) show on hover. Either way, I don't think the user interface should guess semantic intentions...

[kohlhase]

I disagree. But before I do I should say that I do understand that we may not want semantic stuff in the notation parts of \symdef and friends, where it is transported around. But for the "notation part of a \symref" the situation is different (I claim).

To me, the semantic intention of the \symref{FOResolutionCalc}{resolution in $\PREDLOG$} is totally clear and unambiguous, and I really want that behavior. We have $\PREDLOG$ as a semantic entity (which is why I disagree with something presentational here), and the resolution calculus is in that logic.

What the frontend does with that is a different story, and I also think the situation is relatively clear here as well. The front-end should give a link to ...?FOResolutionCalc on resolution in and to ...?PREDLOG on (the presentation of) $\PREDLOG$. There is not really any guessing involved.

So I do not see the problem, even if the situation in the front-end were unclear.

[Jazzpirate]

What the frontend does with that is a different story, and I also think the situation is relatively clear here as well. The front-end should give a link to ...?FOResolutionCalc on resolution in and to ...?PREDLOG on (the presentation of) $\PREDLOG$. There is not really any guessing involved.

There is though; clearly. To me, this is absolutely not obvious. What you describe is the functionality you can directly achieve via \symref{FOResolutionCalc}{resolution in} $\PREDLOG$, and this functionality is indicative of an underlying intention that \PREDLOG has its own semantics separate from FOResolutionCalc. In which case I don't see a reason to put the $\PREDLOG$ in the \symref at all ;)

But there is a second interpretation, namely the one you would achive by doing \symref{FOResolutionCalc}{resolution in $(something purely syntactic)$}. In that case, the whole argument would represent (and show on hover) FOResolutionCalc. I would claim that not only is this interpretation just as valid and meaningful as the one you described, but it could easily be the intended one: After all, since FOResolutionCalc is the resolution calculus explicitly for predicate logic, one could easily argue that the whole argument really should just link to the resolution calculus directly, since the definition of that already entails all the relevant information about predicate logic, and it's annoying to have different parts of the text link to different symbols ;) I'm actually even somewhat inclined to prefer this variant.

What this means to me is that a) the ambiguity is real and b) the author should make their intentions clear, and therefore c) the error message is actually helpful by pointing out that there is an ambiguity here.

[Jazzpirate]

Come to think of it, there's a third way that's more in line with what is actually written: Namely that the text resolution in FOL refers to the application of the function "resolution in" to the argument "FOL". I think this actually most closely represents the sentence itself, if we consider (as you seem to do) \PREDLOG to have its own semantics. In which case the \symref{FOResolutionCalc} would be ""wrong"", and instead it should be something like \ResolutionCalc{\comp{resolution in} $\arg{\PREDLOG}$}.

The ambiguity then is actually due to the fact that the specific application ResolutionCalc(FOL) has its own symbol FOResolutionCalc, and you're trying to "mix up" the syntax for the former to link to the latter. Under that interpretation, I would also argue that the variant \symref{FOResolutionCalc}{resolution in $(something purely syntactic)$} is the more adequate one though, since the application-to-FOL is already part of the symbol FOResolutionCalc := ResolutionCalc(FOL).