Re: [mizar] Type extensions

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

Hi Adam,

both your examples are parameterized types which "respect inclusion" of 
their parameters. I.e., if X1 c= X2 and Y1 c= Y2, then the extensions of 
both "PatrFunc of X1,Y1" and "Element of X1" are included in the 
extensions of "PatrFunc of X2,Y2" and "Element of X2".

Your question is how to make this into automated subtyping.

I think that even simpler question is how to "reflect" normal inclusion in 
subtyping - that's the case for "Element of".

The two solutions used so far are:

a) prove that if X c= Y, then X is Subset of Y (that's now built-in 
"reflection" in Mizar), and then declare "Element of X -> Element of Y" 
provided that X is Subset of Y  (this is used for NAT c= REAL)

b) have a corresponding attribute to each "important set" (e.g. attribute 
"real" for set "REAL"), and declare "real -> complex"

I think that neither (a) nor (b) is perfect. (a) looks more general, but 
(b) works often better, because terms can have mutliple attributes (thus 
allowing multiple "attribute inheritance"), while only one type (like e.g. 
"Subset of"). Additionally, I am not sure if "Subset of" behaves 
transitively now (while attributes definitely do).

So we should try to have "best of both worlds", and allow some limited 
(explicitly) parameterized attributes. It would use the current 
transitive and mutliple inheritance attribute mechanisms, and avoid the 
necessity to have explicitly defined attribute for each "important set" ( 
something like "x is REAL number" instead of first definining "real" as 
the attribute, and then saying "x is real number").

Similarily: "NAT is REAl subset", "REAL is COMPLEX subset", etc. ("subset" 
being a parameterized attribute here).

Then e.g.:

registration
let X be set; let Y be X subset;
cluster Y subset -> X subset;
.... (by transitivity of inclusion)

or even

registration
let X1,X2 be set; let Y1 be X1 subset, Y2 be X2 subset;
cluster X1,X2 partfunc -> Y1,Y2 partfunc;
....


or there could even be a type/attribute property, saying that it respects 
inclusion(wrt. some parameter, or all of them) - effectively doing the 
same as the cluster above.

Two more notes:
- in above, one starts from sets and has language for creating 
corresponding parameterized attributes; this could probably be reversed: 
start from attributes and have good machinery for dealing with "the set of 
all x st x is foo"

- it seems to me that a lot of these typing problems are for type "Element 
of" and "Function of"; these two types are built-in and handled with a lot 
of automation in some other proof assistants using typed (HOL) 
foundations; it would be interesting to see if there are examples of other 
types in MML which do not fall into this category and pose similar 
problems (and thus more general setting than that used in typed proof 
assistants is generally useful for mathematics)

Best,
Josef


On Sun, 10 Sep 2006, Adam Grabowski wrote:

>  Dear all,
>  in one of the articles recently submitted to the Mizar Mathematical
> Library (currently under review process) one can find the following
> definition:
>
> definition
>  let X be non empty set;
>  let S be SigmaField of X;
>  let M be sigma_Measure of S;
>  let f be PartFunc of X,REAL;
>  func Integral(M,f) -> Element of ExtREAL equals
>    Integral(M,R_EAL f);
>  coherence;
> end;
>
> where "Integral" was defined in MESFUNC5 for "f" of the type
> PartFunc of X, ExtREAL (the remaining variables are of the same
> type as in the above definition). Even if the set "REAL" (the set of
> all real numbers) is a subset of "ExtREAL" (the set extending REAL
> by the infinite values), the Mizar system does not give automatically
> a type "PartFunc of X,ExtREAL" to partial functions of X, REAL.
> This could result in the duplication of notions, even if only some
> casting functions are used instead of defining notions from scratch.
> (as R_EAL f just assigns the type "PartFunc of X, ExtREAL" to f which
> is a partial function from X into REAL).
>
> Very similar problem apeared in the case of the type "Element of REAL"
> and "Element of COMPLEX" (with the earlier not extending to the latter).
> Now we force the users to use "real number" and "complex number",
> respectively. Thanks to the mechanism of the conditional clusters
> with the registration as follows:
>
> definition
>  cluster real -> complex number;
>  coherence; :: with some easy proof to be found in XREAL_0
> end;
>
> a number of duplications can be avoided.
>
> I would like to know your opinion about the best solution
> (or at least, the better one) in the case of partial functions
> (and hopefully, some general guidelines for the future).
>  Regards,
>  Adam Grabowski
>  Library Committee of the Association of Mizar Users