Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <20294-0@swan.cl.cam.ac.uk>; Thu, 23 Jul 1992 14:34:27 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08486; Thu, 23 Jul 92 06:18:50 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from ganymede.inmos.co.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08481; Thu, 23 Jul 92 06:15:58 -0700 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Thu, 23 Jul 92 14:04:56 BST From: David Shepherd Message-Id: <2370.9207231304@frogland.inmos.co.uk> Subject: Re: unbounded type in definition To: wishnu@nl.ruu.cs (Wishnu Prasetya) Date: Thu, 23 Jul 92 14:04:43 BST Cc: info-hol@edu.uidaho.cs.ted In-Reply-To: <199207231046.AA25520@infix.cs.ruu.nl>; from "Wishnu Prasetya" at Jul 23, 92 12:46 pm X-Mailer: ELM [version 2.3 PL11] Wishnu Prasetya has said: > Hello, > > I have the following two definitions: > > new_definition (`flup`, > "flup X = > !fP:num->*. !V:(num) set. !i:num. i IN V ==> X (fP i)") ;; > > new_definition (`flop`, > "flop X = > !fP:**->*. !V:(**) set. !i:**. i IN V ==> X (fP i)") ;; > > it doesn't matter what flup and flop may represent, but flup is > accepted by HOL, but not flop. The only difference between flup and > flop is that I have replace the type `num` in flup with the > polymorphic `**` in flop. HOL doesn't accept this, complaining that ** > is an unbound type. Then how do I suppose to define flop? the problem is that :** is not bound in the lhs of the definition. if you allow this definition then you could define BOGUS (x:bool) = ! (f:bool->*) y . f y = f x then instatiating :* to :one (the one element type) we get BOGUS T = ! (f:bool->one) y. f y = f T ---> BOGUS T = ! (f:bool->one) y. one = one ---> BOGUS T since f x = one as :one only has one element. then instantiating :** to :bool we get BOGUS T = ! (f:bool->bool) y. f y = f T ---> BOGUS T = ! y. ~y = ~T ---> ~BOGUS T hence without this restriction the logic is inconsistent. btw ... what is flop meant to do? as far as i can see the quantification on V is vacuous. perhaps you mean "flop X V = !fP:**->*. !i:**. i IN V ==> X (fP i)") ;; which would be accepted -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk or des@inmos.com tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "i speak latin to god, spanish to men, french to women and german to my horse." - charles v of spain