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

Re: [PVS-Help] Dependent types in PVS



Ken: It's still the case that dependencies can only affect the
predicates within types and not their type structure.  This is an
important closure condition for the whole language so that the semantics
can be given in Zermelo Set Theory.  The example of 3 -> R^3, by which I
assume you mean [n: nat -> R^n], can be encoded as a
dependent type [n: nat -> list_of_reals_of_length(n)], where
list_of_reals_of_length is the type of lists of reals restricted to
length n.  The PVS Semantics document:
  http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.pdf
might be a more informative reference.

Cheers,
Shankar

On 10/30/16 6:58 AM, Ken Kubota wrote:
> Dear PVS Users and Developers,
> 
> According to the 1999 paper (published in 2000) by Sam Owre and Natarajan 
> Shankar "[i]n PVS, the dependencies can only affect the predicates in a type 
> but not its structure. For example, the type [n : nat -> A^n] cannot be defined 
> in PVS."
> 	http://www.csl.sri.com/papers/wadt99/wadt99.pdf (p. 13, see also p. 9)
> 	http://dx.doi.org/10.1007/978-3-540-44616-3_3
> 
> This would mean that some mappings from terms to types, e.g., 3 -> R^3
> (= R x R x R), could not be expressed. Is this still valid as of today (2016)?
> 
> 
> The PVS Language Reference (Version 2.4, November 2001) available at
> 	http://pvs.csl.sri.com/doc/pvs-language-reference.pdf
> doesn't provide any other information in section 4.5 (Dependent types).
> 
> The background of my question is a classification of current logics and 
> implementations by their expressiveness in terms of the syntactic features of 
> the formal language:
> 	http://dx.doi.org/10.4444/100.111
> 
> 
> Kind regards,
> 
> Ken Kubota
> 
> ____________________
> 
> Ken Kubota
> doi: 10.4444/100
> http://dx.doi.org/10.4444/100
>