[FOM] Mizar's type system
Artur Kornilowicz
arturk at math.uwb.edu.pl
Sat Oct 3 10:38:09 EDT 2015
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
More information about the FOM
mailing list