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

[PVS-Help] Dependent types in PVS



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