Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

No - you would have to encode the notion of sorts in some way. Maude 
sorts are stored as 16-bit signed numbers so there is a hard limit of 
32767 user sorts per connected component. The expectation is that the 
number of sorts per component will be significantly smaller than this 
for real code. The subsort relation is encoded using bit vectors and 
there is a performance hit for more than 63 user sort per component (on 
a 64-bit machine) and the sorting function for an operator is encoded 
using an ordered decision diagram (which could in principle be 
exponential in the number of arguments).

Steven

On 2/3/14 12:58 PM, Randy Pollack wrote:
> Hello,
>
> I want to define and reason about an order-sorted signature containing
> infinitely many sorts
>
>      S_0<  S_1<  ...
>
> The operators will have signatures such as
>
>      proj(n,i) : S_n                     (if 0<  i<= n  in Nat)
>      pair(n): S_n, S_n ->  S_n
>
> Can this be expressed in Maude?  Please point me to the user manual or
> the Maude book where this is described.
>
> Thanks for any info.
>
> Randy Pollack
> --
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help