Re: [mizar] structures

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

On Mon, 23 Sep 2002, Freek Wiedijk wrote:

> Andrzej Trybulec wrote:
> 
> >>Maybe putting this 0 or 1 in the vocabularies is better?
> >>It would be something like "Ucarrier 0" and "Utopology 1".
> >
> >You cannot have a space inside the symbol. Sorry.
> 
> That's not what I meant.  It's like the priorities with the
> func symbols.  It would mean that the symbol "carrier"
> corresponds to the natural number 0.  I.e., that "the carrier
> of X = X.0" and "the topology of Y = Y.1".

I don't know, first thought is that it is mixing semantics into
vocabulary, second thought that sometimes such things are practical.
I am not sure at all whether the whole process of "hiding" selectors
(using the global choice ) is useful or not - I feared that if using NAT
directly, some structures could accidentally e.g. become FinSequences,
and someone might try to misuse such "accidents". On the other hand, NAT
has some advantages, like 1 <>2 is evident (I hope) to the checker, and if
functors were created for Nats (this was discussed some time ago), we
could even define slectors directly as synonyms ( btw. wouldn't it be
nice to have synonyms for terms, not just functor symbols - like
expandable modes?).

Some errata to what I wrote:

> attr X is TopStruct means
> it is 1-sorted &
> topology in dom it & it.topology is Subset-Family of it.carrier;
obviously:
attr X is TopStruct means
X is 1-sorted &
topology in dom X & X.topology is Subset-Family of carrier(X);

We have to write carrier(X) here to have proper types (they are just 
casting functors here). This can complicate things a bit.

> Rank(omega)
obviously Rank(omega+1), but if we want this at all, st. like 
Rank(omega_2) \ Rank(omega_1) should be guaranteed to keep a good distance 
from any "normal" mathematics.

Josef