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

*To*: Kellom{ki Pertti <pk@cs.tut.fi>*Subject*: Re: More questions about predicate subtypes*From*: Hendrik Tews <tews@tcs.inf.tu-dresden.de>*Date*: Tue, 24 Apr 2001 17:58:47 +0200*Cc*: pvs@csl.sri.com*In-Reply-To*: <200104241242.PAA10939@arokyyhky.cs.tut.fi>*References*: <200104241242.PAA10939@arokyyhky.cs.tut.fi>*Sender*: pvs-owner@csl.sri.com

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

**References**:**More questions about predicate subtypes***From:*Kellom{ki Pertti <pk@cs.tut.fi>

- Prev by Date:
**More questions about predicate subtypes** - Next by Date:
**No Subject** - Prev by thread:
**More questions about predicate subtypes** - Next by thread:
**paperback announcement: Categorical Logic and Type Theory** - Index(es):