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

Re: Type-correctness conditions in HOL

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
-----------------------------------------------------------------
References: