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

*To*: pvs-help@csl.sri.com*Subject*: Re: WITH and dependent types*From*: John Hoffman <hoffman@securecomputing.com>*Date*: Tue, 30 Sep 1997 14:59:06 -0500 (CDT)

Since no one has answered, I'll take my best guess. > I found the following inconvenience in the WITH mechanism, > in combination with dependent types. In fact I wonder > what is the intended behaviour of PVS? > > Given the type S: TYPE = [# X: setof[nat] , f: [(X)->(X)] #], > the function add is defined as follows: > add(s:S, x:nat):S = s WITH > [ X |-> add(x,X(s)), > (f)(x) |-> x] As I understand it, (f)(x) |-> x is telling PVS to replace the current definition of f(x) with x, but it is required that x be in the domain of f in order for this construct to work. This construct does not extend domains. > This gives two TCCs: > > add_TCC1: OBLIGATION (FORALL (s: S, x: nat): add[nat](x, X(s))(x)); > add_TCC2: OBLIGATION (FORALL (s: S, x: nat): X(s)(x)); > > The first is OK (subtype-tcc). The second is not provable. The more > verbose variant below correctly generates only the first TCC. > > add(s:S, x:nat):S = s WITH > [X |-> add(x,X(s)), > f |-> f(s) WITH [x|-> x]] The with construct here extends the domain, so since f(s) is a function with domain X(s) then f(s) WITH [x |-> x] is a function with domain add(x,X(s)) > I would expect that either both definitions fail or both succeed. > Both succeed is more practical. Both fail is in accordance with > the PVS language document, which says that multiple overwrites > are rewritten as single overwrites. The language document that I have (the june '93 version) doesn't specify how the record update construct you're using in the first example (f)(x) |-> x is instantiated. > Note that > (s WITH [X |-> add(x,X(s))] ) WITH [(f)(x) |-> x] > is clearly ill-typed, due to the dependent types. And this is why your first example doesn't typecheck. I believe this answers your question doesn't it? since the above doesn't typecheck, but s WITH [X |-> add(x,X(s)), f |-> f(s) WITH [x|-> x]] does, now we know why. The first version doesn't typecheck because it doesn't extend the domain of f, and PVS doesn't extend domains in the record update as you specified. Hope this helps. John ==============================++====================== John Hoffman, PhD || Secure Computing Corporation || Sushi is good? 2675 Long Lake Road || Life is good! Roseville, MN 55124 || hoffman@securecomputing.com || Fax :(612)628-2701 || - Origami Sushi Chef Phone:(612)628-2808 || ==============================++======================

- Prev by Date:
**Re: Accumulation quantifier support?** - Next by Date:
**Union over a set; quantifiers** - Prev by thread:
**Re: WITH and dependent types** - Next by thread:
**How can we extend type bool with a "bottom" element?** - Index(es):