Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199311191541.AA13132@infix.cs.ruu.nl>
Subject: Re: Help: how to define the following in HOL
To: des@inmos.co.uk (David Shepherd)
Date: Fri, 19 Nov 1993 16:41:33 +0100 (MET)
Cc: info-hol@cs.uidaho.edu (hol mailing list)
In-Reply-To: <23716.9311191532@frogland.inmos.co.uk> from "David Shepherd" at Nov 19, 93 03:32:40 pm
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 1031

  > > 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?
  > 
  > Not surprising ... the two occurrence of "id" have different types.
  > The first is ":*C->?1" and the second ":*B->B". So, even if you supplied
  > more type information, unless you constrain f and g to have the same
  > types then the two occurences of id represent different terms.
  > 
  > What you want to define, I think, requires type quantification and 
  > instatiation.
  > --------------------------------------------------------------------------
  > david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625

Hi David, 
So, are you saying that I can't define INDENTITish is HOL (or at least
not without first defining some theory over types ontop of HOL logic)?

-Wishnu-