[FOM] Mizar's type system
Anthony Coulter
fom at anthonycoulter.name
Thu Oct 1 08:49:45 EDT 2015
Freek Wiedijk writes:
> Relatedly, Mizar shows that there is no conflict between
> "working in raw ZFC" and a "typed formalism". In Mizar
> everything is a "raw ZFC" set, while everything is fully
> typed as well.
I like Mizar's handling of subtypes, where integers are reals and
not a separate set equipped with an injection into the reals. But in a
way the Mizar type feels like a redundant concept---mathematically at
least, unary predicates can be used for the same purpose. Presumably
the "type" concept was separated out from the regular predicates for
reasons of convenience. I would like to see a complete list of such
conveneniences, from the perspective that a predicate-only type system
will have to recreate all of these conveniences before it can be "as
nice as Mizar."
(Note: My understanding of the Mizar type system is based on
section 1.3.4 of [1] and a cursory scanning of the MML. I do not have
a deep familiarity with the system, so please correct me if I get
anything wrong here!)
The strengths of types over predicates appear to be:
1. You can quantify over them, that is, you can use a syntactic con-
struct resembling "For all integers x, P[x]" instead of the more
cumbersome "For all x, if x is an integer then P[x]".
2. Mizar can automate a lot of tedious type inferences (e.g. if m and
n are integers, then m*(m+n+1) is also an integer) so that you can
infer "P[m*(m+n+1)]" from "For all integers x, P[x]" without extra
manual steps.
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.
There are two things I had assumed a priori to be advantages of the
Mizar type system, but on further investigation don't appear to be:
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.]
5. In traditional programming situations, a good type system will help
the user catch a lot of errors at compile time. This advantage *may*
apply to Mizar as well; I honestly don't know because I'm not a
serious Mizar user. But I get the impression from reference [1] that
type errors are more likely to result from not importing enough
other articles than they are to result from the user making an error
while trying to figure out how to write a formula.
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.
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?
Assuming my list above is complete (please, someone, tell me what I'm
missing if it's incomplete!) I could theoretically replicate all of
the "nice" features of types with sorts and ordinary predicates by
providing the following features:
a. A way to quantify over unary predicates, so that people can write
"For all odd x: P[x]" where "odd[x]" is a predicate
b. A way to quantify over n-ary predicates with the last (n-1) slots
filled in, so that people can write:
"For all x in S: P[x]" (where "in[x, S]" is a predicate) or
"For all x < n: P[x]" (where "x < n" is a predicate)
c. A way to manipulate these bounded quantifiers that doesn't require
them to be nonempty. (This goes a step beyond Mizar in convenience;
the idea is that "For all x in EmptySet: P[x]" ought to be as easy
to work with as "For all x in S" when S is a nonempty set.
d. Mechanisms for automatically inferring that m*(m+n+1) is an integer
whenever m and n are (without making the user explicitly cite the
theorem that the sum or product of two integers is an integer on
every line where it is used).
e. Some sort of function overloading? (If numbers and polynomials are
ultimately the same sort of object, i.e. well-founded ZFC sets,
then maybe overloading the word "divides" to provide different
definitions isn't actually the best way to go; it might be better
to insist that people use either "integerdivides" or
"polynomialdivides", and work on finding syntactic tricks to
reduce the amount of typing in such situations.)
Does this sound about right? Or am I missing some other important
advantages to the Mizar type system?
Regards,
Anthony
[1] Freek Wiedijk, "Writing a Mizar article in nine easy steps"
www.cs.ru.nl/~freek/mizar/mizman.pdf
More information about the FOM
mailing list