[FOM] Mizar's type system

[Artur Kornilowicz]

Dear Freek,


On Fri, 2 Oct 2015, Freek Wiedijk wrote:

> Dear Anthony,
>
>> But in a way the Mizar type feels like a redundant
>> concept---mathematically at least, unary predicates can
>> be used for the same purpose.
>
> Foundationally that's fully correct.  Pragmatatically it
> makes a world of a difference.
>
> Only it's not only unary predicates, (n+1)-ary predicates
> correspond to dependent types with n variables.
> And dependent types are *really* useful if you want to
> formalize mathematics (ha!)
>
>> Presumably the "type" concept was separated out from the
>> regular predicates for reasons of convenience.
>
> I think it was the other way around: the Mizar
> people consider their system to be a generalization of
> many-sorted logic.  That also "explains" their non-emptiness
> requirements.
>
>> I would like to see a complete list of such conveneniences,
>
> I think you pretty much got them all.
>
>> (Note: My understanding of the Mizar type system is based on
>> section 1.3.4 of [1] and a cursory scanning of the MML.
>
> There also is
> <http://www.cs.ru.nl/~freek/mizar/miztype.pdf>
> although I doubt it will add much for you.
>
>> 3. You can overload symbols, so that "x divides y" has
>>   one meaning when x and y are numbers and a different
>>   one when they are polynomials.
>
> FWIW: this is _really_ nice to have.  The Mizar types
> are about overloading as much as about type checking and
> predicate inference.
>
>> 4. The type system *could* concievably enforce function domains by
>>   wiring them into the type system, via something like:
>>   "let a be Real; let b be non zero Real; func div(a,b) = ..."
>>   [But Mizar does not appear to do this, at least with regards to
>>    division by zero.]
>
> That's about how the MML is organised, not about the
> type system.  But it just is too inconvenient to do it
> like this, because type changes ("reconsider") only are
> possible on the proof step level, and not in expressions
> (there are no proof terms or things like TCCs!)
>
>> Then there's a weakness of Mizar types:
>>
>> 6. Types must be nonempty; that is, you must prove that at least one
>>   object has a certain type before you're allowed to use that type
>>   for anything. (I assume that Mizar is using Skolem constants and
>>   functions internally, and the restriction to nonempty types is
>>   needed to justify that technique.) Ordinary predicates do not
>>   suffer from this constraint because they're not coupled so closely
>>   to quantifiers.
>
> This is the reason I stopped using Mizar.  I tried hard
> to convince Andrzej Trybulec and the other Mizar users at
> the time that this was a huge defect, but they did not see
> the point.


Mizar supports a way to define new types (and new operations) even if they 
are undefinable for some their arguments (e.g. a homeomorphism between two 
different topological spaces).
We can use permissive definitions - definitions with global assumptions.
For example, a homeomorphism can be introduced under the assumption that
spaces are homeomorphic.

definition
   let S,T be TopStruct;
   assume S,T are_homeomorphic;
   mode Homeomorphism of S,T -> Function of S,T means :LABEL:
   it is being_homeomorphism;
   existence proof ... end;
end;

When we have an expression of the type "Homeomorphism of S,T", Mizar 
understands that the expression is a function between S and T, but to 
infer (by LABEL) that the function satisfies properties of homeomorphisms 
(is "being_homeomorphism") it has to be justified earlier that spaces S 
and T "are_homeomorphic".

Kind regards,
Artur Kornilowicz



> Josef Urban tells me that it would be a rather small change
> to the system to allow non-empty types as well, but I'm
> not sure we'll ever see that experiment.
>
>> Now, when it comes to logic, I'm personally comfortable with "sorts"
>> (i.e. "hard types" that are not interconvertible; think "many-sorted
>> logic") and, like I said earlier, ordinary predicates. So when I try
>> to imagine an ideal proof-checker, I look for solutions that involve
>> only these concepts, and not a separate type mechanism. How close am
>> I to having something workable?
>
>
> Freek
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>


==========================================================================

Artur Kornilowicz                          e-mail: arturk at math.uwb.edu.pl

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Informatics                   tel. +48 (85) 738-83-33
University of Bialystok                    fax. +48 (85) 738-83-33
ul. Konstantego Ciolkowskiego 1M
15-245 Bialystok, Poland