FOM: Reply to Trybulec on MIZAR project

Andrzej Trybulec trybulec at math.uwb.edu.pl
Mon Apr 26 11:59:36 EDT 1999


On Mon, 12 Apr 1999, Joe Shipman wrote:

> >1. I doubt if it can be done with Mizar as it is now. (***)
> >   The further development of the language is necessary. However,
> >   most of the problems related seems to be rather linguistic ones
> rather
> >   than logical.
>
> Can you be more specific?

I mean that for the practical fomalization we need a richer language.
Let us look what we already have in Mizar, just two examples:

1. Types

Mizar Mathematical Library is based on the set theory, TG
(the Grothendieck system) and the root type is "set".
However, Mizar allows for introducing new type constructors with which
we may construct new types: as example of type constructors:

Subset of ...
Function of ..., ...

So, the type of function from A to B is written as

Function of A,B

Perhaps the most important advantages of types are

i. Hidden arguments (I believe they are also in LEGO, maybe Robert Pollack
will give more exact information)
the composition of two morphisms in a category looks like

let C be Category;
let a,b,c be Object of C;
let f be Morphism of a,b, g be Morphism of b,c;
func g * f -> Morphism of a,c
...... (the definiens and the proof of the correctness is given here)

and the associativity of * the may be written as

(h * g) * f = h * (g * f)

Actually the introduced constructor has 6 argumets, two of them are
explicit (we call them "visible"), 4 (C,a,b,c) are "hidden"
It is possible only because knowing g and f, and supposing that they have
the proper types, we may reconstruct the remaining argumens of *
(Actually in Mizar we use extended ASCII, so it is not a star
but d249, i.e. \cdot)

Without types we should write e.g. Comp(C,a,b,c,f,g) and then
the associativity looks like

Comp(C,a,b,d,f,Comp(C,b,d,c,g,h)) = Comp(C,a,c,d,Comp(C,a,b,c,f,g),h)

(h is a morphism from c to d). And C (or some of a,b,c) may be
complicated expressions.

Because the types may be used to identify constructors
we may use the same symbol for different functors. E.g.

The notation a + b  is used now in Mizar for:
- the sum of real numbers
- the sum of complex numbers
- the sum of real sequences
- the sum in vectors spaces
- the sum of two subspaces of a vector space
- the coproduct in a category
and so on. All together more than 50 functors.

iii. Reservations

Mizar allows for so called "reservations", they correspond to clauses like
"In the sequel r,s,t range over real numbers". The actual syntax of it
is:
reserve r,s,t for Real;
Then if in a sentence one of the r,s, or t is free, it will be bound
by default at the beginning of the sentence (In Mizar we have no real
free variables)
Because the reserved identifiers may occur in the type for which
they are reserved, we may shorten (and make more readable) the text

After the reservations:
reserve C for Category,
a,b,c,d for Object of C,
f for Morphism of a,b,
g for Morphism of b,c,
h for Morphism of c,d;

we may write just

(h * g) * f = h * (g * f)

for C being Category,
a,b,c,d being Object of C,
f being Morphism of a,b,
g being Morphism of b,c,
h being Morphism of c,d
holds (h * g) * f = h * (g * f)

that is rather cumbersome. The Mizar language is rather verbose
but even if universal formula is written as (x!)(...) (like in HOL)
instead of "for x holds ..." the repetition of quantifiers is
rather tedious.

I guess it is enough about types in Mizar to feel how they are used.

I am slightly defensive about types, because the use of types in formal
langauges was under strong attack. Leslie Lamport with his papers:
"Types are harmful"
"Types are not harmless"
I do not remember the title of the next. It was something like
"It is pain in ..., to write about types".
Also John McCarthy and Bob Boyer are (or were) definitely against the types.

Mizar allows for defining (Boolean valued) attributes, with which we can
create two adjectives. Let me cite a real piece of Mizar
(the article FINSET_1 by Agata Darmochwal, 1989)

definition let IT be set;
attr IT is finite means
:: FINSET_1:def 1
ex p being Function st rng p = IT & dom p î omega;
antonym IT is infinite;
end;

After introducing the attribute we may use two adjectives
"finite"
"non finite"  (or rather "infinite")

Adjectives are used mostly in clusters on the beginning of a type.
Actually, most of the types is just a shorthand writing
for another type preceded by a cluster of attributes, e.g.

mode AbGroup is
add-associative right_zeroed right_complemented Abelian (non empty GroupStr);

I think that I wrote enough about Mizar, let me
finish with the remark that attributes have been introduced as syntactic
sugar. It seems now, that the proper processing of attributes is one of
the most important problems in the project.

Some other mechanisms are planned (not designed):

1. Modifiers

The construction "Function of A,B" is too rigid. I would like rather
"function from A into B"
It is not only syntactic sugar. We have another type
of functions, called
ManySortedSet of I
(a family parametrized by I),
but Mizar does not know (automatically) that a
Function of A,B
is a
ManySortedSet of A
We want in the future to write ManySortedSet of A as
function from A
and to widen automatically
function from A into B
to function from A, if necessary.

2. Operators

Mizar allows for only one operator (besides quantifiers), corresponding
to the replacement. Some of my collegues argue that we should have
lambda operator. But would be nice to have traditional notation
for integrals or inifite sums.

3. Multiple dots
What we usually (in mathematics) wrote as

a_1 + ... + a_k

One has now (in Mizar) to define a finite sequence
f = (a_1,...,a_k)
and then use a unary operator of the sum (of elements)
of finite sequences.

I put it upside down. We have the operator of the sum of elements
of a finite sequence and to use it we should write

consider f being FinSequence such that
len f = k and
for i st i in dom f holds f.i = a_i

and then use f as the argument. We do not have
the notation (a_1,...,a_k), either.

But of course, the most important may be the mechanisms that
we do not anticipate.

Andrzej Trybulec