Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
To: info-hol@cs.uidaho.edu (hol mailing list)
Subject: Re: Help: how to define the following in HOL
In-Reply-To: Your message of "Fri, 19 Nov 93 15:57:30 +0100." <199311191457.AA11133@infix.cs.ruu.nl>
Date: Sat, 20 Nov 93 15:00:55 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:085500:931120150102"@cl.cam.ac.uk>


Wishnu says:

  I want to define a predicate that characterizes a class of function,
  say a class of indentity-like function. My informal idea is as
  follows:

      id is an IDENTITish function iff

      (id o f) o (id o g) = (f o g)

  how can I define the predicate INDENTITish in HOL?

You are proposing, I assume, a definition like this:

  IDENTish(id) = !f g. (id o f) o (id o g) = (f o g)

or

  IDENTish(id) = (!f. id o f = f) /\ (!g. g o id = g)

Unfortunately it's not possible to do it, because in a definition all type
variables free in the RHS must be free in the LHS. This is necessary to
preserve consistency given the implicit quantification over polymorphic types
at the *sequent* level.

You can of course define the following equivalent:

  IDENTish(id) = !x. id(x) = x

but if you are hoping to be able to make categorical-style definitions with
quantification over *all functions* you may as well forget it, as HOL stands at
the moment. However, being able to make such definitions would be part of the
wonderland opened up by adding explicit (local) type quantification to the HOL
logic as proposed by Tom Melham.

John.