X400-Received: by mta hedera.stl.stc.co.uk in /PRMD=STC Plc/ADMD=GOLD 400/C=GB/;
               Relayed; Fri, 26 Jul 1991 10:06:03 +0100
X400-Received: by /PRMD=stc plc/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
               Fri, 26 Jul 1991 10:10:39 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; Relayed;
               Fri, 26 Jul 1991 09:44:45 +0100
Date: Fri, 26 Jul 1991 09:44:45 +0100
X400-Originator: R.B.Jones@gb.gold-400.icl.icl.win0103
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0103 0000010300000773]
Original-Encoded-Information-Types: undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 773
From: R.B.Jones@gb.gold-400.icl.icl.win0103
Message-Id: <"773*/I=RB/S=Jones/OU=win0103/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: More on the choice function


         MORE ON CHOICE

         Sorry Josh, I have to dissent from most of what you said in your
         last message to info-hol.

         The choice operator is not nearly as pathological as you suggest,
         it has no special status in the semantics and it is completely
         deterministic in the sense that the body completely determines the
         value.  This is in fact the reason why using choice is a poor way
         of writing a loose specification, and is demonstrated by the
         provability of the theorem:

         |- !p1,p2. (p1 = p2) => ((@x. p1 x) = (@x. p2 x))

         which is an instance of a more general result which can be
         specialised to choice.

         It's true that we don't know HOW the value of a choice expression
         is determined by its body, but we do know THAT it is.

         If you want to understand the motivation for the choice function
         then you must separate out the discussion of the choice function
         from the axiom of choice.

         The motivation for the axiom of choice is clearly mathematical,
         there are many results in classical mathematics which cannot be
         proven without it.  If you want to do classical mathematics then
         you need the axiom of choice.  There is then the question of how
         to introduce the axiom.  It is a convenience, and nothing more
         than that, to introduce the axiom of choice using the choice
         function.

         Given that Cambridge HOL now has the "new_specification" feature
         the choice function need not be primitive at all, definite
         description would suffice.  Provided that we have the axiom of
         choice (which can be expressed without reference to the choice
         function), we can prove consistent a loose specification which
         would introduce the choice function.

         A version of the axiom of choice (stuiable for HOL) may be
         expressed:

         !(R:*->**->bool) (!x.?y. R x y) => (?(f:*->**). !x. R x (f x))

         If we substitute for R the relation:

         \x:*->bool,y:*. (?z:*.x z) => x y

         then we obtain (after beta reduction):

         (!x:*->bool. ?y. (?z. x z) => x y)
              => (?f. !x. (?z. x z => (f x) z))

         The left hand side of this implication is clearly true, and the
         right hand side asserts the existence of a choice function; it can
         therefore be used to introduce a choice function using
         "new_specification".

         One reason why people may have difficulty in using the choice
         function is that they think it is less deterministic than is the
         case.  It is just as well behaved as any other function, we just
         don't happen to know much about the values it yields.

         I repeat finally my previous advice on how to avoid problems with
         the choice function:

              DON'T USE IT

         If you want a loose specification, use "new_specification", if you
         want a genuinely non-deterministic function (from * to ** say)
         then a HOL object of type ":*->**" will not do.  You could use a
         relation (":*->**->bool) to model a non-deterministic function,
         but you must accept that you are starting from scratch in the
         theory of this kind of function, and HOL's function application
         cannot be used for applying them (define your own).


         Roger Jones,  International Computers Limited,

         R.B.Jones@win0103.uucp