Re: [mizar] Structures and strictness

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

Hi Gilbert,

it seems to me that using attributes and clusters as you suggest is now 
the best way to handle this, quite unfortunately for the whole system of 
structures contained in MML now. 

One other idea, if you want to avoid replicating the definitions, is to 
compose the original functor (creating the strict structure) with some 
"enriching" functor, adding back the forgotten fields, but this is also 
quite painful.

I hope your example will convince the ENOD ("Experience Not Only 
Doctrine" :) worshippers, that there is really time to do something about 
the structure system and its semantics in Mizar, if it is to be used at all.

Best,
Josef


On Wed, 31 Dec 2003, Gilbert Lee wrote:

> Hi
> 
> I am having a number of problems with Mizar structures and "strictness"
> and would like some opinons about possible work-arounds.
> 
> I've created a hierarchy of structures based on the MultiGraphStruct
> (defined in GRAPH_1) by the addition of 3 selectors: Weight, ELabel, and
> VLabel, which represent weights on an edge, edge labels, and vertex
> labels.  For purposes of generality, the sets from which weights and
> labels come from are given as parameters to the structure:
> 
> ========================================================================
> definition let WL be set;
>   struct (MultiGraphStruct) WGraphStruct over WL
>    (# Vertices, Edges -> set,
>       Source, Target -> Function of the Edges, the Vertices,
>       Weight -> Function of the Edges, WL #);
>  end;
> 
> definition let EL be set;
>  struct (MultiGraphStruct) EGraphStruct over EL
>   (# Vertices, Edges -> set,
>      Source, Target -> Function of the Edges, the Vertices,
>      ELabel -> PartFunc of the Edges, EL #);
> end;
> 
> definition let VL be set;
>   struct (MultiGraphStruct) VGraphStruct over VL
>   (# Vertices, Edges -> set,
>      Source, Target -> Function of the Edges, the Vertices,
>      VLabel -> PartFunc of the Vertices, VL #);
> end;
> ========================================================================
> 
> Inheritance is as follows:
> 
>         WGraph over WL - WEGraph over WL,EL
>       /                X                    \
> Graph - EGraph over EL   WVGraph over WL,VL - WEVGraph over WL,EL,VL
>       \                X                    /
>         VGraph over VL - EVGraph over EL,VL
> 
> An example of a function I would like to define assigns a label to a
> particular vertex in a VGraph.
> 
> for example:
> definition let VL be set, G be VGraph of VL, v, val be set;
>   func G.labelVertex(v, val) -> strict VGraph of VL means
>    the MultiGraphStruct of it = the MultiGraphStruct of G &
>    the VLabel of it = (the VLabel of G) +* (v .--> val) if
>    (v in the Vertices of G & val in VL) otherwise
>    the VGraphStruct of it = the VGraphStruct of G;
> 
> As far as I know, in order to prove uniqueness, the return type for this
> kind of function must be a strict VGraph of VL. However, this means that
> I will need three more nearly identical functions to deal with WVGraphs,
> EVGraphs, and WEVGraphs.  Three is still manageable, however this becomes
> a larger problem as more selectors are introduced.
> 
> What are current methods are there to work around this problem?  I have 
> played with not using structures, and emulating selectors using 
> attributes, which seems to work well.
> 
> Thanks and have a Happy New Year
> 
> Gilbert Lee
> 
> 
> 
>