Re: More questions about predicate subtypes

[Hendrik Tews <tews@tcs.inf.tu-dresden.de>]

Hi,


Kellom{ki Pertti writes:
   From: Kellom{ki Pertti <pk@cs.tut.fi>
   Date: Tue, 24 Apr 2001 15:42:12 +0300 (EET DST)
   Subject: More questions about predicate subtypes
   
   I have some more questions about predicate subtypes. What I am trying
   to do is to use predicate subtypes to constrain more than one argument
   of a function. The following theory hopefully illustrates what I am
   doing:
   
   test: THEORY
    BEGIN
     obj: TYPE+
     t: TYPE+
     p: [obj, t -> bool]
     i: [(p) -> int]
     f: [(p) -> int] = LAMBDA (x: obj, st: t): i(x, st) + 1
     g(x: obj, st: (LAMBDA (s: t): p(x, s))): int = i(x, st) + 1
    END test
   
What about

     f1: [(p) -> int] = LAMBDA (z : (p)) : 
        let x = proj_1(z), 
            st = proj_2(z) 
         in i(x, st) + 1

(BTW the typechecker refuses x = z`1, I submit that as a bug.)

This produces a tcc 

    % Subtype TCC generated (at line 15, column 14) for  (x, st)
      % unfinished
    f1_TCC1: OBLIGATION
      FORALL (x, z: (p)):
	x = pi1(z) IMPLIES (FORALL (st): st = pi2(z) IMPLIES p(x, st));

that can be proved with 

    ;;; Proof for formula test.f1_TCC1
    ;;; developed with old decision procedures
    (""
     (SKOLEM-TYPEPRED)
     (SKOSIMP*)
     (EXPAND "pi1")
     (EXPAND "pi2")
     (CASE "(x!1, st!1) = z!1")
     (("1" (GRIND)) ("2" (GRIND))))


   I am trying to express a function of type [(p) -> int]. I would prefer
   the form in which f is written, but I get a TCC
   
     f_TCC1: OBLIGATION FORALL (st: t, x: obj): p(x, st);
   
   and I do not know how to get to the type information that says that
   p(x,st) is true. Skolemizing and doing (typepred "(x!1, st!1)") does
   not work.
   
This tcc is unprovable. I guess you hit one of the examples where
pvs 2.3 produces an unprovable tcc due to the change in the tcc
generation with respect to 2.2.

   My questions now are:
      - Can f_TCC1 be proved?

Only if you exploit a soundness problem.

      - Is restricting the last argument using dependent types as in g 
        completely equivalent to giving the restriction as in the
        declaration of f?
   
I would say yes, but then it should be possible to prove 

     eq : Lemma (lambda(x: obj, st: (LAMBDA (s: t): p(x, s))) : i(x,st)) = i

but this fails, because of an unprovable tcc. So the answer is
probably no, because the typechecker handles both alternatives
differently.

Bye,

Hendrik

-----------------------------------------------------------------
Hendrik Tews     Department of Theoretical Computer Science
                 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
-----------------------------------------------------------------