[mizar] structures

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

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

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. 


We can choose well-ordered ("SelOrder") infinite set of selectors 
("Selectors"), and then define e.g.:

definition
func carrier equals SelOrder(0);
synonym Objects;
synonym Vertices;
func topology equals SelOrder(1);
end;

definition
   let X be Function;
attr X is 1-sorted  means
carrier in dom it & it.carrier is set; 
attr X is TopStruct means
it is 1-sorted &
topology in dom it & it.topology is Subset-Family of it.carrier; 
:: synonyms can be here (probably for richer structures) 
attr X is strictly-1-sorted  means
{carrier} = dom it & it.carrier is set; 
end;


definition
  cluster 1-sorted Function;
  cluster TopStruct Function;
existence; :: from StructExistence;
  cluster strictly-1-sorted Function;
existence; :: from StrictStructExistence;
end;

definition
 cluster TopStruct -> 1-sorted Function;
  cluster strictly-1-sorted -> 1-sorted Function;
coherence; :: from StrictCoherence;
end;

definition
  let X be 1-sorted Function;  
func carrier(X) -> set equals X.carrier;
coherence; :: from def of 1-sorted
synonym Objects;
synonym Vertices; :: ....
end;


semantics of "1-sorted(#X#)":

we can ( like it is done now) automatically generate a functor (but then 
the system needs to be told to do it, e.g. by having attribute property 
"structural"). Such functors can behave as if their definition were
"equals {[carrier,X]}". 

Or it can be just a syntactic sugar for {[carrier,X]} - but then we need 
reconsidering, or we can (also automatically) try a cluster
{[carrier,X]} -> 1-sorted (but then the definition has to be done for 
"set", and we also need to state a cluster 1-sorted -> Function-like).


The set "Selectors" can be created e.g. using a global choice (e.g. on 
infinite sets from Rank(omega)), "SelOrder" also using a global choice
on 1-1 functions from NAT to Selectors. That makes the selectors quite 
abstract, so that they do not come in the way too much (like e.g. just NAT 
would, but I am not sure this has much sense). We could also take some 
urelements, but that requires adding them into axiomatics.


Pros:
- we immediately have synonyms for structures and selectors ( for 
  different contexts)
- we know what structures are at all, many assertions stated now only for 
  "strict" can be proved generally  
- we can try more abstract structures - e.g. attr "having-Binop" for 
  structures (functions) having somewhere in rng x,y st x is set & y is
  Binop of x, and then e.g. for structures with several "Binop"s use
  general theorems for "having-Binop"; also, it could be easier to do 
  various isomorphisms
- we have anything that now works for normal functors and modes, e.g. now
  it is not possible to redefine selectors (only state functor-clusters)
- the implementation can be simplified - we can throw away three kinds of 
  constructors (g,l,u), we do not need a special implementation for 
  structures (at least in the checker) - the work is done by clusters


Problems:
- how much should be done automatically? - e.g. having the property 
  "structural", which clusters should be generated, what should be left to 
  the user?; 
- we have to watch the numeration of selectors - e.g. several people in 
  their new article can choose the next free SelOrder; probably the 
  Library Committee should resolve the conflicts then ( as it is done 
  with new vocabulary)
- I surely forgot something, it requires some practical experiments
  (take it as a request for comments :-) )


Josef