Date: Thu, 20 Jun 91 19:58:58 EDT
From: Sandy Murphy <sandy@com.TIS>
Message-Id: <9106202358.AA25006@TIS.COM>
To: info-hol@edu.uidaho.cs.ted
Subject: select
Cc: sandy@com.TIS


Many math algorithms have a statement in them that denotes a choice to
be made.  Something like: take any item X with the property P.  The
specific item is not important, just the fact that it has property P.
Using the @ function works fine in specifying such an algorithm, and you
can go on to prove useful theorems about the algorithm.

The implementations of such algorithms must devise some way to make the
choice.  Some function f that returns an item with property P must be
written.

Then comes the point of proving that the implementation correctly
implements the algorithm, so that the theorems about the algorithm can
carry over to the implementation.

I believe that it is not possible to show that the function f correctly
implements the @ function, given the usual meaning of "correctly
implements".  (@x.Px) denotes some particular but unspecified x.  The
usual meaning of "correctly implements" is that every state change in
the implementation must be an allowed state change in the algorithm
(this is an over simplification, but OK for now).  There is no way to
show that the state change made by f is the same as the one made by @ --
no way to show that f chooses the same x as @.

On the other hand, the only property of x that one knows and can use in
a proof is that x satisfies P.  So presumably, if one had a proof of a
term involving (@x.Px), the same proof should work for a term which
substituted (f P) for (@x.Px).  But this is a meta-theorem, something
like
 (|- t[...,(@x.Px),...])  ==> (|-(!f (!Q.Q (f Q)) ==> t[...,(f P),...]))
I don't think the un-meta version of this (take out the turnstiles) can
be proven in HOL.  (From what I understand about Isabelle, the meta
version could be proven there.)

I have concluded that @ is the wrong thing to use in specifying an
algorithm, where your goal is to prove an implementation.  If I've
gotten any of this wrong, I would sure like to hear about it.


--Sandy Murphy
  Trusted Information Systems