Re: [mizar] weak types

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>To be a bit more precise, x/y is defined as x*y", so
>breaking the permissiveness we rather put 0" = 0 (it is not
>original, I owe the information, that this works pretty well
>in HOL, to John Harrison; and John has shown me a book of a
>British algebraist, sorry I do no remember the name, that
>observed that nobody knows why mathematician do not allow
>division by zero).

Yes I know all this.  My point is not that it doesn't make
any mathematical sense to define x/0 = 0.  I think the whole
theory would be perfectly fine with that choice.  My point is
that it is not what is the _customary way_ of talking about it.

I don't think that formalizing mathematics in Mizar should
mean changing mathematical conventions if it happens to be
convenient for the formalization.

No, I don't like it in HOL either.  You get "accidental"
theorems.  I hate that.

>I do not know what you mean by _illegal_ (I am not kidding,
>there are few different meanings of it).

(So what are the meanings of illegal I can choose from?)

What I meant is that x/0 is not defined, and not in the sense
that we don't know what it is, but in the sense that (x,0) is
outside the domain of the division function.

>Let us think about an experiment. Let we introduce
>   fd(x,y)       fd - funny division
>with the meaning as it is in MML, and x/y in your meaning
>(Michael Kohlhase has nothing against our x/y, but claims
>that we should use a different notation).

Ha!  I know now what I want.  I want / to be defined by

  definition let x be complex number, y be non-zero complex number;
   func x/y -> complex number ...
   ...
  end;

Now _that_ would be masochism :-)

>Then we will see which functor the authors would prefer. It
>is difficult to forecast the result, but I believe that
>(most of) the authors would prefer the functor that is
>easier to use, i.e. fd(x,y)

I don't know.  It's similar to a choice between on the one
hand using m - n for natural numbers and then reconsidering
the answer to be a natural number (if it is), and on the
other hand using m -' n.  I always hate writing m -' n if I
mean m - n (even if from the context I know that the answer
is a natural number.)  So to me your "fd" is like m -' n.
Maybe it should be written x /' y :-)

>I think that using 'element of ...' defined above instead of
>'Element of ...' is a sort of masochism.  But maybe it is
>more honest way to cope with the problem.

But I don't like either definition!  As, of course, I want
Element of X to be the empty type when X = {} :-)

Freek