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