Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
id GAA02656 for qed-out; Mon, 22 May 1995 06:47:42 -0500
Received: from cksr.ac.bialystok.pl (cksr.ac.bialystok.pl [193.59.8.46]) by antares.mcs.anl.gov (8.6.10/8.6.10) with SMTP
id GAA02641 for ; Mon, 22 May 1995 06:43:03 -0500
From: trybulec@cksr.ac.bialystok.pl
Date: Mon, 22 May 95 13:41 MED
Message-ID: <9505221347.AA09578@cksr.ac.bialystok.pl>
To: qed@mcs.anl.gov
Content-Length: 4089
Content-Type: binary
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
X-UIDL: 801410893.008
The approach [2] (according to Harrison's classification) is standard in
Mizar. The inverse is treated exactly as John wrote:
1. The definition of inverse is (I edited it slightly
to make it understandable outside the context, the same goes for
other examples)
definition
let x be Real;
assume x<>0 ;
func x" -> Real means
x * it = 1 ;
end;
One can justify that 0 * (0/0) = 0 by reference to the theorem REAL_1:23:
x*y=0 iff (x=0 or y=0)
i.e. Mizar accepts
0 * (0/0) = 0 by REAL_1:23;
as a correct inference.
(actually in Mizar we use rather \cdot than *).
We say that a definition is permissive if it allows for assigning
some arbitrary value outside its domain.
( We borrowed the name from W{\l}adys{\l}aw Turski, he used it for
incomplete specification.)
If I correctly recall
permissiveness is used in Excheck for the abstraction operator, one
can use
{ x : P[x] }
without any restriction, but to infer
y \in { x : P[x] } implies P[y]
one have to prove earlier that there exists a set A such that
P[x] implies x \in A
(I doubt if the syntax I use is really the Excheck syntax, sorry;
I just like this example).
However, the approach [1] gives quite often better results. We have
changed (while revising the Mizar library) a number of definition
that were originally permissive, that enabled enhancement of the
library:
The definition of the result of the application of a function f to
an arbitrary x was originally permissive:
definition let f,x;
assume x \in dom f;
func f.x -> Any means
[x,it] \in f;
end;
(square brackets we use for ordered pairs)
It is now:
definition let f,x;
func f.x -> Any means
[x,it] \in f if x \in dom f otherwise it = 0;
end;
with the second definition we can simplify the original theorem FUNCT_1:23
x \in dom f & f.x \in dom g implies (g \cdot f).x = g.(f.x);
to
x \in dom f implies (g \cdot f).x = g.(f.x);
( \cdot stands for the composition of functions )
It is very important in Mizar to get more concise theorems.
To use a theorem in a proof we have first to prove
its premises, and we get an abundance of trivial facts (something is
non empty, something belongs somewhere) that makes the proof obscure
and takes a lot of work (it takes in some proofs more than 50 per cent of
the text).
Also, after such simplification some theorems coincide, and may be removed
from the library (and data base as well). And the size of the data base
is a critical parameter.
Then, why the second approach ?
John pointed out that the first one
>>> gives you strange "accidental" theorems
and the second one gives
>>> gives fewer convenient theorems, but also fewer accidental ones
That's right, but this is a minor point, nobody is pressed to formulate
such theorems. I would like to call them "obscene" (or it is too
strong ? then "shocking", "indecent" ? ... English native speakers
should decide; we need a technical term for them, I hope that "obscene"
might be good, because it is rarely used as a scientific term).
Teaching Mizar I often use the slogan
" you can divide by zero, but you don't do it"
or more general
"even if the language allows for obscenities, it does not mean
that the user should use them"
and of course it is just nothing in comparison to the Automath restaurant,
could you imagine what will be served in it ?
What is more important, quite often it is not clear which value is
convenient.
One can put
0" = 0, to get (-x)" = -x", or
0" = 1, to get x/y = 0 implies x = 0 or
0" = +\infty (the most reasonable if system allows for infinite values).
Therefore we encourage users to use permissiveness (if they have no
precise preference). After some experience we change to non permissive
definition, while revising the library. If it is possible.
Mizar is a typed language and if f is a finite sequence of elements of
a non empty set D, then the concept of
the k-th member of f
must be permissive (if it is supposed to be an element of D).
To summarize, the general approach is the approach [2], when possible
and useful we use approach [1].
Andrzej Trybulec