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

Re: More questions about predicate subtypes


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
   test: THEORY
     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
      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
     (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



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