SIMPLE-ID ::= WORDS
ID ::= TOKEN-ID
TOKEN-ID ::= TOKEN
TOKEN ::= WORDS | DOT-WORDS | SIGNS | DIGIT | QUOTED-CHAR
The internal structure of identifiers ID, used to identify sorts, operations, and predicates, is insignificant in the abstract syntax of basic many-sorted specifications. (ID is extended with compound identifiers, whose structure is significant, in connection with generic specifications in Section 6.5.)
In concrete syntax, an identifier may be written as a single token: either a sequence of letters and/or digits--possibly mixed with single underscores (_) and/or primes ('), and possibly prefixed by a dot (.)--or a sequence of other printable ISO Latin-1 characters (excluding ( ) ; , ` " %). Keywords, and various other sequences that could be confused with separators, are not allowed as tokens in the input syntax (however, display annotations may be used to produce them when formatting identifiers).
ID ::= ... | MIXFIX-ID
MIXFIX-ID ::= TOKEN-PLACES
TOKEN-PLACES ::= token-places TOKEN-OR-PLACE+
TOKEN-OR-PLACE ::= TOKEN | PLACE
An identifier may also be a mixfix identifier `t0__...__tn', consisting of a list of tokens or spaces ti interspersed with place-holders, each place-holder being written as a pair of underscores `__'. Mixfix identifiers allow the use of mixfix notation4 for application of operations and predicates to argument terms in concrete syntax. A mixfix identifier such as f__ is a different symbol from f. An application of the (unqualified) symbol f__ to x may be written as f x, f(x), f__(x); an application of f to x may only be written as f(x). `Invisible' identifiers, consisting entirely of two or more place-holders (separated by spaces), are allowed.
Braces `{', `}' and square brackets `[', `]' are allowed as complete tokens in identifiers; however, any occurrences of these characters in a declared identifier must be balanced; e.g., `{[__}]' and `{__]' are not allowed.
An identifier ID may be used simultaneously to identify different kinds of entities (sorts, operations, and predicates) in the same local environment. It would not, however, be appropriate to use it simultaneously for constants and variables of the same sort, since its (unqualified) use would then always be ambiguous, making the enclosing formula ill-formed.