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

Re: [PVS-Help] Dependent types in PVS



Dear Natarajan Shankar,

Thank you very much for the helpful explanation, which is similar to that in 
the document (p. 35) for which you kindly provided the link.

Best wishes,

Ken Kubota

____________________

Ken Kubota
doi: 10.4444/100
http://dx.doi.org/10.4444/100



> Am 30.10.2016 um 18:19 schrieb Natarajan Shankar <shankar@xxxxxxxxxxx>:
> 
> 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
>>