[mizar] [arms@dendronic.com: Re: A request from W W Armstrong]

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

Bill Armstrong has asked me to forward the follwoing message.

PR


----- Forwarded message from William W Armstrong <arms@dendronic.com> -----

Date:	Sun, 25 Aug 2002 11:42:13 -0600
From:	William W Armstrong <arms@dendronic.com>
To:	piotr@cs.ualberta.ca
Subject: Re: A request from W W Armstrong
Cc:	arms@dendronic.com
Reply-To: arms@dendronic.com
Organization: Dendronic Decisions Limited
In-Reply-To: <20020825092349.B4314@sedalia.cs.ualberta.ca>
X-Mailer: Becky! ver. 2.00.05
X-MDaemon-Deliver-To: piotr@cs.ualberta.ca
X-Envelope-To: <piotr@cs.ualberta.ca> (uid 60001)
X-Orcpt: rfc822;piotr@cs.ualberta.ca

Hi Piotr,

Thanks for your note re MIZAR.  There is another suggestion that I made
which I think is important for readability.  All optimization
information should be syntactically separated from the logic, eg

pragma
<defined term>
automatically uses
<properties>
end

eg

definition
  let n be Nat, p, q be Tuple of n, BOOLEAN;
 func p '&' q -> Tuple of n, BOOLEAN means
for I being set st i in Seg n holds it.i = (p/.i) '&' (q/.i);
end

pragma
'&'
automatically uses
commutativity;
end;

This could be placed in a section at the back of a MIZAR document so as
not to disturb readability. Note that the above pragma would apply both
to the basic operation on BOOLEAN as well as the overloading to Tuple.
 As MIZAR evolves and becomes smarter, this part could change, but the
definitions will remain the same, for example some day with a smarter
MIZAR, you may be able to replace the pragma by the following

pragma
'&'
automatically uses
commutativity;
associativity;
distributes over '|';
end;

This pragma concept is a bit like "proof hints" that go beyond
proof checking without making MIZAR a proof finder. Thus the goal
of pragma becomes not only optimization, but shortening proofs by
skipping more steps which are "obvious" to a mathematician.  If I recall
correctly there was something like this in LCF (logic for computable
functions -- I can't find the book, but I see this has continued in the
form of HOLCF.  http://www4.informatik.tu-muenchen.de/papers/MNOS-JFP99.html

Best wishes to Andrej when you write to him.

Bill

_____________________________________________________
  D E N D R O N I C    D E C I S I O N S    L I M I T E D
          Advanced computing research and consulting
                       Special expertise in machine learning


  3624 - 108 Street N W           phone/fax:         +1 780 421-0800
  Edmonton, Alberta               email:          info@dendronic.com
  Canada  T6J 1B4                 website:  http://www.Dendronic.com

             William W. Armstrong PhD   "Bill"
             President and Chief Scientist
_____________________________________________________


----- End forwarded message -----

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr