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

Re: [PVS-Help] D_infinity construction in PVS

Steven: The PVS semantics document observes that all PVS types are 
rank-bounded and the D_infinity construction is not.  This means that
there is no way to define a dependent type D(n) such that D(n+1) =
[D(n)->D(n)].   There could be another way of defining it as a subtype
of some large type that contains all the elements you need for the


> In PVS, is it possible to construct a sequence type D, where D(0) is
> some given type, and D(n+1) has type [D(n) -> D(n)].  This is used in
> Scott's D_infinity construction.
> Thanks,
> Steven.