[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs@csl.sri.com*Subject*: Re: Type-correctness conditions in HOL*From*: Hendrik Tews <tews@tcs.inf.tu-dresden.de>*Date*: Thu, 3 Aug 2000 14:58:40 +0200 (MET DST)*Cc*: pvs@csl.sri.com, mjones@cs.utah.edu, konrad.slind@cl.cam.ac.uk, mike.gordon@cl.cam.ac.uk*Delivery-Date*: Thu Aug 3 05:58:52 2000*In-Reply-To*: <E13K1eL-0007jO-00@wisbech.cl.cam.ac.uk>*References*: <E13K1eL-0007jO-00@wisbech.cl.cam.ac.uk>

Joe Hurd writes: From: Joe Hurd <Joe.Hurd@cl.cam.ac.uk> Date: Wed, 02 Aug 2000 17:45:44 +0100 Subject: Type-correctness conditions in HOL term_TCC1: OBLIGATION FORALL (x : A) : P(x); Which may well be false. Can this `too-strong' TCC cause any problems in PVS? In principle yes. It might be, that you can't complete the proof chain for a theorem because of an unprovable TCC although the theorem itself is true. This happend to me serveral times. But compared to the cases where I got unprovable TCC's because my theories were wrong, it is negligible. In my opinion it is reasonable to expect that the user provides enough context information for the generation of the TCC's. In your example the user should write term1 : bool = EXISTS (x : A) : P(x) and (LAMBDA (y : (P)) : TRUE)( x ) A second example where unprovable TCC's are generated, because the user provides wrong information is the following: t1 : bool = Forall( n : nat ) : 10 >= 10 / n or n = 0 PVS generated the unprovable TCC n /= 0. But I think it is reasonable to expect the user to write instead t2 : bool = Forall( n : nat ) : n = 0 or 10 >= 10 / n and for t2 PVS does not generate a TCC. I think it is more interesting to look at cases, where PVS generates unprovable TCC's, although all the relevant information is available. Consider Prop : Theory Begin f : Var [nat -> [nat -> nat]] prop?(f) : bool = f(0)(0) < f(1)(1) g : [int -> [int -> int]] = lambda(m : int) : Lambda(n:int) : m + n + 4 g_prop : Lemma prop?(g) end Prop Here PVS generates the unprovable TCC % Subtype TCC generated (at line 13, column 23) for restrict(g) % untried g_prop_TCC1: OBLIGATION FORALL (x1: nat): (FORALL (x: int): x >= 0) AND (FORALL (x2: int): restrict[int, nat, [int -> int]](g)(x1)(x2) >= 0); although from the type information it is clear, that FORALL (x: nat): (FORALL (y: nat): g(x)(y) >= 0); would be sufficient to ensure soundness. Bye, Hendrik ----------------------------------------------------------------- Hendrik Tews PhD student in theoretical computer science at Dresden University of Technology, Germany Telefon: +49 351 463 8351 e-mail: tews@tcs.inf.tu-dresden.de www: http://home.pages.de/~tews/ pgp key: http://home.pages.de/~tews/pgpkey.asc -----------------------------------------------------------------

**Type-correctness conditions in HOL***From*: Joe Hurd <Joe.Hurd@cl.cam.ac.uk>