Re: [CZT-Users] Z Standard issues related to user-defined operators

[Petra M. <Pet...@ec...>]

Hi Pablo,

You wrote:
> I am having troubles in determining, from the Z Standard, which names
> are valid (and which are not) for user-defined operators. In Page 28,
> the Z Standard assures "Each operator template creates additional
> keyword-like associations between WORDs and operator tokens.". However,
> not all WORD seems to be accepted. And I could not find more
> restrictions about this issue in the Z Standard.

There are a few more restrictions on user-defined operators on page 35
(8.3 User-defined operators).  Also relevant to your question is page 25
(7.2 Formal definition of context-free lexis) and page 26 (7.3
Additional lexical restrictions, notes and examples) as well as page 84
(Annex A; A.2 LaTeX mark-up).

> the following are rejected:

> \_ <1 \_: X \rel X

"<1" is lexed as two tokens: the DECORWORD "<" followed by DECORWORD
"1".  If you have a look at page 25, you'll find that "1" is an ALPHASTR
while "<" is a SYMBOLSTR and if you want to form a word out of those you
have to put WORDGLUE between the two like in "<_1".


> \_ <? \_: \nat \rel \nat \\

"<?" is actually a DECORWORD but since you are using LaTeX mark-up and
spaces are added around "<" (see page 84 of the Standard) it is lexed as
two words.  To avoid having spaces added when translating from LaTeX to
Unicode add braces: "{<}?"

>  \function 40 \leftassoc (\_ ope \_)

Here you need hard spaces: "\_~ope~\_" or even better use the \varg
latex command "\varg ope \varg" to avoid having the lexer merge the
underscore and "ope" to a word.  (Note that "_" is defined as WORDGLUE
on page 21 and then used to glue words on page 25.)

> I suppose that the name cannot start with a letter

It can start with a letter as in the ope example above.

> nor finish with a stroke (case in which it is
> a DECORDWORD instead of a WORD).

And it can have decorations, too.

> However, I understand that <1 and 1< are valid WORD's.

But they are not; see example above.

> Additionally, which situations, where an operator appear, needs to
> previously define the corresponding operator template paragraph and
> which not? The following two paragraphs are accepted without one of
> these paragraphs:
> 
> \begin{gendef}[X]
> \_ <_1 \_: X \rel X
> \end{gendef}

That's because in one of the toolkits there is an operator template for
"<" and the mapping to operator tokens is based on the WORD part (see
page 27).

Hope this helps,
Petra