Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Thu, 20 Nov 2003, Freek Wiedijk wrote:

> 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 :-)

Prof. Goguen has for similar reasons defined in
http://www.cs.ucsd.edu/users/goguen/pps/nosa1.ps
the notion of "retract" operators, providing some middle way between 
"compile-time" and "run-time" type checking. They may even have 
implemented it in OBJ3, I am not sure.

The idea is, that for types T1 < T2 (e.g. non-zero complex < complex), you 
give those terms formally typed as T2 "the benefit of doubt", i.e. if you 
need T1 for them instead, you temporarily use a formal casting (retract) 
operator, and delay the verification of T1 until "run-time".

In Mizar, just substitute "analyser" for "compile-time", and "checker" for 
"run-time".

Then if you have e.g.  1/(6 - 4), and the definition of "/" requires the 
second argument non-zero, you give (6-4) "the benefit of doubt", and check 
it for being non-zero in the checker.

I think this method can be both strengthened and weakened, one could e.g. 
allow this only for certain operators, or arguments of certain operators, 
etc. The main problem for Mizar is relative weakness of the checker - 
checking number for being non-zero would be ok, but there might be more 
complicated definitions of T1. 
I think that in longer horizon, it will become necessary to have more 
computer algebra in Mizar, or even some elements of programming stronger 
than just cluster mechanisms today, so this method may eventually become 
an option too.

Josef