Re: [mizar] structures

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

Josef Urban wrote:

> Hi,
>
> 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.

Josef is right, only he wrote about structures, not about the Global Choice.
Let me remind what it is about. Actually I wrote few years ago about it. On
the Mizar Digest. Maybe a bit more that few, we were still on BITNET.

I proposed then to add to Mizar syntax a construction
      the <type>
with the meaning a fixed object of the type <type>. The syntax is no good, too
much ambiguity. Piotr (Peter Rudnicki) proposed to use 'fixed' or 'chosen'. I
like
   the fixed <type>
It is verbose, but Mizar is verbose anyway. I believe that it was a Stef
Postma's slogan that
 "the language should be rather verbose than obscure"
or it is from a Scottish project, sorry, I do not remember.

Grzegorz (Bancerek) propose that we should adopt an additional rule, that
    'the fixed set' should be the empty set
I agree, but it looks as a requirement. Moreover, he proposed that if the
empty set has the type theta, then 'the fixed theta' equals to the empty set.
It may be generalized: if the mother type of theta is theta_1 and
      the theta is theta_1
then
     the theta = the theta_1
Grzegorz proposed much more, but because I disagree, let him write about that.

It is useful. E.g. the attribute 'circular' is defined in FINSEQ_6 as

definition let D be non empty set;
 let IT be FinSequence of D;
 attr IT is circular means
:: FINSEQ_6:def 1
 IT/.1 = IT/.len IT;  :: (*)
end;

it of course should be define for 'FinSequence' rather than 'FinSequence of D'

so the definiens becomes
    IT.1 = IT.len IT   :: (**)
But, if you try to revise the library in this way, you run into problems with
the empty sequence. According to (**) the empty finite sequence is circular,
because the permissiveness in the definition of the application is broken, and
the values of the function on an element outside its domain is 0. The
restricted application is still permissive, and you cannot to define it as a
non permissive functor, so one does not know if
     IT/.1 = IT/.len IT
or not. And we cannot claim, according to (*) that the empty FinSequence is
circular.
But if we use Global choice, then
    IT/.1 = the fixed PartFunc of NAT, D .= IT/.len IT
and the generalization can be done. 'PartFunc of NAT,D' is the mother type of
'FinSequence of D'

I believe it is worth to use this more precise semantics.

Andrzej Trybulec