Re: [mizar] structures

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

> Josef Urban wrote:
>
> > Discussion about the usage of global choice in the Mizar type system has
> > been revived recently. I believe we should discuss these things
> > publicly, so I resend here some thoughts about the structures in Mizar.
> > -----
> >
> > I think there is a general agreement, that the semantics of Mizar
> > structures are partial functions. We could simplify (and perhaps
> > strengthen a bit) the system, if we defined them as such in Mizar - i.e.
> > they would be just normal modes, widening to the type Function.
> > I believe some (all?) of the things I suggest are similar to some
> > Grzegorz's suggestions.
>
> Hi Josef,
>
> You touched many problems so I intend to address them in separate mails.
>
> I doubt if I want structures widen to the type 'Function'. I do not see what
> is the gain, besides the general fact that we would may to instantiate the
> theorems about function by structures (for what purpose? ). But it will cause
> problems with overloading the symbols, putting the proper order in the
> 'notation' directive will be, perhaps, even more difficult.
>
> Actually I am not certain, if I want structures to widen to 'set'. If we have
> another root type,
> say 'something', that it would be enough if they widen to 'something' (I do
> not want to have urelements, we just have restore TARSKI:1 (now cancelled) :
> 'everything is a set').
>
> Then some problems related to the identification will vanish. E.g.
>
> 'Element of X'   (X being a set, grammatically)
> 'Element of S' with the meaning 'Element of the carrier of S'
> Now, one have to be careful to put STRUCT_0 after SUBSET_1 in the 'notation'
> directive.
>
> Actually we may to move all the concepts related to sets (Function, Relation,
> FinSequence and so on) to 1-sorted structures (I am tempted to steal 'setoid'
> from Coq and substitute it for '1-sorted').
> No need then to use a different symbol like in
>
> definition let S, T be 1-sorted;
>   mode map of S, T -> Function of the carrier of S, the carrier of T
>    means
> :: PRE_TOPC:def 11
> not contradiction;
> end;
>
> and the overloading in RLVECT_1

definition let V be 1-sorted; let x;
 pred x in V means
:: RLVECT_1:def 1
   x in the carrier of V;
end;

will be not dangerous. It caused sometimes problems.

Greetings,
Andrzej

PS I again pushed the "Send" button, instead of "Edit". I guess you get the
uncompleted message. I apologize for the inconvenience.

AT