Date: Mon, 29 Jul 91 11:27:45 BST
From: Mike Gordon <mjcg%cam.sri.com@com.sri.ai>
Message-Id: <9107291027.AA06596@harlech.cam.sri.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Select operator (practical perspective)


I'm not sure if all of the messages below reached info-hol. I suspect
not, so here is some discussion on practical aspects of the choice
operator; this was prompted by Josh's questions. Apologies if you
have seen this before.

Mike

-----------------------------------------------------------------------


As I understand it, the key idea of Hilbert was that the
epsilon-operator is not "non-deterministic". It just denotes a
canonical element of the domain of a predicate. By this trick, Hilbert
was able to get a choice operator within ordinary logic, without the
hassle of having non-denoting terms. The semantics of epsilon-terms is
straightforward within a conventional Taskian semantics. For details,
see the book:

   A. Leisenring, "Mathematical Logic and Hilbert's epsilon-Symbol",
   Macdonald & Co. Ltd., London, 1969.

or Section 10.2.1 of Chapter 10 of DESCRIPTION (one of the volumes of
the HOL documentation).

You ask:

   Why does HOL have to have this operator, and how is it properly
   (reliably) used?

Different people use it in different ways. I just did an fgrep on a
directory of mine containing some current work on real-time program
verification. This contains the definition:

   define "Min P = @x. IsMin P x"

where "IsMin P x" is true if "x" is a minimal element of the domain of
"P". Theorems like the following are then proved:

   |- !P n. P n ==> P(Min P)
   |- !P n. n < (Min P) ==> ~P n
   |- !P x. P x ==> IsMin P(Min P)
   |- !P n. P n ==> (Min P) <= n
   |- !P n. IsMin P n ==> (n = Min P)
   |- !P n. IsMin P n = P n /\ (n = Min P)

A similar example is in the library prog_logic88, where Dijkstra-style
weakest preconditions are defined and various laws about them proved:

   define "WEAKER p' p = !s:*. p s ==> p' s"


   define "WEAKEST(P:(*->bool)->bool) =
            @p. P p /\ !p'. P p' ==> WEAKER p p'"

Yet another example is the definition of fixed-points (see the library
fixpoints)

  define "FIX fun =
           @f:*->bool. (fun f = f) /\ !f'. (fun f' = f') ==> (f << f')"

with suitable definitions (see the library for details) one can then
prove Scott-induction in the form:

   |- "!(p:(*->bool)->bool) fun.
        ADMITS_INDUCTION p /\
        CONTINUOUS fun     /\
        p BOT              /\
        (!f. p f ==> p(fun f))
        ==>
        p(FIX fun)"

Besides in definitions, I also sometimes use epsilon-terms as
existential witnesses to solve existential goals via EXISTS_TAC (but
I'd guess that Prolog-style logical variables would be a better
method).

-----------------------------------------------------------------------

Yes, I agree "canonical" makes the choice function seem less arbitrary
than it is -- however I was reacting to "non-determininstic"!

I think most uses of epsilon, at least in specifications, are really
definite descriptions. However, the big advantage of not having
definite descriptions is that one does not need uniqueness for the
term to be well formed. I have discussed this somewhat with Mike
Fourman in the past. In his logic (and presumably yours too) this is
less of a problem. One could imagine defining fixedpoint and minimality
separately:

   FIX f = @x. (f x = x)

here the epsilon is not an iota.

My general feeling about epsilon is that it not really necessary, but
it is quite elegant, logically harmless and occasionally gets one out
of a tricky spot. It's main problem is that logically inexperienced
users tend to think it is more useful than it is -- it has a sort of
magical power that is illusory.

I probably wouldn't prove the example you [refers to Josh -- MJCG]
give using epsilon-terms, but one could. The examples I had in mind
were situations where the existential witness was some fairly
complicated function of the current assumptions.  I always regard
proofs done this way as a bit of a hack -- but then ad hoc proof hacks
happen a lot (alas) with HOL.


-----------------------------------------------------------------------

I looked around in my own files and the HOL Library to see what other
uses of epsilon I could find.

Here is the definition of the inverse of a function:

   define "INVERSE(f:*->**) = \y. @x. f x = y"

This isn't a definite description.

An example proof using epsilon to define a witness is the following
one taken from the sets library (g sets up a goal; e expands with a
user-supplied tactic; input preceded by # comes from the user, other
stuff is output from the system).

#g "?choice. !s:(*)set. ~(s = {}) ==> (choice s) IN s";;
"?choice. !s. ~(s = {}) ==> (choice s) IN s"

#e(REWRITE_TAC [EXTENSION;NOT_IN_EMPTY]);;
Theorem NOT_IN_EMPTY autoloaded from theory `sets`.
NOT_IN_EMPTY = |- !x. ~x IN {}

Theorem EXTENSION autoloaded from theory `sets`.
EXTENSION = |- !s t. (s = t) = (!x. x IN s = x IN t)

OK..
"?choice. !s. ~(!x. ~x IN s) ==> (choice s) IN s"

#e(EXISTS_TAC "\s. @x:*. x IN s");;
OK..
"!s. ~(!x. ~x IN s) ==> ((\s. @x. x IN s)s) IN s"

#e(CONV_TAC (ONCE_DEPTH_CONV BETA_CONV));;
OK..
"!s. ~(!x. ~x IN s) ==> (@x. x IN s) IN s"

#e(CONV_TAC (ONCE_DEPTH_CONV SELECT_CONV));;
OK..
"!s. ~(!x. ~x IN s) ==> (?x. x IN s)"

#e(CONV_TAC (ONCE_DEPTH_CONV NOT_FORALL_CONV));;
OK..
"!s. (?x. ~~x IN s) ==> (?x. x IN s)"

#e(REWRITE_TAC []);;
OK..
goal proved
|- !s. (?x. ~~x IN s) ==> (?x. x IN s)
|- !s. ~(!x. ~x IN s) ==> (?x. x IN s)
|- !s. ~(!x. ~x IN s) ==> (@x. x IN s) IN s
|- !s. ~(!x. ~x IN s) ==> ((\s. @x. x IN s)s) IN s
|- ?choice. !s. ~(!x. ~x IN s) ==> (choice s) IN s
|- ?choice. !s. ~(s = {}) ==> (choice s) IN s