Date: Tue, 30 Jul 91 16:38:16 BST
From: Mike Gordon <mjcg%cam.sri.com@com.sri.ai>
Message-Id: <9107301538.AA08235@harlech.cam.sri.com>
To: guttman@org.mitre.linus
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: guttman@linus.mitre.org's message of Tue, 30 Jul 91 08:54:36 -0400 <9107301254.AA00690@malabar.mitre.org>
Subject: Select operator (practical perspective)


Re. Josh's last message:

My feeling is that from a practical point of view epsilon is a bit like
lambda: eliminable in principle, but handy in practice (lambda
abstractions are not necessary because one could always introduce a
new function symbol instead; similarly epsilon-terms are not
necessary because one could always introduce a new constant using a
specification).

However, lambda and epsilon are nifty because they allow things to be
denoted "on-the-fly" without extending the signature.

On the subject of INVERSE defined by:

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

The properties I needed were the following (which were straightforward
to prove).

   |- !f. ONE_ONE(f:*->**) ==> !x. INVERSE f (f x) = x

   |- !f. ONTO(f:*->**) ==> !y. f(INVERSE f y) = y

   |- !(f:*->**). ONE_ONE f ==> !s. IMAGE (INVERSE f) (IMAGE f s) = s

I think that having "a relation between functions" might lead to notational
messiness in the statements of these elementary results.

Mike