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

Re: subtyping problem



Jean-Paul BODEVEIX writes:
 > I am surprised by the proof obligations generated by the
 > following example where I define two predicates p and q with
 >   (q) <: (p)  ie. (q) is a subtype of (p)
 > 
 > Then I define the function f with an argument of type (q) which is
 > initialised by a lambda expression with an argument of type (p). 
 > 
 > The initialization should be correct if the type of the rhs value is
 > a subtype of the type of the lhs value. However, PVS requires the types
 > to be identical (f_TCC3). Why ? Furthermore the TCC (1) seems 
 > inverted : it requires (p) :< (q).
 > Thanks for any help

In PVS, the domains of two functions must be exactly the
same for the functions' types to be compatible.

Sam Owre gave a good justification of PVS's treatment of
subtyping for functions on the main PVS list in April.  
I've quoted it below.

In the theory you showed, you can eliminate the unprovable
TCCs by writing the definition of f as

  f: [(q) -> nat] = restrict(LAMBDA (x: (p)): x - 1) 

As Sam points out, `restrict' is a conversion.  I don't
quite understand the circumstances under which conversions
are automatically applied, so I'm not sure why it must be
used explicitly here.

- Darrell

Sam Owre writes:
> We chose not to use contravariance in order to keep equality simple;
> equals can always be substituted for equals without worrying about the
> type of the equalities (assuming everything is well-formed to begin
> with).  Thus in
>        
> ex: THEORY
>  BEGIN
>   i: VAR int
>   n: VAR nat
>   abs(i): nat = IF i < 0 THEN -i ELSE i ENDIF
>   idint(i): int = i
>   idnat(n): nat = n
>   abs_is_id: FORMULA
>       idnat = abs and idnat = idint IMPLIES idint = abs
>  END ex
> 
> the formula abs_is_id should not be provable.  In PVS, the above does
> not typecheck as given because [nat -> nat] and [int -> nat] are not
> compatible types, i.e., they do not share a common supertype.  Not
> having contravariance can be inconvenient in many cases, so we added
> conversions to the language.  The prelude defines the restrict
> operator as follows:
> 
> restrict [T: TYPE, S: TYPE FROM T, R: TYPE]: THEORY
>  BEGIN
>   f: VAR [T -> R]
>   s: VAR S
>   restrict(f)(s): R = f(s)
>   CONVERSION restrict
>  END restrict
> 
> and given f:[int->int], G[[nat->int]->bool], G(f) is automatically
> transformed by the typechecker to G(restrict[int,nat,int](f)).
> We also define an extension operator:
> 
> extend [T: TYPE, S: TYPE FROM T, R: TYPE, d: R]: THEORY
>  BEGIN
>   f: VAR [S -> R]
>   t: VAR T
>   extend(f)(t): R = IF S_pred(t) THEN f(t) ELSE d ENDIF
>  END extend
> 
> In this case, we can't easily make extend a conversion, as the
> typechecker will never be able to derive the default value d.  This
> default is similar to using 0 or 9999 as a default representing
> invalid values in a program or database.  In one case that occurs
> frequently, however, there is a good default value.  This is when
> dealing with predicates (which are also sets in PVS), where the
> range type is boolean.  By using FALSE for the default, as is done
> in the prelude, then given s:pred[nat], P[pred[int] -> int], the
> term P(s) is transformed to P(extend[int,nat,bool,false](s)).  This
> allows a set of nats to be viewed as a set of ints.
> 
> In the abs_is_id example, the restrict operator is automatically
> applied, and if you try to prove the formula you will see
> 
> abs_is_id :  
> 
> {-1}    idnat = restrict(abs)
> {-2}    idnat = restrict(idint)
>   |-------
> {1}    idint = abs
>