FOM: Reply to Trybulec on MIZAR project

[Andrzej Trybulec]

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)
  Let me start with an example. The definition of
  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.

 ii. Overloading

   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)

instead of

      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.

2. Adjectives

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