Re: [mizar] weak types

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

Dear Andrzej,

>Sorry, I did not read the paper,

I think you heard my talk though, but maybe it should have
been clearer...

>Does it means, that the system generates the sentence
>             x >= 0 & sqrt x > a

Yes, something like that.  Although in the theory this
conjunction does not occur as such.

>We experimented with something similar in seventies. Then for
>
>   not sqrt x > a
>
>we generated
>
>    x >=0 implies not sqrt x > a

I'm not 100% sure how the theory from our paper would translate
to Mizar-style proofs, but I would expect that in that case
it _also_ would be a conjunction:

     x >= 0 & not sqrt x > 0

Which is not so strange, if you think about it.  Why should
">" be positive and "<=" be negative? (if you're not an
intuitionist that is, for intuitionists it _is_ like that :-))
Because of course "not ... > 0" is the same as "... <= 0".

>Even if the implementation was easy, the results were
>discouraging - nobody knew how the sentence looks like.

So in PVS it works like this.  There it's called a "type
correctness condition".  The idea is that the type of "x" is
real number, but the type of "sqrt" is {x where x is real number :
x >= 0}->real, or something like that.  So the extra conditions
are added by the type checker.  Apparently there the people
don't have problems understanding how things turn out.

Freek