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

Re: WITH and dependent types


The language document is out of date, and badly needs to be updated.
Otherwise there is no real bug here.

As you noted, an override expression with multiple assignments can be
separated into a sequence of single assignments only if dependent types
are not involved.  For dependent record (or tuple) types, the assignments
are all done in parallel.  In effect, the left-hand sides are all
evaluated and then updated with the right-hand sides.  Thus
   [  X    |-> add(x,X(s)), 
    (f)(x) |-> x]
is equivalent to
   [(f)(x) |-> x,
      X    |-> add(x,X(s))]

With function updates, the domain of the function may be extended if
necessary to include the new element.  This means that (finite) functions
may be built from the empty function.  Thus in
   f(s) WITH [x|-> x]
the typechecker checks whether x is of a subtype of the domain type for f,
and if it cannot determine it the type for the WITH expression is
   {y: setof[nat] | X(y) OR y = x}
This is why the second form works.

I hope this is an adequate explanation; if not, I'm happy to discuss it



> Hi,
> 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]
> 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]]
> 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. Note that 
>   (s WITH [X |-> add(x,X(s))] ) WITH [(f)(x) |-> x]
> is clearly ill-typed, due to the dependent types.