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

WITH and dependent types


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.

| Jaco van de Pol,                     /                          /
| Eindhoven University of Technology / Phone: +31-(0)40-2474350 / 
| Department of Computing Science   / Fax: +31-(0)40-2468508   /
| P.O. Box 513,  5600 MB Eindhoven / E-mail:jaco@win.tue.nl   /
| The Netherlands      /-------------------------------------/
|---------------------/ http://www.win.tue.nl/win/cs/tt/jaco/