Re: [mizar] Medice, cura te ipsum

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hello,

On Wed, 31 Jul 2002, Piotr Rudnicki wrote:

> On Mon, Jul 29, 2002 at 03:45:28PM +0200, Andrzej Trybulec wrote:
>
> > Piotr Rudnicki and Adam Naumowicz recently discuss semantics and syntax of
> > Functor Cluster Registration, in private.
>
> Fascinating, I did not know about it.

Well, we exchanged some e-mails on that matter. I cannot quote it here
because it was done in Polish, but let me just recall the idea.
Piotr Rudnicki asked why a (functorial) cluster of the form

definition
 let x_1 be T_1;
 ...
 let x_n be T_n;

 cluster x_n -> A_1 A2 ... A_k;

correctness;
end;

doesn't work, i.e. a sentence

for x being T_n x is A_1 A_2 ... A_k;

is not accepted by Mizar checker. He suggested that it should
be treated as if it was a conditional cluster:

definition
 let x_1 be T_1;
 ...
 let x_n be T_n-1;

 cluster -> A_1 A2 ... A_k (T_n);

correctness;
end;

Currently, Mizar doesn't complain about the first cluster but
merely ignores it. In my opinion, the best solution is to report parser
error restricting functorial clusters to proper terms. Of course, it is
also possible to pass the cluster to the analyzer as if it was a corresponding
conditional cluster, but then, the usual justification of correctness in
that case:

correctness
 proof
  let a be T_n;
  thus a is A_1 A2 ... A_k;
 end;

looks weird because of the 'let'. So I think the first solution is
somewhat 'cleaner' and doesn't complicate the syntax. Any ideas?

Regards,
Adam Naumowicz

--------------------------------------
WWW: http://math.uwb.edu.pl/~adamn/
--------------------------------------