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

Re: WITH and dependent types




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